Core algorithms, Model checker / solver for hybrid systems


iSAT-ODE is a solver for arithmetic constraint systems containing ordinary differential equations. The solver targets formulae that arise from the predicative encoding of bounded model checking properties of hybrid discrete-continuous systems whose continuous dynamics can be described by ODEs.


A. Eggers, N. Ramdani, N.S. Nedialkov, and M. Fränzle. Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In 9th International Conference on Software Engineering and Formal Methods (SEFM), LNCS, 2011. To appear. M. Fränzle, T. Teige, and A. Eggers. Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. Journal of Logic and Algebraic Programming, 79:436-466, 2010. A. Eggers, M. Fränzle, and C. Herde. Application of constraint solving and ODE-enclosure methods to the analysis of hybrid systems. In Theodore E. Simos, George Psihoyios, and Ch. Tsitouras, editors, NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on Numerical Analysis and Applied Mathematics 2009, volume 1168 of American Institue of Physics (AIP) Conference Proceedings, pages 1326-1330, 2009. A. Eggers, M. Fränzle, and C. Herde. SAT modulo ODE: A direct SAT approach to hybrid systems. In Sungdeok (Steve) Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan, editors, Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), volume 5311 of Lecture Notes in Computer Science (LNCS), pages 171-185, 2008.


Two Tank System


Click here for binary & manual.


(see above)