Inferring invariants with quantifier alternations: taming the search space explosion

DOI10.1007/978-3-030-99524-9_18MaRDI QIDQ6535571zbMATH OpenFDO

Authors Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken

Publication date 23 January 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

quantifier alternationinvariant inferencePDR/IC3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Quantified invariants via syntax-guided synthesis
• Bounded quantifier instantiation for checking inductive invariants
• Bounded quantifier instantiation for checking inductive invariants
• Property-directed inference of universal invariants or proving their absence
• Quantifiers on demand

Cites work

• Bounded quantifier instantiation for checking inductive invariants
• Bounded quantifier instantiation for checking inductive invariants
• Generalized property directed reachability
• Global guidance for local generalization in model checking
• Inferring inductive invariants from phase structures
• Property-directed inference of universal invariants or proving their absence
• Quantified invariants via syntax-guided synthesis
• Quantifiers on demand
• SAT-Based Model Checking without Unrolling
• SMT-based model checking for recursive programs
• Syntax-guided synthesis for lemma generation in hardware model checking
• Verification of threshold-based distributed algorithms by decomposition to decidable logics

This page was built for publication: Inferring invariants with quantifier alternations: taming the search space explosion

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