SAL

SAL — the Symbolic Analysis Laboratory — is a declarative specification language and an accompanying toolkit for the formal analysis of concurrent and reactive systems. Developed by SRI International’s Computer Science Laboratory (the same lab behind the PVS theorem prover and the Yices SMT solver), SAL is built around a single idea: provide a clean, mathematical language for describing transition systems, and then bring a whole suite of automated analysis tools — several model checkers, a simulator, a deadlock checker, and a test generator — to bear on that one description. It is less a general-purpose programming language than a language for stating what a system does and what it must never do, so that machines can check the two against each other.

History & Origins

SAL grew out of a late-1990s observation in the formal-methods community: many excellent verification tools existed — symbolic model checkers, theorem provers, abstraction engines, static analyzers — but each demanded its own input notation, so combining them was painful. The SAL project set out to define a common intermediate language for transition systems that could serve as a meeting point for these tools.

The design was a collaboration. The language was developed by SRI together with researchers at Stanford University, UC Berkeley, and Verimag in France. It was first presented publicly in the paper An Overview of SAL, given at LFM 2000, the Fifth NASA Langley Formal Methods Workshop in June 2000. That paper laid out the vision: a language expressive enough to capture both finite- and infinite-state concurrent systems, and an open framework in which abstraction, invariant generation, slicing, model checking, and theorem proving could be combined to “perform symbolic analysis” of those systems.

Implementation followed in stages. SAL 1, released in July 2002, shipped an explicit-state model checker. SAL 2, released in December 2003 and presented as a tool paper at CAV 2004, added high-performance symbolic (BDD-based) and bounded (SAT-based) model checkers as well as a novel infinite-bounded model checker — one that uses an SMT solver to reason about systems defined over unbounded types such as integers and reals, and can prove invariants by k-induction — plus an experimental witness checker. SAL 3.0, released in December 2006, was the first open-source version; it packaged the model-checker suite together with the ICS decision procedure and, optionally, the Yices SMT solver. The Yices SMT solver, which became the workhorse decision procedure behind the infinite-bounded analysis, was itself developed at SRI in the context of the SAL effort.

Design Philosophy

SAL is unapologetically declarative. A SAL specification does not describe a sequence of imperative steps; it describes a state space and a transition relation over that space, plus the properties the system is required to satisfy.

• Systems are transition systems. The fundamental unit is a module: a self-contained description of a transition system in terms of state variables, an initialization, and transitions.
• Two complementary styles of transition. Following its influences, SAL lets you write transitions either as variable-wise next-state definitions in the style of SMV, or as guarded commands in the style of Murphi — a guard (a condition on the current state) paired with an assignment to the next state.
• Composition is first class. Modules combine through synchronous composition (the modules step together; their transition relations are conjoined) and asynchronous composition (the modules interleave; their relations are disjoined). This compositional structure mirrors the reactive modules model and lets large systems be assembled from independently understandable parts.
• Rich, mathematical types. SAL inherits much of its type language from PVS: booleans, scalar/enumeration types, subranges, integers, reals, arrays, and records, giving specifications a precise mathematical reading rather than a machine-level one.
• Properties as logic. Requirements are written in temporal logic — SAL’s model checkers target LTL (Linear Temporal Logic) — so safety and liveness obligations are stated formally alongside the system they constrain.

Key Features

The defining feature is that all of these tools read the same SAL specification. A single model can be exhaustively verified with the symbolic checker, debugged quickly with the bounded checker, scaled to infinite data types with the SMT-backed checker, explored with the simulator, and mined for tests — without rewriting it for each tool.

A Taste of the Language

A SAL specification lives in a context and is built from modules, each declaring state variables, an INITIALIZATION, and TRANSITION guarded commands. A schematic example of a small mutual-exclusion-style module looks like:

example: CONTEXT =
BEGIN
  STATE: TYPE = {idle, trying, critical};

  proc: MODULE =
  BEGIN
    LOCAL pc: STATE
    INITIALIZATION pc = idle
    TRANSITION
    [
      enter:  pc = idle    --> pc' = trying
      []
      win:    pc = trying  --> pc' = critical
      []
      leave:  pc = critical --> pc' = idle
    ]
  END;

  % A property to check: the process is never stuck outside 'idle' forever
  liveness: THEOREM proc |- G(F(pc = idle));
END

Here the guards (pc = idle) and primed next-state assignments (pc' = trying) define the transition relation, and the THEOREM states an LTL property the model checkers can verify or refute with a counterexample trace.

Evolution

SAL evolved from an academic design study into a stable, openly distributed toolkit. The trajectory ran from the explicit-state checker of SAL 1, through the symbolic, bounded, and SMT-powered infinite-bounded checkers introduced in SAL 2, to SAL 3.0, which made the whole toolkit open source. The infinite-bounded analysis was a significant step: by coupling SAL to an SMT solver and using k-induction, the toolkit could prove properties of systems with unbounded integer and real state — a class of problems beyond the reach of pure BDD- or SAT-based methods.

The project also spawned and influenced a family of related SRI tools. Yices matured into a widely used standalone SMT solver. HybridSAL extended the approach to hybrid systems by computing relational abstractions of continuous dynamics so that discrete model checkers could analyze them. Later, Sally, an infinite-state model checker, carried forward the SMT-based verification ideas that SAL had helped pioneer.

Current Relevance

SAL remains available from SRI and continues to be used in research and teaching, though its core releases date to the mid-2000s and much of SRI’s newer verification work has flowed into successor tools such as Yices and Sally. Its lasting relevance is twofold. First, it is a practical, batteries-included environment for learning and applying model checking: a single declarative language backed by multiple checkers that illustrate the trade-offs between symbolic, bounded, and SMT-based techniques. Second, it remains a useful back end for verifying systems originally written in other notations, thanks to its design as an intermediate language with a clean transition-system semantics.

Why It Matters

SAL captured an important lesson in formal verification: the bottleneck is often not any single algorithm but the integration of complementary techniques. By insisting on one well-designed declarative language as the shared substrate, SAL made it natural to apply abstraction, several flavors of model checking, and decision procedures to the same specification. The infrastructure it pioneered — particularly SMT-based and k-induction model checking — became central to modern automated verification, and the tools it incubated, above all the Yices SMT solver, went on to influence the broader field well beyond SAL itself.