HySAT: An efficient proof engine for bounded model checking of hybrid systems

1. Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Generic ILP versus specialized 0–1 ILP: An update. In: Proceedings of the ACM/IEEE International Conference Computer-Aided Design (ICCAD), pp 450–457

2. Audemard G, Bertoli P, Cimatti A, Kornilowics A, Sebastiani R (2002) A SAT-based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov A (ed) Proceedings of the 18th International Conference on Automated Deduction, vol 2392. Lecture Notes in Artificial Intelligence. Springer-Verlag, pp 193–208

3. Audemard G, Bozzano M, Cimatti A, Sebastiani R (2004) Verifying industrial hybrid systems with MathSAT. ENTCS 89(4)

4. Baptista L, Lynce I, Marques-Silva J (2001) Complete search restart strategies for satisfiability. In: Proceedings of the IJCAI′01 workshop on stochastic search algorithms (IJCAI-SSA)

5. Barrett C, Dill D, Stump A (2002) Checking satisfiability of first-order formulas by incremental translation to SAT. In: Proceedings of the 14th international conference on computer-aided verification

6. Barth P (1995) A Davis-Putnam based enumeration algorithm for linear pseudo-boolean optimization. Technical Report MPI-I-95-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany

7. Bemporad A, Morari M (1999) Verification of hybrid systems via mathematical programming. In: Vaandrager FW, van Schuppen JH (eds) Hybrid systems: Computation and control (HSCC′99), vol 1569. Lecture Notes in Computer Science, Springer-Verlag, pp 31–45

8. Biere A, Cimatti A, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS′99, vol 1579. Lecture Notes in Computer Science, Springer-Verlag

9. Bik A, Wijshoff H (1994) Implementation of Fourier-Motzkin elimination. Technical Report TR94-42, Dpt. of Computer Sceince, University of Leiden, The Netherlands

10. Chai D, Kuehlmann A (2003) A fast pseudo-boolean constraint solver. In: Proceedings of the 40th Design Automation Conference (DAC 2003). ACM, Anaheim, California, USA, pp 830–835

    Chapter  Google Scholar 

11. Chinneck JW (1997) Finding a useful subset of constraints for analysis in an infeasible linear program. INFORMS J Comput 9(2):164–174

    Article  MATH  MathSciNet  Google Scholar 

12. Chinneck JW, Dravnieks EW (1991) Locating minimal infeasible constraint sets in linear programs. ORSA J Comput 3(2):157–168

    MATH  Google Scholar 

13. Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. Commun ACM 5:394–397

    Article  MATH  MathSciNet  Google Scholar 

14. de Moura L, Owre S, Ruess H, Rushby J, Shankar N (2004) The ICS decision procedures for embedded deduction. In: Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR), vol 3097. Lecture Notes in Computer Science. Springer-Verlag, Cork, Ireland, pp 218–222

    Google Scholar 

15. de Moura L, Owre S, Rueß H, Rushby J, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Alur R, Peled D (eds) Computer-aided verification, CAV 2004, vol 3114. Lecture Notes in Computer Science. Springer-Verlag, Boston, MA, pp 496–500

    Google Scholar 

16. de Moura L, Rueß H, Sorea M (2002) Lazy theorem proving for bounded model checking over infinite domains. In: Proceedings of the 18th international conference on automated deduction, vol 2392. Lecture Notes in Computer Science. Springer-Verlag, pp 438–455

17. Enslev J, Nielsen A-S, Fränzle M, Hansen MR (2005) Bounded model construction for duration calculus. In: Jones N, et al (eds) Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05). Københavns Universitet

18. Fourier J (1826) Solution dùne qestion particulière du calcul des inégalités. Nouveau Bulletin par la Société Philomathique des Paris pp 99–100

19. Fränzle M, Herde C (2003) Efficient SAT engines for concise logics: Accelerating proof search for zero-one linear constraint systems. In: Vardi M, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning (LPAR 2003), vol 2850. Lecture Notes in Artificial Intelligence, Springer-Verlag

