Simplics is a recent successor of the Integrated Solver and Canonizer (ICS). However, unlike ICS, Simplics is specialized for a more narrow set of problems. It is a tool for deciding the validity of boolean combination of linear-arithmetic constraints over the reals. The main intended application of Simplics is bounded model-checking of infinite transition systems including several forms of timed transition systems. Examples of applications include distributed real-time fault-tolerant systems and clock synchrnozation protocols.
Simplics got the first place in the QF_LRA (linear real arithmetic) division in SMT-COMP'05.
Last modified: