19 January 2006
17 January 2006
Why: a software verification tool
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for
16 January 2006
The contributions
Formal verification of an extension of a UNIX compatible, secure filesystem
The TLA Tools Project
The goal of this project is to develop methods and tools that will permit engineers to apply formal specification and verification to high-level designs of concurrent algorithms and systems. We believe this can significantly improve the design process
