A Fully Verified Executable LTL Model Checker.

Javier Esparza Peter Lammich René Neumann Tobias Nipkow Alexander Schimpf Jan-Georg Smaus

Published in: CAV (2013)

Keyphrases

model checking
model checker
formal specification
temporal logic
formal verification
transition systems
symbolic model checking
formal methods
specification language
concurrent systems
artificial intelligence
reinforcement learning
knowledge representation
rough sets
ai planning