Synthesis of Circular Compositional Program Proofs via Abduction

DOI10.1007/978-3-642-36742-7_26zbMath1381.68057OpenAlexW176283517MaRDI QIDQ5326338

K. L. McMillan, Thomas Dillig, Mooly Sagiv, Isil Dillig, Bo-yang Li

Publication date: 5 August 2013

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-36742-7_26

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Assume, Guarantee or Repair ⋮ Theory exploration powered by deductive synthesis ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Backward symbolic execution with loop folding ⋮ Selectively-amortized resource bounding ⋮ Automated circular assume-guarantee reasoning ⋮ When Is a Formula a Loop Invariant? ⋮ Transformation-Enabled Precondition Inference ⋮ Automated program repair using formal verification techniques ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties ⋮ A unifying view on SMT-based software verification ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ From invariant checking to invariant inference using randomized search ⋮ Unnamed Item ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Scalable algorithms for abduction via enumerative syntax-guided synthesis