basic data structures and core algorithms
| MiraXT multi-threaded SAT solver |
| Mira-Craig library for generation of Craig interpolants |
| incQuBE incremental QBF solver |
| QMiraXT multi-threaded QBF solver |
| PaQuBE parallel QBF solver |
| Quaig combined QBF solver (AIGsolve and QuBE) |
| LIRA decision procedures for first-order logics with linear arithmetic over the integers and the reals |
verification
| CIP Bounded Model Checker for discrete systems |
| mbmc Bounded Model Checker for discrete systems |
| bounce Bounded Model Checker for incomplete discrete systems |
| sigref symbolic minimization of finite labeled transition systems |
| lter long-term expected rewards |
| bb Model Checker for incomplete probabilistic systems |
| (S)SBMC counterexample generation for probabilistic systems |
| timemachine Bounded Model Checker for incomplete timed systems |
| iSAT SMT solver for non-linear arithmetic |
| iSAT-Craig Bounded Model Checker for hybrid systems |
test
| TIGUAN TSI SAT-based test pattern generator |
| PARSIM parallel fault simulation |
| TAMSIN highly accurate delay-fault simulation |
| PHAETON SAT-based tool for the enumeration of sensitisable paths |
smartenergy
| SmartMeter a versatile electricity meter for the future connected home |
| FIRED A Fully-labeled hIgh-fRequency Electricity Disaggregation Dataset |
| Annoticity |
| FLANdERS a Fully Labeled AppliaNce ElectRicity dataSet |
