LinAIG

 

Subproject

H3

Categories

Data structures for symbolic state representation

Overview

The LinAIG library provides a C++ API for the representation of arbitrary Boolean combinations of linear constraints and Boolean variables. Moreover, LinAIGs support several operators to manipulate or compare such formulas. It was developed for the symbolic representation of linear hybrid systems and is used within the fomc and fsmtMC model checking tools.

Publications

W. Damm, H. Dierks, S. Disch, W. Hagemann, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces. Science of Computer Programming, Special Issue on Automated Verification of Critical Systems, 2011. Accepted for publication.

F. Pigorsch and C. Scholl. Using Implications for Optimizing State Set Representations of Linear Hybrid Systems. In Carsten Gremzow and Nico Moser, editors, GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pages 77-86, 2009.

C. Scholl, S. Disch, F. Pigorsch, and S. Kupferschmid. Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints. In Stefan Kowalewski and Anna Philippou, editors, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of Lecture Notes in Computer Science (LNCS), pages 383-397, 2009.

C. Scholl, S. Disch, F. Pigorsch, and S. Kupferschmid. Using an SMT solver and Craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra. In Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pages 18-26, 2008.

W. Damm, S. Disch, H. Hungar, S. Jacobs, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Exact state set representation in the verification of linear hybrid systems with large discrete state space. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, 5th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4762 of Lecture Notes in Computer Science, pages 425-440, 2007.

W. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz. Automatic Verification of Hybrid Systems with Large Discrete State Space, In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of Lecture Notes in Computer Science, 2006.

Benchmarks

---

Download

Click here for the library.

Manual

Click here for the manual.

Status

Prototype