3 papers
cs.LO2026
A Program Logic for Abstract (Hyper)Properties
Paolo Baldan, Roberto Bruni, Francesco Ranzato +1
We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic…
cs.LO2025
U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
Flavio Ascari, Roberto Bruni, Roberta Gori +1
O'Hearn's Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms…
cs.LO2025
Model Checking as Program Verification by Abstract Interpretation (Extended Version)
Paolo Baldan, Roberto Bruni, Francesco Ranzato +1
Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions…