Model Checking

By D. Peled, Patrizio Pelliccione, P. Spoletini. 2018

5,383 citations recorded by the source corpus.

ion ● Approximation ○ M’ approximates M ○ Use M’ to deduce properties of M

Subfields: Computational Theory and Mathematics, Hardware and Architecture

How researchers see this paper

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

In Computational Theory and Mathematics

In Hardware and Architecture

Citations in the corpus

Explainable Planning (2017, methodology): “Model-checking algorithms and tools can prove very suitable [Clarke et al., 2001].”
Processing flows of information: From data stream to complex event processing (2012, methodology): “In particular, as these tools are heavily inspired by model checking [Clarke and Schlingloff 2001], rules are usually expressed in some kind of linear temporal logic [Pnueli 1997].”
Practical verification of decision-making in agent-based autonomous systems (2013, methodology): “The latter has been extremely successful in Computer Science and Artificial Intelligence, primarily through themodel checking approach (Clarke et al. 1999).”
Differential Dynamic Logic for Hybrid Systems (2008, positive): “Model Checking As a standard verification technique, model checking [15, 24] has been used successfully for verifying temporal logic properties [2, 24, 25, 50] of finitestate abstractions of automata-based transition structures by exhaustive state space exploration [3, 36, 37, 44].”
Worst‐case execution time analysis for a Java processor (2010, positive): “Even those efforts directed at the use of finite state model checking [8, 5] for concurrent and distributed program verification are too vast to survey; applications in telecommunication software design (e.”
A brief account of runtime verification (2009, neutral): “Traditionally, one considers three main verification techniques: theorem proving [12], model checking [20], and testing [49,16].”
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]).”
Temporal logic motion planning for dynamic robots (2009, positive): “Posing the topological graph as an FTS allows us to use standard automata theoretic techniques [5] in order to solve the high level planning problem.”
Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners (2009, neutral): “The following equivalences can be proved (amongst many others—indeed, until is sufficient to capture all other modalities that do not have numeric arguments [19]):”
Incremental Sampling-based Algorithms for Optimal Motion Planning (2010, background): “, ω-regular properties [44]) require cyclic trajectories, which are not included in trees.”
DecSerFlow: Towards a Truly Declarative Service Flow Language (2006, neutral): “Different algorithms have been studied in the field of model checking [15].”
Model Checking and the State Explosion Problem (2011, neutral): “7 of [11]).”
Uppaal SMC tutorial (2015, background): “, model checking [17], that is a more mathematical approach that can guarantee the absence of bugs in the system design.”
Towards automatic generation of vulnerability-based signatures (2006, positive): “Although in our example we can statically infer how many times to unroll the loop, in general such inferences are not possible and an upper bound to unroll loops must be provided (this is the same approach taken by bounded model checkers [15]).”
Executable cell biology (2007, positive): “This, however, can be done by a technique called model checking 28 , which systematically analyzes all of the infinitely many possible outcomes of a computational model without executing them one by one.”