Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development

DOI10.1007/978-3-642-14203-1_34zbMath1291.68377OpenAlexW1835682006MaRDI QIDQ5747779

Nikolaj Bjørner, Leonardo de Moura

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

Related Items (4)

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

Uses Software

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

Cites Work

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

This page was built for publication: Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development