Skip to main content

The theory and practice of SALT


Andreas Bauer and Martin Leucker


Australian National University

Technische Universitaet Muenchen


This paper presents \SALT.

\SALT is a general purpose specification and assertion language developed for creating concise temporal specifications to be used in industrial verification environments.

It incorporates ideas of existing approaches, such as specification patterns, but also provides nested scopes, exceptions, support for regular expressions and real-time. The latter is needed in particular for verification tasks to do with reactive systems imposing strict execution times and deadlines. However, unlike other formalisms used for temporal specification of properties, \SALT does not target a specific domain.

The paper details on the design rationale, syntax and semantics of \SALT in terms of a translation to temporal (real-time) logic, as well as on the realisation in form of a compiler. Our results will show that the higher level of abstraction introduced with \SALT does not deprave the efficiency of the subsequent verification tools---rather, on the contrary.

BibTeX Entry

    author           = {Bauer, Andreas and Leucker, Martin},
    editor           = {{M. Bobaru, K. Havelund, G. Holzmann, R. Joshi}},
    month            = apr,
    year             = {2011},
    keywords         = {temporal logic, specification, verification},
    address          = {Pasadena, CA, USA},
    title            = {The Theory and Practice of {SALT}},
    pages            = {28},
    booktitle        = {NASA Formal Methods Symposium},
    publisher        = {Springer}


Served by Apache on Linux on seL4.