The TLA+ Toolbox

We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineers. Two features are novel in the scope of formal IDEs: CloudTLC connects the Toolbox with cloud computing to scale up mo...

Full description

Bibliographic Details
Main Authors: Markus Alexander Kuppe, Leslie Lamport, Daniel Ricketts
Format: Article
Language:English
Published: Open Publishing Association 2019-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1912.10633v1