Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
From MaRDI portal
Recommendations
- Pointer logic for verification of pointer programs
- Proving pointer programs in higher-order logic
- Proving pointer programs in higher-order logic.
- scientific article; zbMATH DE number 1612488
- Completeness and expressiveness of pointer program verification by separation logic
- Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
- Automated verification of recursive programs with pointers
- Exploiting pointer analysis in memory models for deductive verification
Cites work
- A rewriting approach to satisfiability procedures.
- A Switch-Level Model and Simulator for MOS Digital Systems
- An axiomatic basis for computer programming
- Assignment Commands with Array References
- Automated Deduction with Shannon Graphs
- Computing small clause normal forms
- scientific article; zbMATH DE number 1617320 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 1956575 (Why is no real title available?)
- scientific article; zbMATH DE number 1980926 (Why is no real title available?)
- Introduction to the OBDD algorithm for the ATP community
- Paramodulation-based theorem proving
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Set theory in first-order logic: Clauses for Gödel's axioms
- Symbolic execution and program testing
- The B-Book
- Theorem-proving with resolution and superposition
Cited in
(9)- 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
- Enhancing theorem prover interfaces with program slice information
- Distributing the workload in a lazy theorem-prover
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- An instantiation scheme for satisfiability modulo theories
- Programming Languages and Systems
This page was built for publication: Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4916225)
