Verification, Model Checking, and Abstract Interpretation

DOI10.1007/11609773MaRDI QIDQ5898616zbMATH OpenOpenAlexFDO

Authors Thomas Wies, Viktor Kuncak, Patrick P. Lam, Andreas Podelski, Martin C. Rinard

Publication date 12 February 2007

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

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

Mathematics Subject Classification ID

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

Recommendations

• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Formal verification of skiplists with arbitrary many levels
• A shape graph logic and a shape system
• Fragment abstraction for concurrent shape analysis

Cited in

(8)

• Towards Complete Reasoning about Axiomatic Specifications
• Formal verification of skiplists with arbitrary many levels
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Verification of multi-linked heaps
• Analysis of constrained theories without use of primary constraints
• An efficient decision procedure for imperative tree data structures
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Verification, Model Checking, and Abstract Interpretation

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