Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
High-Level Specifications: Lessons from Industry

Brannon Batson and Leslie Lamport

Abstract

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.

Details

Publication typeInproceedings
Published inFormal Methods for Components and Objects
URLhttp://www.springer-ny.com/
Pages242-262
Volume2852
SeriesLNCS
PublisherSpringer Verlag
> Publications > High-Level Specifications: Lessons from Industry