Verification, Model Checking, and Abstract Interpretation

DOI10.1007/B105073MaRDI QIDQ5711490zbMATH OpenOpenAlexFDO

Authors Roman Manevich, Eran Yahav, G. Ramalingam, Mooly Sagiv

Publication date 6 December 2005

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

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Predicate abstraction for linked data structures
• Verification, Model Checking, and Abstract Interpretation
• Verifying properties of well-founded linked lists
• scientific article; zbMATH DE number 1953039
• scientific article; zbMATH DE number 2102703

Cited in

(15)

• Fuzzy set abstraction
• Verify heaps via unified model checking
• Verifying Heap-Manipulating Programs in an SMT Framework
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Approximate super- and sub-harmonic response of a multi-DOFs system with local cubic nonlinearities under resonance
• Model checking dynamic memory allocation in operating systems
• Predicate abstraction for linked data structures
• Parameterized recursive refinement types for automated program verification
• Abstraction Refinement for Quantified Array Assertions
• Verifying properties of well-founded linked lists
• Verification of multi-linked heaps
• Programs with lists are counter automata
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• The Spotlight Principle

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 Q5711490)