Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs

DOI10.1016/S1571-0661(04)80656-XzbMath1261.68106WikidataQ56020736 ScholiaQ56020736MaRDI QIDQ4916225

David Déharbe, Silvio Ranise

Publication date: 19 April 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)80656-x

Mathematics Subject Classification ID

68N99: Theory of software

Related Items

An instantiation scheme for satisfiability modulo theories, Theory decision by decomposition, SMELS: satisfiability modulo equality with lazy superposition, Efficient theory combination via Boolean search, Decision procedures for extensions of the theory of arrays, Distributing the Workload in a Lazy Theorem-Prover, SMELS: Satisfiability Modulo Equality with Lazy Superposition

Uses Software

• ESC/Java
• NQTHM
• E Theorem Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theorem-proving with resolution and superposition
• Set theory in first-order logic: Clauses for Gödel's axioms
• Introduction to the OBDD algorithm for the ATP community
• A rewriting approach to satisfiability procedures.
• A Switch-Level Model and Simulator for MOS Digital Systems
• Symbolic execution and program testing
• Assignment Commands with Array References
• The B-Book
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Automated Deduction with Shannon Graphs
• An axiomatic basis for computer programming
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic