ABsolver - Arithmetic and Boolean solver and ABcircuit - Arithmetic and Boolean circuit library. Our framework provides a single engine to possibly solve all mixed arithmetic and Boolean problems using standard tools, such as zChaff or COIN. Even though the primary intend was to tackle linear arithmetic, the extensible architecture proved useful as we added non-linear solvers as well and are thus able to solve a set of mixed Boolean and non-linear problems too, which, to the best of our knowledge, no other tool is capable of. Furthermore a layered design approach makes it easy to add new solvers and thus new problem domains, and will also help new programmers joining in. The command line interface allows for customization of the background solvers, whereby heuristics are supported which should help to solve even very hard problems.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Navarro-López, E. M.; O’Toole, M. D.: Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties (2018)
- Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
- Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
- Corzilius, Florian; Ábrahám, Erika: Virtual substitution for SMT-solving (2011)
- Eggers, Andreas; Kruglov, Evgeny; Kupferschmid, Stefan; Scheibler, Karsten; Teige, Tino; Weidenbach, Christoph: Superposition modulo non-linear arithmetic (2011)
- Loup, Ulrich; Ábrahám, Erika: I-RiSC: an SMT-compliant solver for the existential fragment of real algebra (2011)
- Teige, Tino; Eggers, Andreas; Fränzle, Martin: Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems (2011)
- Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael: Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers (2010) ioport
- Fränzle, Martin; Teige, Tino; Eggers, Andreas: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata (2010)
- Eggers, Andreas; Kalinnik, Natalia; Kupferschmid, Stefan; Teige, Tino: Challenges in constraint-based analysis of hybrid systems (2009)
- Fränzle, Martin; Herde, Christian; Teige, Tino; Ratschan, Stefan; Schubert, Tobias: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure (2006)