Introduction to model checking

DOI10.1007/978-3-319-10575-8_1zbMATH Open1392.68242OpenAlexW2803481836MaRDI QIDQ3176359FDOQ3176359

Authors: Helmut Veith, Edmund Clarke, Thomas A. Henzinger 

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

Recommendations

• Handbook of model checking
• scientific article; zbMATH DE number 1487860
• Model checking
• scientific article; zbMATH DE number 910719
• Model checking.

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (17)

• Title not available (Why is that?)
• Meanings of model checking
• Title not available (Why is that?)
• A partial approach to model checking
• Combining model checking and testing
• Transfer of model checking to industrial practice
• Title not available (Why is that?)
• Explicit-state model checking
• Title not available (Why is that?)
• Model Checking – My 27-Year Quest to Overcome the State Explosion Problem
• Easy instances for model checking
• Model checking techniqes for the analysis of reactive systems
• First order Büchi automata and their application to verification of LTL specifications
• Tutorial on Model Checking: Modelling and Verification in Computer Science
• Handbook of model checking
• The Beginning of Model Checking: A Personal Perspective
• Temporal Logic for Programmable Logic Controllers

Uses Software

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

This page was built for publication: Introduction to model checking

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