1;3409;0c The TLA+ Proof System: Building a Heterogeneous Verification Platform

The TLA+ Proof System: Building a Heterogeneous Verification Platform

Oretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, vol. 6255, 2010
Pages: 44-44DOI: 10.1007/978-3-642-14808-8_3

International Colloquium on Theoretical Aspects of Computing

bibtex

Model checking has proved to be an efficient technique for finding subtle bugs in concurrent and distributed algorithms and systems. However, it is usually limited to the analysis of small instances of such systems, due to the problem of state space explosion. When model checking finds no more errors, one can attempt to verify the correctness of a model using theorem proving, which also requires efficient tool support.