What is it?

LASH is a toolset for representing infinite sets and exploring infinite state spaces. It is based on finite-state representations, which rely on finite-state automata for representing and manipulating infinite sets of values over various data domains.

The current version of LASH is beta version 0.9 and consists of

• C libraries providing functions and datatypes for performing the following tasks:
  • Constructing and manipulating some types of finite-state 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 first-order combined additive theory of the reals and integers.
    • The QDD (Queue-content Decision Diagram), suited for sets of contents of unbounded FIFO queues.
  • Exploring the state-space of systems composed of a finite control and of unbounded integer variables over which linear operations are performed.
• Front-ends for
  • Compiling program models expressed in the Simple-PROMELA and the Simple-IF languages, and exploring the state-space of these programs.
  • Solving problems expressed in Presburger arithmetic.

The following features are under development and will soon become part of the toolset:

• State-space exploration tools for timed systems and hybrid systems, based on the RVA package.
• A visualization tool for sets represented by NDDs and RVA.

The LASH toolset is currently maintained by Bernard Boigelot, Louis Latour and Sébastien Jodogne.

Past or occasional contributors include Gérard Cécé, Jean-Marc François and Yves Bontemps.

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. The toolset documentation can be found in the next section.

How can I use it?

Documentation and sample programs are available - or will be available soon - for the main components of the package:

• Installation instructions
• Core package: [ Documentation | Examples ]
• NDD package: [ Documentation | Examples ]
• RVA package: [ Documentation | Examples ]
• QDD package: [ Documentation | Examples ]
• State-space exploration package: [ Documentation | Examples ]
• Simple-IF compiler: [ Documentation | Examples ]
• Simple-PROMELA compiler: [ Documentation | Examples ]
• Presburger solver: [ Documentation | Examples ]

References

The techniques and algorithms implemented in LASH are described in the following papers.

• General:

  • P. Wolper and B. Boigelot. Verifying Systems with Infinite but Regular State Spaces. Proc. 10th International Conference on Computer-Aided Verification, volume 1427, Lecture Notes in Computer Science, pages 88-97, Vancouver, June 1998, Springer-Verlag.

  • B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD Thesis, volume 189, Collection des Publications de la Faculté des Sciences Appliquées de l'Université de Liège, 300 pages, 1999.

  • B. Boigelot and P. Wolper. Representing Arithmetic Constraints with Automata: An Overview. To appear in Proc. ICLP 2002.

  • B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets. Proc. 6th International Conference on Computer-Aided Verification, volume 818, Lecture Notes in Computer Science, pages 55-67, Stanford, June 1994, Springer-Verlag.

• NDDs:

  • P. Wolper and B. Boigelot. An Automata-Theoretic Approach to Presburger Arithmetic Constraints. Proc. 2nd Static Analysis Symposium, volume 983, Lecture Notes in Computer Science, pages 21-32, Glasgow, September 1995, Springer-Verlag.

  • B. Boigelot and L. Latour. Counting the Solutions of Presburger Equations without Enumerating Them. To appear in Proc. International Conference on Implementations and Applications of Automata, Lecture Notes in Computer Science, Pretoria, July 2001, Springer-Verlag.

• QDDs:

  • B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs, Formal Methods in System Design, volume 14, pages 237-255, 1999, Kluwer Academic Publishers.

  • B. Boigelot, P. Godefroid, B. Willems and P. Wolper. The Power of QDDs. Proc. 4th Static Analysis Symposium, volume 1302, Lecture Notes in Computer Science, pages 172-186, Paris, September 1997, Springer-Verlag.

  • B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. Proc. 8th International Conference on Computer-Aided Verification, volume 1102, Lecture Notes in Computer Science, pages 1-12, New-Brunswick, July 1996, Springer-Verlag.

• RVA:

  • B. Boigelot, S. Jodogne and P. Wolper. On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. Proc. International Joint Conference on Automated Reasoning, volume 2083, Lecture Notes in Artificial Intelligence, pages 611-625, Siena, June 2001, Springer-Verlag.

  • B. Boigelot, L. Bronne and S. Rassart. An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems. Proc. 9th International Conference on Computer-Aided Verification, volume 1254, Lecture Notes in Computer Science, pages 167-177, Haifa, June 1997, Springer-Verlag.

  • B. Boigelot, S. Rassart and P. Wolper. On the Expressiveness of Real and Integer Arithmetic Automata. Proc. 25th International Colloquium on Automata, Languages and Programming, volume 1443, Lecture Notes in Computer Science, pages 152-163, Aalborg, July 1998, Springer-Verlag.

Feedback

Questions, suggestions and bug reports are welcome. Please send your feedback to Bernard Boigelot.

[ What is it? | Where can I find it? | How can I use it? | Feedback ]