Quantified invariants via syntax-guided synthesis

DOI10.1007/978-3-030-25540-4_14MaRDI QIDQ6194577zbMATH OpenOpenAlexFDO

Authors Grigory Fedyukovich, Sumanth Prabhu, K. Madhukar, Aarti Gupta

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25540-4_14

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Quantifiers on demand
• SMT-based array invariant generation
• Learning inductive invariants by sampling from frequency distributions
• Invariant Synthesis for Combined Theories
• Aligators for Arrays (Tool Paper)

Cited in

(10)

• Loop verification with invariants and contracts
• Unbounded procedure summaries from bounded environments
• Lemmaless induction in trace logic
• Synthesizing history and prophecy variables for symbolic model checking
• Inferring invariants with quantifier alternations: taming the search space explosion
• Maximizing branch coverage with constrained Horn clauses
• Automatic program instrumentation for automatic verification
• Lockstep composition for unbalanced loops
• A program instrumentation framework for automatic verification
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants

This page was built for publication: Quantified invariants via syntax-guided synthesis

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