Inferring invariants with quantifier alternations: taming the search space explosion
From MaRDI portal
Publication:6535571
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
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)