Model checking lattices: using and reasoning about information orders for abstraction

DOI10.1093/JIGPAL/7.3.375zbMath0930.03031OpenAlexW1987507597MaRDI QIDQ4255977

Scott Hazelhurst, Carl-Johan H. Seger

Publication date: 15 February 2000

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/7.3.375

zbMATH Keywords

model checkingbilatticesautomatic verificationhardware verificationstate explosioncontradictory informationsymbolic trajectory evaluationinformation orderingquaternary logicfour-valued temporal logicvery large state spaces

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50) Temporal logic (03B44)

Related Items (1)

Data structures for symbolic multi-valued model-checking

This page was built for publication: Model checking lattices: using and reasoning about information orders for abstraction