Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic

By E. Clarke. 25 Years of Model Checking, 2008

1,682 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/843abecc52872013d64960bfae7533fa83a20372

How researchers see this paper

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

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Introduction to Embedded Systems - A Cyber-Physical Systems Approach (2013, background): “It was introduced by Clarke and Emerson (1981) and Queille and Sifakis (1981), which earned the creators the 2007 ACM Turing Award, the highest honor in Computer Science. Central to model checking is the notion of the set of reachable states of a system. Reachability analysis is the process of compu”
Program synthesis by sketching (2008, background): “In fact, Clarke and Emerson's seminal paper on model checking looked at the problem of synthesizing the synchronization logic in a program from temporal specications [20].”
Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III (2019, neutral): “In an oriented CTRS the conditions in the rules are interpreted as reachability and type 3 is a syntactic restriction on the distribution of variables in rewrite rules which ensure that rewriting does not introduce fresh variables [6].”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “Clarke and Emerson [36] and, independently, by Queille and Sifakis [97].”
Principles of model checking (2008, methodology): “Clarke and Emerson [86] reported the first (fair) CTL model checker, called EMC.”
Automated Verification Techniques for Probabilistic Systems (2011, methodology): “PCTL (Probabilistic Computational Tree Logic) [54,18] is a probabilistic extension of the temporal logic CTL [33].”
Model Checking and the State Explosion Problem (2011, methodology): “This framework was developed independently in the early 1980’s by Clarke and Emerson [8] and by Queille and Sifakis [22].”
Towards Verified Artificial Intelligence (2016, methodology): “Verification techniques such as model checking [9, 40, 10] and theorem proving (see, e.”
The software model checker Blast (2007, methodology): “Model checking is an algorithmic technique to verify a system description against a specification [ 20 ,22,75].”
Synthesis of Reactive(1) designs (2006, methodology): “This followed two previous attempts ([CE81], [MW84]) to synthesize programs from temporal specification which reduced the synthesis problem to satisfiability, ignoring the fact that the environment”