Bugs, moles and skeletons: symbolic reasoning for software development

DOI10.1007/978-3-642-14203-1_34MaRDI QIDQ5747779zbMATH OpenOpenAlexFDO

Authors Leonardo de Moura, Nikolaj Bjørner

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14203-1_34

Mathematics Subject Classification ID

Recommendations

• Symbolic optimization with SMT solvers
• Computer Aided Verification
• Satisfiability modulo theories
• A survey of satisfiability modulo theory
• Model Checking Software

Cites work

• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Constraint-Based Invariant Inference over Predicate Abstraction
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• From program verification to program synthesis
• Ranking function synthesis for bit-vector relations
• Schema-Guided Synthesis of Imperative Programs by Constraint Solving
• Simplify: a theorem prover for program checking
• Toward automatic program synthesis
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• Blocking and other enhancements for bottom-up model generation methods
• On interpolation in automated theorem proving
• Interpolation systems for ground proofs in automated deduction: a survey
• Semantically-guided goal-sensitive reasoning: model representation
• The QSMA algorithm for quantifiers in SMT

Describes a project that uses

Uses Software

• z3
• ESC/Java
• VCC
• Spec#
• SIMPLIFY
• Amphion

This page was built for publication: Bugs, moles and skeletons: symbolic reasoning for software development

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