What is it?
LASH is a toolset for representing infinite sets and exploring infinite state spaces. It is based on finitestate representations, which rely on finitestate automata for representing and manipulating infinite sets of values over various data domains.
The current version of LASH is beta version 0.92 and consists of C libraries providing functions and datatypes for performing
the following tasks:
 Constructing and manipulating some types of finitestate automata (on finite and infinite words).
 Representing and manipulating finite and infinite sets of
values. The representation systems implemented by
LASH are
 The NDD (Number Decision Diagram), suited for sets of unbounded integer vectors. NDDs are slightly more expressive than Presburger arithmetic.
 The RVA (Real Vector Automaton), suited for sets of unbounded real and integer vectors. RVA can represent all the sets that can be defined in the firstorder combined additive theory of the reals and integers.
 The QDD (Queuecontent Decision Diagram), suited for sets of contents of unbounded FIFO queues.
 Exploring the statespace of systems composed of a finite control and of unbounded integer variables over which linear operations are performed.

Frontends for
 Compiling program models expressed in the SimplePROMELA and the SimpleIF languages, and exploring the statespace of these programs.
 Solving problems expressed in Presburger arithmetic.
 Statespace exploration tools for timed systems and hybrid systems, based on the RVA package.
 A visualization tool for sets represented by NDDs and RVA.
Where can I find it?
The C sources of the LASH toolset are available free of charge for evaluation purposes and educational use. A copy of the most recent version can be downloaded here. After downloading, please consult the installation instructions.How can I use it?
Documentation and sample programs are available for some components of the package. Additional documentation is available in the source code. Installation instructions
 Core package: [ Documentation  Examples ]
 NDD package: [ Documentation ]