An automatic method for the dynamic construction of abstractions of states of a formal model

DOI10.1007/s10559-010-9235-9zbMath1288.68166OpenAlexW2037318704MaRDI QIDQ2452756

A. V. Kolchin

Publication date: 5 June 2014

Published in: Cybernetics and Systems Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10559-010-9235-9

zbMATH Keywords

verificationmodel checkingabstraction

Mathematics Subject Classification ID

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

Uses Software

• APS-1
• veriSoft
• BLAST
• NuSMV
• visualSTATE
• APS
• CBMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining partial-order reductions with on-the-fly model-checking.
• The complementation problem for Büchi automata with applications to temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Computations in APS
• Slicing software for model construction
• Control and data abstraction: The cornerstones of practical formal verification
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• Systems specification by basic protocols
• Guarded commands, nondeterminacy and formal derivation of programs
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate Abstraction with Under-approximation Refinement
• Depth-First Search and Linear Graph Algorithms
• Verification of large state/event systems using compositionality and dependency analysis

This page was built for publication: An automatic method for the dynamic construction of abstractions of states of a formal model