Computer Aided Verification

DOI10.1007/B98490MaRDI QIDQ5312907zbMATHOpenAlexFDO

Authors Alexander Rabinovich, Mooly Sagiv, Greta Yorsh, Thomas Reps, Neil Immerman

Publication date 25 August 2005

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

Full work available at URL https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated Deduction – CADE-20
• Simulating reachability using first-order logic with applications to verification of linked data structures
• A logic of reachable patterns in linked data-structures
• Tools and Algorithms for the Construction and Analysis of Systems
• Verifying concurrent data structures by simulation

Cited in

(11)

• Generalised multi-pattern-based verification of programs with linear linked structures
• Refinement checking based on simulation relations
• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Verification of multi-linked heaps
• Simulating reachability using first-order logic with applications to verification of linked data structures
• Formal verification of skiplists with arbitrary many levels
• Hybrid Systems: Computation and Control
• A logic of reachable patterns in linked data-structures
• Automated Deduction – CADE-20
• Quantitative separation logic and programs with lists

This page was built for publication: Computer Aided Verification

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