Automatic abstraction refinement for hyperproperties verification

DOI10.1007/978-3-032-32589-1_26MaRDI QIDQ7411184zbMATH OpenFDO

Authors Malak Marrid, Shachar Itzhaky, Sharon Shoham, Yakir Vizel

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_26

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Abstractions from proofs
• Automated hypersafety verification
• Constraint-based relational verification
• Counterexample-guided abstraction refinement for symbolic model checking
• Farkas-based tree interpolation
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• Lazy abstraction
• Lazy self-composition for security verification
• Model checking algorithms for hyperproperties (invited paper)
• Nested interpolants
• On recursion-free Horn clauses and Craig interpolation
• Predicate abstraction for software verification
• Software Verification of Hyperproperties Beyond k-Safety
• Static Analysis
• The \textsc{Golem} Horn solver
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Automatic abstraction refinement for hyperproperties verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411184)