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
(13)
Binary Decision Diagram
Decision Procedure
Finite Automata
General Methods
Graph Model
Model Checking
Observational Equivalence
Satisfiability
Specification Language
State Space
Symbolic Model Checking
Transition Systems
Linear Time Temporal Logic
Related Publications
(130)
Symbolic Model Checking: 10
GraphBased Algorithms for Boolean Function Manipulation
Symbolic model checking for sequential circuit verification
Symbolic model checking: an approach to the state explosion problem
Model checking
Subscribe
Academic
Publications
Symbolic Model Checking: 10^20 States and Beyond
Symbolic Model Checking: 10^20 States and Beyond,10.1109/LICS.1990.113767,Jerry R. Burch,Edmund Melson Clarke,Kenneth L. McMillan,L. J. Hwang
Edit
Symbolic Model Checking: 10^20 States and Beyond
(
Citations: 1532
)
BibTex

RIS

RefWorks
Download
Jerry R. Burch
,
Edmund Melson Clarke
,
Kenneth L. McMillan
,
L. J. Hwang
Many different methods have been devised for automatically verifying finite state systems by examining stategraph models of system behavior. These methods all depend on decision procedures that explicitly represent the
state space
using a list or a table that grows in proportion to the number of states. We describe a general method that represents the
state space
symbolically instead of explicitly. The generality of our method comes from using a dialect of the MuCalculus as the primary specification language. We describe a
model checking
algorithm for MuCalculus formulas that uses Bryant's Binary Decision Diagrams (1986) to represent relations and formulas. We then show how our new MuCalculus
model checking
algorithm can be used to derive efficient decision procedures for CTL model checking,
satisfiability
of lineartime
temporal logic
formulas, strong and weak
observational equivalence
of finite transition systems, and language containment for finite !automata.
Conference:
Logic in Computer Science  LICS
, pp. 428439, 1990
DOI:
10.1109/LICS.1990.113767
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.cadence.com
)
(
www2.cs.cmu.edu
)
(
www.cs.cmu.edu
)
(
www.informatik.unitrier.de
)
(
www.cs.cmu.edu
)
(
ieeexplore.ieee.org
)
(
www.cs.cmu.edu
)
(
w2.cadence.com
)
(
ieeexplore.ieee.org
)
More »
Citation Context
(618)
...We derive a transition relation in the standard way [
22
], by making two copies of the set of state variables: s ¼ð x1 ;x 2; ... ;x nÞ, denoting the variables of the current state, and s þ ¼ð x þ ;x þ ; ... ;x þ Þ, denoting the variables of...
Elena Dubrova
,
et al.
A SATBased Algorithm for Finding Attractors in Synchronous Boolean Ne...
...Symbolic algorithms have been shown to be applicable in many cases where exhaustive techniques do not scale [
7
]...
Andreas Classen
,
et al.
Symbolic model checking of software product lines
...This is utilized in symbolic model checking [
35
]...
Matthew L. Bolton
,
et al.
A Systematic Approach to Model Checking Human–Automation Interaction U...
...Many iteratively compute pre or postimages precisely [
7
,20] or approximately [21]; others unroll the transition relation [2,24,23]...
...Standard symbolic model checkers [
7
,20] and interpolationbased model checkers [21] compute inductive strengthenings of a given safety property P . Upon convergence, iterative postimage, respectively preimage, computation yields the strongest, respectively weakest, inductive strengthening of P , while approximate methods yield strengthenings of intermediate strength...
Aaron R. Bradley
.
SATBased Model Checking without Unrolling
...[
26
]). Here, it suffices to know that some operations are efficient in this form and others are not...
Marta Kwiatkowska
,
et al.
Incremental quantitative verification for Markov decision processes
References
(27)
Sequential Circuit Verification Using Symbolic Model Checking
(
Citations: 331
)
Jerry R. Burch
,
Edmund M. Clarke
,
Kenneth L. Mcmillan
Conference:
Design Automation Conference  DAC
, pp. 4651, 1990
Synthesis of Communicating Processes from Temporal Logic Specifications
(
Citations: 353
)
Zohar Manna
,
Pierre Wolper
Conference:
Logic of Programs
, pp. 253281, 1981
Using Partial Orders to Improve Automatic Verification Methods
(
Citations: 171
)
Patrice Godefroid
Conference:
Computer Aided Verification  CAV
, pp. 176185, 1990
Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic
(
Citations: 46
)
S. Bose
,
A. Fisher
Published in 1989.
Local Model Checking in the Modal MuCalculus
(
Citations: 201
)
Colin Stirling
,
David Walker
Conference:
Theory and Practice of Software Development  TAPSOFT
, pp. 369383, 1989
Sort by:
Citations
(1532)
A SATBased Algorithm for Finding Attractors in Synchronous Boolean Networks
(
Citations: 2
)
Elena Dubrova
,
Maxim Teslenko
Journal:
IEEE/ACM Transactions on Computational Biology and Bioinformatics  TCBB
, vol. 8, no. 5, pp. 13931399, 2011
A LTL Fragment for GR (1)Synthesis
(
Citations: 1
)
Andreas Morgenstern
,
Klaus Schneider
Journal:
Electronic Proceedings in Theoretical Computer Science
, vol. 50, pp. 3345, 2011
Symbolic model checking of software product lines
(
Citations: 2
)
Andreas Classen
,
Patrick Heymans
,
PierreYves Schobbens
,
Axel Legay
Conference:
International Conference on Software Engineering  ICSE
, pp. 321330, 2011
A Systematic Approach to Model Checking Human–Automation Interaction Using Task Analytic Models
(
Citations: 2
)
Matthew L. Bolton
,
Radu I. Siminiceanu
,
Ellen J. Bass
Journal:
IEEE Transactions on Systems, Man, and Cybernetics  TSMC
, vol. 41, no. 5, pp. 961976, 2011
SATBased Model Checking without Unrolling
(
Citations: 1
)
Aaron R. Bradley
Conference:
Verification, Model Checking and Abstract Interpretation  VMCAI
, pp. 7087, 2011