Incremental Instance Generation in Local Reasoning

DOI10.1007/978-3-642-02658-4_29MaRDI QIDQ3636873zbMATH OpenOpenAlexFDO

Authors Swen Jacobs

Publication date 30 June 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_29

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Deciding local theory extensions via E-matching
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Induction for SMT solvers

Cited in

(4)

• Decision Procedures for Automating Termination Proofs
• Incremental search for conflict and unit instances of quantified formulas with E-matching
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Towards Complete Reasoning about Axiomatic Specifications

Describes a project that uses

Uses Software

• SIMPLIFY

This page was built for publication: Incremental Instance Generation in Local Reasoning

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