Principles of model checking

By Christel Baier, Joost-Pieter Katoen. 2008

6,059 citations recorded by the source corpus.

Subfields: Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Program Analysis & Verification

Citations in the corpus

Extreme value theory for the study of probabilistic worst case delays in wireless networks (2016, methodology): “To address this issue, formal methods have been developed specifically to study real-time critical systems [3] [4].”
LTL2Action: Generalizing LTL Instructions for Multi-Task RL (2021, methodology): “Given a ﬁnite set of propositional symbols P , the syntax of an LTL formula is deﬁned as follows (Baier & Katoen, 2008): In contrast to propositional logic, LTL formulas are evaluated over sequences of observations (i.e., truth assignments to the propositional symbols in P ).”
A Program Logic for Union Bounds (2016, neutral): “Probabilistic model-checking is a successful line of research that has delivered mature and practical tools and addressed a broad range of case studies; Baier and Katoen [2], Katoen [26], Kwiatkowska et al. [30] cover some of the most interesting developments in the ﬁeld.”
Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation (2019, background): “Rather than continuing the race with adversaries, formal verification (Baier and Katoen, 2008; Barrett and Tinelli, 2018; Katz et al., 2017) offers a different approach: it aims at providing provable guarantees to a given model specification.”
Output Range Analysis for Deep Feedforward Neural Networks (2018, background): “While traditional system design approaches include rigorous system verification and analysis techniques to ensure the correctness of systems deployed in safety-critical applications [1], the inclusion of complex machine learning models in the form of deep NNs has created a new challenge to verify th”
Automated Verification Techniques for Probabilistic Systems (2011, background): “In particular, Chapter 10 of [11] covers some of the MDP model checking techniques presented here, but in greater depth, with additional focus on the underlying theory and proofs.”
Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools (2014, background): “A full discussion of minimization techniques is beyond the scope of this paper, but several are listed in [104].”
Set Propagation Techniques for Reachability Analysis (2021, neutral): “In the early 1980s, research on model checking of discrete state dynamical systems [1, 2] was initiated with the objective of proving automatically that a system satisfies some requirements.”
Contracts for System Design (2018, background): “The typical case is when these properties are languages or sets of traces, which includes the class of safety properties [173, 84, 196, 23, 89].”
A NICE Way to Test OpenFlow Applications (2012, neutral): “Testing correctness involves asserting safety properties (“something bad never happens”) and liveness properties (“eventually something good happens”), defined more formally in Chapter 3 of [19].”
Reachability Analysis and its Application to the Safety Assessment of Autonomous Cars (2010, background): “In terms of safety verification for stochastic dynamic systems, guaranteed results for largescale systems have only been obtained for purely discrete stochastic systems [95] which extend the classical model checking approach [16, 41].”
Hamilton-Jacobi reachability: A brief overview and recent advances (2017, background): “In particular, satisfaction of properties such as safety, liveness, and fairness in computer software and in discrete-time dynamical systems can be verified by checking whether runs of a transition system, or words of a finite automaton satisfy certain desired properties [17], [18].”
Statistical Model Checking: An Overview (2010, neutral): “Hence, statistical model checking provides a uniform approach for the veriﬁcation of a wide range of stochastic models, including Markov Chains or Continuous Timed Markov Chains.”
Temporal-Logic-Based Reward Shaping for Continuing Reinforcement Learning Tasks (2020, methodology): “…(v, a) ∈ W ∀ a ∈ Act(v) then Ĥ = Ĥ ∪ {v} end end Wmin0 (H) = (V ×A) \W returnWmin0 (H) end Algorithm 1: Almost-sure winning set construction We note that the algorithm above is a variation of the algorithm to compute the set of states with Prmin(s |= ♦B) found in (Baier and Katoen 2008).”
Model checking lots of systems: efficient verification of temporal properties in software product lines (2010, background): “We assume that the reader is familiar with automata theory and has basic knowledge of formal veriﬁcation (otherwise, see [6, 4]).”
Semantically-based crossover in genetic programming: application to real-valued symbolic regression (2011, methodology): “A controller is specified by a number of computation tree logic formulas [3].”
Learning to Compose Skills (2017, methodology): “In this work, we consider a subset of compositions deﬁned by Linear Temporal Logic (LTL) [18, 3].”
Output Range Analysis for Deep Neural Networks (2017, background): “…approaches include rigorous system veriﬁcation and analysis techniques to ensure the correctness of systems deployed in safety-critical applications (Baier and Katoen 2008), the inclusion of complex machine learning models in the form of deep NNs has created a new challenge to verify these models.”