Verification, Model Checking, and Abstract Interpretation
From MaRDI portal
Publication:5711490
DOI10.1007/B105073zbMATH Open1111.68398OpenAlexW2611288859MaRDI QIDQ5711490FDOQ5711490
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)
Cited In (15)
- Verifying Heap-Manipulating Programs in an SMT Framework
- Verify heaps via unified model checking
- 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
- Parameterized recursive refinement types for automated program verification
- Predicate abstraction for linked data structures
- 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
- Fuzzy set abstraction
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)