scientific article

zbMath0716.68035MaRDI QIDQ3204034

David E. Long, K. L. McMillan, Edmund M. Clarke

Publication date: 1989

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

model checkingparallel processesCTLprocess modelcommunicating processesprocess logic

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Logic in computer science (03B70)

Related Items

Projecting transition systems: overcoming state explosion in concurrent system verification ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ A mechanism of function calls in MSVL ⋮ A survey on compositional algorithms for verification and synthesis in supervisory control ⋮ Compositional runtime enforcement revisited ⋮ On the computation of counterexamples in compositional nonblocking verification ⋮ Compositional Verification for Component-Based Systems and Application ⋮ Verification of asynchronous systems with an unspecified component ⋮ Reasoning about programs by exploiting the environment ⋮ Verification of evolving software via component substitutability analysis ⋮ Formal Verification of Concurrent Systems via Directed Model Checking ⋮ A formal abstract framework for modelling and testing complex software systems ⋮ Automatic Synthesis of Assumptions for Compositional Model Checking ⋮ Grey-Box Checking ⋮ Bounded model checking of traffic light control system ⋮ Compositional Model Checking of product-form CTMCs ⋮ Compositional Failure-based Equivalence of Constraint Automata ⋮ Compositional minimisation of finite state systems using interface specifications ⋮ Runtime Verification of Component-Based Systems ⋮ A compositional \(\mu\)-calculus proof system for statecharts processes ⋮ A Logical Process Calculus ⋮ Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach ⋮ Automated formal analysis and verification: an overview