Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
From MaRDI portal
Publication:4916225
DOI10.1016/S1571-0661(04)80656-XzbMath1261.68106WikidataQ56020736 ScholiaQ56020736MaRDI QIDQ4916225
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
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
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