Checking properties of heap-manipulating procedures with a constraint solver

DOI10.1007/3-540-36577-X_37MaRDI QIDQ4417952zbMATH OpenFDO

Authors Mandana Vaziri, Daniel Jackson

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2619/26190505.htm

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Quantified Heap Invariants for Object-Oriented Programs
• Scalable error detection using Boolean satisfiability
• Model and proof generation for heap-manipulating programs
• Verification, Model Checking, and Abstract Interpretation
• Efficient bounded model checking of heap-manipulating programs using tight field bounds

Cited in

(5)

• Alloy*: a general-purpose higher-order relational constraint solver
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Visualizing SAT instances and runs of the DPLL algorithm
• A study of symmetry breaking predicates and model counting
• CRNs exposed: a method for the systematic exploration of chemical reaction networks

Describes a project that uses

Uses Software

• SLAM
• Bandera
• BerkMin
• SPIN

This page was built for publication: Checking properties of heap-manipulating procedures with a constraint solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4417952)