Lemmaless induction in trace logic
From MaRDI portal
Publication:6160563
DOI10.1007/978-3-031-16681-5_14OpenAlexW4296050229MaRDI QIDQ6160563
Ahmed Bhayat, Pamina Georgiou, Laura Kovács, Clemens Eisenhofer, Giles Reger
Publication date: 2 June 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-031-16681-5_14
Cites Work
- Unnamed Item
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- \textsc{Diffy}: inductive reasoning of array programs using difference invariants
- Integer induction in saturation
- Induction with generalization in superposition reasoning
- Making theory reasoning simpler
- SMT-Based Array Invariant Generation
- Dafny: An Automatic Program Verifier for Functional Correctness
- Integrating Linear Arithmetic into Superposition Calculus
- Automating Inductive Proofs Using Theory Exploration
- Verifying Array Manipulating Programs with Full-Program Induction
- Coming to terms with quantified reasoning
- Quantifiers on demand
- Quantified invariants via syntax-guided synthesis
This page was built for publication: Lemmaless induction in trace logic
