Synthesis of circular compositional program proofs via abduction

DOI10.1007/978-3-642-36742-7_26MaRDI QIDQ5326338zbMATH OpenOpenAlexFDO

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

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

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

Recommendations

• Look for the proof to find the program: decorated-component-based program synthesis
• From program verification to program synthesis
• Automated circular assume-guarantee reasoning
• Ilinva: using abduction to generate loop invariants
• Compositional shape analysis by means of bi-abduction

Cited in

(21)

• Automated circular assume-guarantee reasoning
• A unifying view on SMT-based software verification
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Scalable algorithms for abduction via enumerative syntax-guided synthesis
• Backward symbolic execution with loop folding
• Selectively-amortized resource bounding
• 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
• When is a formula a loop invariant?
• Guiding Craig interpolation with domain-specific abstractions
• Assume, guarantee or repair
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• From invariant checking to invariant inference using randomized search
• Transformation-Enabled Precondition Inference
• Automated program repair using formal verification techniques
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Affine Loop Invariant Generation via Matrix Algebra
• Partial quantifier elimination and property generation
• On recursion-free Horn clauses and Craig interpolation
• Theory exploration powered by deductive synthesis

This page was built for publication: Synthesis of circular compositional program proofs via abduction

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