Inferring invariants with quantifier alternations: taming the search space explosion

DOI10.1007/978-3-030-99524-9_18zbMATH Open1547.68433MaRDI QIDQ6535571FDOQ6535571

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

Publication date: 23 January 2024

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

zbMATH Keywords

quantifier alternationinvariant inferencePDR/IC3

Mathematics Subject Classification ID

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

Cites Work

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

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)