Model Checking: Software and Beyond

This paper introduces model checking, originally conceived for checking finite state systems. It surveys its evolution to encompass finitely checkable properties of systems with un- bounded state spaces, and its application to software and other systems.

• Publication year

  2007

• Venue

  Journal of universal computer science (Online)

• Publication date

  Unknown publication date

• Fields of study

  Computer Science

• Identifiers
  DOI 10.3217/jucs-013-05-0639
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A machine program for theorem-proving

  2011cited by this paper
• The Birth of Model Checking

  2008cited by this paper
• An Abstraction Technique for Real-Time Verification

  2007cited by this paper
• MODEL CHECKING OF ROBOTIC CONTROL SYSTEMS

  2005cited by this paper
• A survey of recent advances in SAT-based formal verification

  2005cited by this paper
• Completeness and Complexity of Bounded Model Checking

  2004cited by this paper
• Modular verification of software components in C

  2004cited by this paper
• Bounded model checking

  2003influential reference
• Counterexample-guided abstraction refinement for symbolic model checking

  2003cited by this paper
• Modular verification of software components in C

  2003cited by this paper
• Interpolation and SAT-Based Model Checking

  2003cited by this paper
• Behavioral consistency of C and Verilog programs using bounded model checking

  2003cited by this paper
• Efficient Computation of Recurrence Diameters

  2002cited by this paper
• Lazy abstraction

  2002cited by this paper
• Chaff: engineering an efficient SAT solver

  2001cited by this paper
• Checking Safety Properties Using Induction and a SAT-Solver

  2000cited by this paper
• Counterexample-Guided Abstraction Refinement

  2000cited by this paper
• Bebop: A Symbolic Model Checker for Boolean Programs

  2000cited by this paper
• Symbolic Model Checking without BDDs

  1999cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• KRONOS: a verification tool for real-time systems

  1997cited by this paper
• Verifying the SRT Division Algorithm Using Theorem Proving Techniques

  1996cited by this paper
• Formal methods: state of the art and future directions

  1996cited by this paper
• Simple on-the-fly automatic verification of linear temporal logic

  1995cited by this paper
• Compositional and symbolic model-checking of real-time systems

  1995cited by this paper
• A Theory of Timed Automata

  1994cited by this paper
• Symbolic model checking

  1992cited by this paper
• Symbolic model checking

  1992cited by this paper
• Automata on Infinite Objects

  1991cited by this paper
• Symbolic Model Checking: 10^20 States and Beyond

  1990cited by this paper
• Model-checking for real-time systems

  1990cited by this paper
• Symbolic model checking: 1020 states and beyond

  1989cited by this paper
• Graph-based Algorithm for Boolean Function Manipulation

  1989cited by this paper
• Temporal Logic of Programs

  1987cited by this paper
• Automatic verification of finite-state concurrent systems using temporal logic specifications

  1986cited by this paper
• An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

  1986cited by this paper
• “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

  1986cited by this paper
• Graph-Based Algorithms for Boolean Function Manipulation

  1986cited by this paper
• Specification and verification of concurrent systems in CESAR

  1982cited by this paper
• The temporal logic of branching time

  1981cited by this paper
• The Temporal Semantics of Concurrent Programs

  1979cited by this paper
• A Computing Procedure for Quantification Theory

  1960cited by this paper

• Advancing verification of process mining models with quantitative model checking in stochastic environment

  2024cites this paper
• Ensuring Trustworthy and Ethical Behavior in Intelligent Logical Agents

  2024cites this paper
• Runtime verification of self-adaptive multi-agent system using probabilistic timed automata

  2023cites this paper
• Statistical Model Checking in Process Mining: A Comprehensive Approach to Analyse Stochastic Processes

  2023cites this paper
• PM2PMC: A Probabilistic Model Checking Approach in Process Mining

  2023cites this paper
• Runtime Verification of Multi-Agent Self-Adaptive System

  2021cites this paper
• Model Checking Based Approach for Compliance Checking ITC 2 / 48

  2019cites this paper
• Towards Integrated Correctness Analysis and Performance Evaluation of Software Systems (Doctoral Forum Paper)

  2019cites this paper
• Conformance Checking using Formal Methods

  2016cites this paper
• Introducing Mode Switch in Component-Based Software Development

  2015influential citation
• Model checking LTL properties over ANSI-C programs with bounded traces

  2015influential citation
• Applying symbolic bounded model checking to the 2012 RERS greybox challenge

  2014cites this paper
• UML-Checker: An Approach for Verifying UML Behavioral Diagrams

  2014cites this paper
• Formalization and verification of mode changes in hierarchical scheduling---An extended report

  2014cites this paper
• Self-checking Logical Agents

  2013cites this paper
• Model Checking LTL Properties over C Programs with Bounded Traces

  2013cites this paper
• Self-adaptive software needs quantitative verification at runtime

  2012cites this paper
• Temporal Meta-Axioms in Logical Agents

  2012cites this paper
• Generating correct compositions of semantic web services with respect to temporal constraints

  2012cites this paper
• Continually verify self-adaptation decisions taken by critical software in response to changes in the operating environment.

  2012cites this paper
• Generating model-based test cases from natural language requirements for space application software

  2011cites this paper
• Scientific Theories of Computational Systems in Model Checking

  2011cites this paper
• Context-Bounded Model Checking of LTL Properties for ANSI-C Software

  2011cites this paper
• Formal methods for the development and verification of autonomic IT systems

  2011cites this paper
• Formal Methods @ Runtime

  2010cites this paper
• Ensuring Agent Properties under Arbitrary Sequences of Incoming Events

  2010cites this paper
• Contracts Violation: Justification via Argumentation

  2009cites this paper
• Runtime Verification of Agent Properties

  2009cites this paper
• Proceedings of the 18th international conference on Applications of declarative programming and knowledge management

  2009cites this paper
• Chapter X A Multi-Level Time-Committed Framework for Evolving Agents

  2009cites this paper
• Specification and Dynamic Verification of Agent Properties

  2008cites this paper