Brannon Batson and Leslie Lamport
We explain the rationale behind the design of the TLA+ specification language, and we describe our experience using it and the TLC model checker in industrial applications—including the verification of multiprocessor memory designs at Intel. Based on this experience, we challenge some conventional wisdom about high-level specifications.
|Published in||Formal Methods for Components and Objects|
All copyrights reserved by Springer 2003.