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

DOI10.1016/S1571-0661(04)80656-XzbMath1261.68106OpenAlexW1991453972WikidataQ56020736 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

Related Items (7)

Efficient theory combination via Boolean search ⋮ An instantiation scheme for satisfiability modulo theories ⋮ SMELS: Satisfiability Modulo Equality with Lazy Superposition ⋮ Decision procedures for extensions of the theory of arrays ⋮ Theory decision by decomposition ⋮ 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

This page was built for publication: Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs