Showing cs.LOShow all
2 papers · 1 filter
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
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…