20. Fränzle M, Herde C (2003) Efficient SAT engines for concise logics: Accelerating proof search for zero-one linear constraint systems. In: Moshe AV, Vardi Y (eds) Logic for programming, artificial intelligence and reasoning (LPAR 2003), vol 2850. LNCS, subseries LNAI, Springer Verlag, pp 302–316

21. Gleeson J, Ryan J (1990) Identifying minimally infeasible subsystems of inequalities. ORSA J Comput 2(1):61–63

    MATH  Google Scholar 

22. Groote JF, Koorn JWC, van Vlijmen SFM (1995) The safety guaranteeing system at station hoorn-kersenboogerd. In: Compass ′95: 10th annual conference on computer assurance. National Institute of Standards and Technology, Gaithersburg, Maryland, pp 57–68

    Google Scholar 

23. Hehner ECR (1984) Predicative programming. Commun ACM 27:134–151

    Article  MATH  MathSciNet  Google Scholar 

24. Henzinger TA, Ho P-H, Wong-Toi H (1995) HyTech: The next generation. In: Proceedings of the 16th Annual IEEE Real-time Systems Symposium (RTSS 1995). IEEE Computer Society Press, pp 56–65

25. Henzinger TA, Kopke PW, Puri A, Varaiya P (1995) what's decidable about hybrid automata. In: Proceedings of the 27th Annual ACM symposium on the theory of computing. ACM, pp 373–382

26. Jin H, Somenzi F (2004) An incremental algorithm to check satisfiability for bounded model checking. In: Biere A, Strichman O (eds) Preliminary proceeding of BMC′04, ETH Zürich

27. Marques-Silva JP (1999) The impact of branching heuristics in propositional satisfiability algorithms. In: Proceedings of the 9th Portuguese Conference on Artificial Intelligence (EPIA).

28. Marques-Silva JP, Sakallah KA (1999) GRASP: A search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506–521

    Article  MathSciNet  Google Scholar 

29. Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC′01).

30. Motzkin TS (1936) Beiträge zur Theorie der linearen Ungleichungen. Doctoral dissertation, Universität Zürich

31. Nonnengart A, Weidenbach C (1999) Computing small clause normal forms. In: Robinson A, Voronkov A (eds) Handbook of automated reasoning, Elsevier Science B.V

32. Pfetsch ME (2002) The maximum feasible subsystem problem and vertex-facet incidences of polyhedra. Doctoral dissertation, TU Berlin

33. Ratschan S (2002) Continuous first-order constraint satisfaction with equality and d isequality constraints. In: van Hentenryck P (ed) Proceedings of the 8th international conference on principles and practice of constraint programming, vol 2470. Lecture Notes in Computer Science, Springer, pp 680–685

34. Strichman O (2000) Tuning SAT checkers for bounded model checking. In: Emerson EA, Sistla AP (eds) Computer aided verification (CAV 2000), vol 1855. Lecture Notes in Computer Science, Springer-Verlag, pp 480–494

35. Torrisi FD (2003) Modeling and reach-set computation for analysis and optimal control of discrete hybrid automata. Doctoral dissertation, ETH Zürich

36. Tseitin G (1968) On the complexity of derivations in propositional calculus. In: Slisenko A (ed) Studies in constructive mathematics and mathematical logics

37. Warners JP (1998) A linear-time transformation of linear inequalities into conjunctive normal form. Inf Process Lett 68(2):63–69

    Article  MathSciNet  Google Scholar 

38. Whittemore J, Kim J, Sakallah K (2001) SATIRE: A new incremental satisfiability engine. In: Proceedings of the Design Automation Conference (DAC 2001). Las Vegas, Nevada, USA, pp 542–545

39. Wolfman SA, Weld DS (1999) The LPSAT engine & its application to resource planning. In: Dean T (ed) Proceeding of the 16th International Joint Conference on i Artificial Intelligence. Morgan Kaufmann Publishers, pp 310–315

40. Zhang L, Madigan CF, Moskewicz MW, Malik S (2001) Efficient conflict driven learning in a Boolean satisfiability solver. In: Proceeding of the International Conference on Computer-Aided Design (ICCAD′01), pp 279–285

Download references