Experience with predicate abstraction

DOI10.1007/3-540-48683-6_16MaRDI QIDQ4817541zbMATH OpenFDO

Authors Satyaki Das, Seung Joon Park, David L. Dill

Publication date 24 September 2004

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

Full work available at URL https://doi.org/10.1007/3-540-48683-6_16

Mathematics Subject Classification ID

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

Recommendations

• A symbolic approach to predicate abstraction.
• Verification, Model Checking, and Abstract Interpretation
• Predicate abstraction with indexed predicates
• Predicate abstraction for program verification
• Predicate abstraction in program verification: survey and current trends

Cited in

(30)

• A local approach for temporal model checking of Java bytecode
• Correctness kernels of abstract interpretations
• Verification of SpecC using predicate abstraction
• Abstractions of data types
• Using heuristic search for finding deadlocks in concurrent systems
• Program verification with interacting analysis plugins
• Counter abstraction in the CSP/FDR setting
• A three-value abstraction technique for the verification of epistemic properties in multi-agent systems
• Predicate abstraction for program verification
• Model checking parameterized systems
• On height and happiness
• A Retrospective on Murϕ
• Predicate Abstraction in a Program Logic Calculus
• Compositional Predicate Abstraction from Game Semantics
• Program verification using symbolic game semantics
• Predicate abstraction with indexed predicates
• Predicate Abstraction via Symbolic Decision Procedures
• Indexed predicate discovery for unbounded system verification
• Competent predicate abstraction in model checking
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Predicate abstraction in a program logic calculus
• Predicate abstraction and canonical abstraction for singly-linked lists
• Predicate abstraction via symbolic decision procedures
• A symbolic approach to predicate abstraction.
• Verification, Model Checking, and Abstract Interpretation
• First order Büchi automata and their application to verification of LTL specifications
• Verifying time partitioning in the DEOS scheduling kernel
• Algebraic simulations
• Specification and verification of data-driven Web applications
• Efficient SAT-based bounded model checking for software verification

This page was built for publication: Experience with predicate abstraction

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