Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition

DOI10.1007/978-3-319-94144-8_22OpenAlexW2810373436MaRDI QIDQ1656596

Sorav Bansal, Aseem Saxena, Anmol Mahajan, Shubhani Gupta

Publication date: 10 August 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94144-8_22

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Towards a dereversibilizer: fewer asserts, statically

Uses Software

• Beaver
• WoLFram
• SMT-LIB
• Daikon
• Yices
• z3
• KLEE

This page was built for publication: Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition