Introduction to Model Checking

DOI10.1007/978-3-319-10575-8_1zbMath1392.68242OpenAlexW2803481836MaRDI QIDQ3176359

Helmut Veith, Thomas A. Henzinger, Edmund M. Clarke

Publication date: 20 July 2018

Published in: Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_1

Mathematics Subject Classification ID

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

Related Items (1)

Temporal Logic for Programmable Logic Controllers

Uses Software

• Coq
• Isabelle/HOL
• SPIN
• DART
• jSpin
• CESAR
• UMDES
• NModel
• Liss
• Limi
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Simulation distances
• Results on the propositional \(\mu\)-calculus
• Verification of sequential and concurrent programs
• 25 years of model checking. History, achievements, perspectives
• Time for verification. Essays in memory of Amir Pnueli
• Defining liveness
• Statecharts: a visual formalism for complex systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Learning programs from noisy data
• From Model Checking to Model Measuring
• Quantitative abstraction refinement
• Temporal Specifications with Accumulative Values
• A completeness theorem in modal logic
• Introduction to Discrete Event Systems
• Verification and Control of Hybrid Systems
• “Sometimes” and “not never” revisited
• Symbolic execution and program testing
• Proving the Correctness of Multiprocess Programs
• Shield Synthesis:
• Model-Based Software Testing and Analysis with C#
• An axiomatic basis for computer programming
• Classes of Recursively Enumerable Sets and Their Decision Problems
• From non-preemptive to preemptive scheduling using synchronization synthesis
• Software reliability methods. Foreword by Edmund M. Clarke
• LSCs: Breathing life into message sequence charts

This page was built for publication: Introduction to Model Checking