TY - GEN
T1 - The TLA+ proof system
T2 - 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010
AU - Chaudhuri, Kaustuv
AU - Doligez, Damien
AU - Lamport, Leslie
AU - Merz, Stephan
PY - 2010/11/9
Y1 - 2010/11/9
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/78049422555
U2 - 10.1007/978-3-642-14808-8_3
DO - 10.1007/978-3-642-14808-8_3
M3 - Conference contribution
AN - SCOPUS:78049422555
SN - 3642148077
SN - 9783642148071
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 44
BT - Theoretical Aspects of Computing, ICTAC 2010 - 7th International Colloquium, Proceedings
Y2 - 1 September 2010 through 3 September 2010
ER -