Symbolic Model Checking

E239161
formal verification technique model checking technique

Symbolic Model Checking is a formal verification technique that uses symbolic representations, such as binary decision diagrams, to efficiently verify properties of hardware and software systems with very large state spaces.

Try in SPARQL Jump to: Surface forms Statements Referenced by

All labels observed (4)

Label Occurrences
Symbolic Model Checking canonical 1
Symbolic Model Checking (paper) 1
Symbolic Model Checking: 10^20 States and Beyond 1

Statements (51)

Predicate Object
instanceOf formal verification technique ⓘ
model checking technique ⓘ
addresses state space explosion problem ⓘ
aimsTo verify properties of hardware systems ⓘ
verify properties of software systems ⓘ
associatedWithInstitution CMU ⓘ
surface form: Carnegie Mellon University
associatedWithResearcher E. Allen Emerson ⓘ
Edmund M. Clarke ⓘ
Kenneth L. McMillan ⓘ
checksPropertyType fairness properties ⓘ
liveness properties ⓘ
safety properties ⓘ
comparedTo explicit-state model checking ⓘ
coreConcept symbolic encoding of state sets as Boolean formulas ⓘ
symbolic encoding of transition relations as Boolean formulas ⓘ
hasAdvantage can handle extremely large state spaces compactly ⓘ
often more memory-efficient than explicit-state methods ⓘ
hasLimitation BDD size can blow up for some systems ⓘ
performance depends on variable ordering ⓘ
inspired development of SAT-based model checking ⓘ
introducedIn late 1980s ⓘ
notablePublication Symbolic Model Checking self-linksurface differs ⓘ
surface form: Symbolic Model Checking: 10^20 States and Beyond
operatesOn very large state spaces ⓘ
relatedTechnique SAT-based model checking ⓘ
SMT-based model checking ⓘ
bounded model checking ⓘ
represents sets of states symbolically ⓘ
transition relations symbolically ⓘ
supportsLogic CTL ⓘ
LTL ⓘ
temporal logic ⓘ
µ-calculus ⓘ
usedInDomain embedded systems verification ⓘ
hardware verification ⓘ
protocol verification ⓘ
usedInTool Cadence SMV ⓘ
NuSMV ⓘ
SMV ⓘ
usesAlgorithmicTechnique backward reachability ⓘ
fixed-point computation ⓘ
forward reachability ⓘ
reachability analysis ⓘ
usesDataStructure OBDDs ⓘ
ordered binary decision diagrams ⓘ
usesRepresentation BDDs ⓘ
binary decision diagrams ⓘ
symbolic representation ⓘ
verificationTarget communication protocols ⓘ
concurrent software ⓘ
finite-state systems ⓘ
synchronous hardware circuits ⓘ

Referenced by (4)

Full triples — surface form annotated when it differs from this entity's canonical label.

Edmund M. Clarke → notableWork → Symbolic Model Checking ⓘ
Symbolic Model Checking → notablePublication → Symbolic Model Checking self-linksurface differs ⓘ
this entity surface form: Symbolic Model Checking: 10^20 States and Beyond
Edmund Melson Clarke Jr. → notableWork → Symbolic Model Checking ⓘ
subject surface form: Edmund M. Clarke
this entity surface form: Symbolic Model Checking (paper)
Kenneth McMillan → notableWork → Symbolic Model Checking ⓘ
this entity surface form: Symbolic Model Checking: An Approach to the State Explosion Problem