Computer Aided Verification

DOI10.1007/B98490MaRDI QIDQ5312907zbMATH OpenOpenAlexFDO

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