Quantified invariants via syntax-guided synthesis

DOI10.1007/978-3-030-25540-4_14OpenAlexW2960656136MaRDI QIDQ6194577

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

Publication date: 16 February 2024

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

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)

Related Items (5)

\textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Loop verification with invariants and contracts ⋮ Lemmaless induction in trace logic ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ Unbounded procedure summaries from bounded environments

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