Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(9)
Automatic Verification
Binary Decision Diagram
Communication Protocol
Model Checking
Reactive System
Satisfiability
Sequential Circuits
Temporal Logic
State Transition Graph
Related Publications
(12)
Design and synthesis of synchronization skeletons using branching time temporal logic
Temporal and modal logic
Using model checking to generate tests from requirements specifications
Functional test generation using property decompositions for validation of pipelined processors
The Temporal Logic of Programs
Subscribe
Academic
Publications
Model Cheking
Model Cheking,10.1007/BFb0058022,Edmund M. Clarke
Edit
Model Cheking
(
Citations: 4031
)
BibTex

RIS

RefWorks
Download
Edmund M. Clarke
Model checking
is an automatic technique for verifying finitestate reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the
reactive system
is modeled as a statetransition graph. An efficient search procedure is used to determine whether or not the statetransition graph satisfies the specifications. We describe the basic
model checking
algorithm and show how it can be used with binary decision diagrams to verify properties of large statetransition graphs. We illustrate the power of
model checking
to find subtle errors by verifying part of the Contingency Guidance Requirements for the Space Shuttle.
Conference:
Foundations of Software Technology and Theoretical Computer Science  FSTTCS
, pp. 5456, 1997
DOI:
10.1007/BFb0058022
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
Citation Context
(2848)
... of nite state machines [20], asks the following question: given a (control ow) graph over a set of nodes and edges, an initial state, and an error state, does there exist a path from the initial to the error state? Subsequent to the recognition that a large class of computer systems can be modeled as nite state machines, this problem received a lot of attention from researchers interested in formal verication of computer systems [19,
7
]. ...
Akash Lal
,
et al.
Corral: A Solver for Reachability Modulo Theories
...We refer to [
12
] for detailed background on LTL, automata and model checking.,See [
12
] for a detailed description of the syntax and semantics of CTL.,Finally we note that all the algorithms of this section apply also to the more powerful branching time logic CTL* (see [
12
] for a definition) with exactly the same complexity:...
Patrice Godefroid
,
et al.
Analysis of Boolean Programs
...Other interesting directions are extensions of this approach to branching time logical specifications, such as computation tree logic specifications (Clarke
1997
), and to more complicated dynamics, such as polynomial dynamics (Benedetto
2002
)...
Yajuan Sun
,
et al.
An input–output simulation approach to controlling multiaffine system...
...Temporal logics (LTL, CTL and CTL*) were initially intended as a framework for specifying and verifying the correctness of digital circuits and computer programs [
1
]...
...Rich, humanlike specifications can be obtained by interconnecting these operators, and details on syntax, semantics, and usage of LTL X in connection with continuous systems can be found in [
1
], [2], [4]...
Narcis Ghita
,
et al.
Probabilistic carlike robot path planning from temporal logic specifi...
...It aims to be a lightweight verification technique complementing other verification techniques such as model checking [
2
] and testing [3]...
...• ⊲alive ∈ [0,
2
]Udone states that the event done has to occur eventually and that until then, the eventalive must occur every 2 time units...
...• ⊲alive ∈ [0,
2
]Udone evaluates to ? if done has not occurred so far while two subsequent occurrences of alive have never been separated by more than 2 time units...
Andreas Bauer
,
et al.
Runtime Verification for LTL and TLTL
References
(16)
SML: A high level language for the design and verification of finite state machines
(
Citations: 16
)
M. C. Browne
,
E. M. Clarke
Published in 1986.
Checking the correctness of sequential circuits
(
Citations: 13
)
M. Browne
,
E. M. Clarke
,
D. Dill
Published in 1985.
Automatic circuit verification using temporal logic: two new examples
(
Citations: 15
)
M. Browne
,
E. Clarke
,
D. Dill
Published in 1986.
Automatic Verification of Sequential Circuits Using Temporal Logic
(
Citations: 159
)
Michael C. Browne
,
Edmund M. Clarke
,
Bud Mishra
Journal:
IEEE Transactions on Computers  TC
, vol. 35, no. 12, pp. 10351044, 1986
GraphBased Algorithms for Boolean Function Manipulation
(
Citations: 5307
)
Randal E. Bryant
Journal:
IEEE Transactions on Computers  TC
, vol. C35, no. 8, pp. 677691, 1986
Sort by:
Citations
(4031)
Corral: A Solver for Reachability Modulo Theories
(
Citations: 1
)
Akash Lal
,
Shaz Qadeer
,
Shuvendu K. Lahiri
Published in 2012.
Analysis of Boolean Programs
Patrice Godefroid
,
Mihalis Yannakakis
Published in 2012.
An input–output simulation approach to controlling multiaffine systems for linear temporal logic specifications
Yajuan Sun
,
Hai Lin
,
Ben M. Chen
Journal:
International Journal of Control  INT J CONTR
, vol. aheadofp, no. aheadofp, pp. 113, 2012
Probabilistic carlike robot path planning from temporal logic specifications
Narcis Ghita
,
Marius Kloetzer
,
Octavian Pastravanu
Published in 2012.
Runtime Verification for LTL and TLTL
(
Citations: 11
)
Andreas Bauer
,
Martin Leucker
,
Christian Schallhart
Journal:
ACM Transactions on Software Engineering and Methodology  TOSEM
, pp. 164, 2011