Research

[ LASH | Publications | Conferences | Links | Main page ]

The LASH toolset

The Liège Automata-based Symbolic Handler (LASH) is a toolset for representing infinite sets and exploring infinite state spaces. Its beta version can be downloaded from the LASH page.

Publications

Thesis

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.

Conference Papers

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.
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 P. Godefroid. Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN. Proc. 3rd Symposium on Formal Methods Europe, volume 1051, Lecture Notes in Computer Science, pages 465-478, Oxford, March 1996, 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.
B. Boigelot and P. Godefroid. Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs. Proc. 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1217, Lecture Notes in Computer Science, pages 312-333, Enschede, April 1997, 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, 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. A full version of this paper is also available.
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, 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.
P. Wolper and B. Boigelot. On the Construction of Automata from Linear Arithmetic Constraints. Proc. Tools and Algorithms for the Construction and Analysis of Systems, volume 1785, Lecture Notes in Computer Science, pages 1-19, Berlin, March 2000, Springer-Verlag.
B. Boigelot, S. Jodogne and P. Wolper. On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. Proc. 1st International Joint Conference on Automated Reasoning, volume 2083, Lecture Notes in Artificial Intelligence, pages 611-625, Siena, June 2001, Springer-Verlag.
B. Boigelot and L. Latour. Counting the Solutions of Presburger Equations without Enumerating Them. Proc. 6th International Conference on Implementations and Applications of Automata (Revised Papers), volume 2494, Lecture Notes in Computer Science, pages 40-51, Pretoria, July 2001, Springer-Verlag.
B. Boigelot and P. Wolper. Representing Arithmetic Constraints with Automata: An Overview. Proc. Proc. 18th International Conference on Logic Programming, volume 2401, Lecture Notes in Computer Science, pages 1-19, Copenhagen, July 2002, Springer-Verlag.
B. Boigelot, A. Legay P. Wolper. Iterating Transducers in the Large. Proc. 15th International Conference on Computer-Aided Verification, volume 2725, Lecture Notes in Computer Science, pages 223-235, Boulder, July 2003, Springer-Verlag.
B. Boigelot, F. Herbreteau S. Jodogne. Hybrid Acceleration using Real Vector Automata. Proc. 15th International Conference on Computer-Aided Verification, volume 2725, Lecture Notes in Computer Science, pages 193-205, Boulder, July 2003, Springer-Verlag.
B. Boigelot, A. Legay P. Wolper. Omega-regular Model Checking. Proc. 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2988, Lecture Notes in Computer Science, pages 561-575, Barcelona, March 2004, Springer-Verlag.
B. Boigelot. Number-Set Representations for Infinite-State Verification. Proc. 1st NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security" (VISSAS 2005), NATO Security through Science Series D: Information and Communication Security 1, IOS Press, pages 1-16, Timisoara, March 2005.
B. Boigelot and F. Herbreteau. The Power of Hybrid Acceleration. Proc. 18th International Conference on Computer-Aided Verification, volume 4144, Lecture Notes in Computer Science, pages 438-451, Seattle, August 2006, Springer-Verlag.
B. Boigelot and J. Brusten. A Generalization of Cobham's Theorem to Automata over Real Numbers. Proc. 34th International Colloquium on Automata, Languages and Programming, volume 4596, Lecture Notes in Computer Science, pages 813-824, Wroclaw, July 2007, Springer-Verlag.
B. Boigelot, J. Brusten and V. Bruyère. On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases. Proc. 35th International Colloquium on Automata, Languages and Programming, volume 5126, Lecture Notes in Computer Science, pages 112-123, Reykjavik, July 2008, Springer-Verlag.
B. Boigelot and J.-F. Degbomont. Partial Projection of Sets Represented by Finite Automata, with Application to State-Space Visualization. To appear in Proc. 3rd International Conference on Language and Automata Theory and Applications.

Journal Papers

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. On Iterating Linear Transformations over Recognizable Sets of Integers. Theoretical Computer Science, volume 309, number 2, pages 413-468, 2003, Elsevier.
B. Boigelot and L. Latour. Counting the Solutions of Presburger Equations without Enumerating Them, 2003. Theoretical Computer Science, volume 313, pages 17-29, 2004, Elsevier.
B. Boigelot, S. Jodogne, and P. Wolper. An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables. ACM Transactions in Computational Logic, 6(3): 614-633, 2005.
B. Boigelot and J. Brusten. A Generalization of Cobham's Theorem to Automata over Real Numbers. Theoretical Computer Science, in press, 2009.

Patents

B. Boigelot and P. Godefroid. Protocol Verification using Symbolic Representation of Queues. United States Patent 5,768,498. Filed in January 1996, issued in June 1998.
P. Godefroid and B. Boigelot. Simulation of a Process of a Concurrent System. United States Patent 5,937,181. Filed in April 1997, issued in August 1999.

Conferences

List of conferences maintained by Torben Mogensen.