Control and data abstraction: The cornerstones of practical formal verification

DOI10.1007/s100090050040zbMath1059.68589OpenAlexW2066680644MaRDI QIDQ1856157

Amir Pnueli, Yonit Kesten

Publication date: 2000

Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)

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

zbMATH Keywords

formal verificationmodel checkinglinear temporal logicdata abstractioncontrol abstractionnetwork invariantsafety and liveness propertyweak and strong fairness

Mathematics Subject Classification ID

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

Related Items

Compositional analysis for verification of parameterized systems, Model checking and abstraction to the aid of parameterized systems (a survey), Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions, \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms, Learning Meets Verification, An automatic method for the dynamic construction of abstractions of states of a formal model, Equational abstractions, Bridging the gap between fair simulation and trace inclusion, Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms, The Spotlight Principle, Network invariants for real-time systems, Narrowing and Rewriting Logic: from Foundations to Applications