References

  1. Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani & Bengt Jonsson (2004): Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design 25(1), pp. 39–65, doi:10.1023/B:FORM.0000033962.51898.1a.
  2. Kyungmin Bae & Sicun Gao (2017): Modular smt-based analysis of nonlinear hybrid systems. In: 2017 Formal Methods in Computer Aided Design (FMCAD). IEEE, pp. 180–187, doi:10.23919/FMCAD.2017.8102258.
  3. Stanley Bak, Sergiy Bogomolov & Taylor T. Johnson (2015): HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models. In: Proc. of the 18th Intl. Conf. on Hybrid Systems: Computation and Control (HSCC). ACM, doi:10.1145/2728606.2728630.
  4. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017): The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.
  5. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds & Cesare Tinelli (2011): CVC4. In: Ganesh Gopalakrishnan & Shaz Qadeer: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science 6806. Springer, pp. 171–177, doi:10.1007/978-3-642-22110-1_14.
  6. Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson & Wang Yi (1996): UPPAAL: A tool suite for automatic verification of real-time systems. In: Rajeev Alur, Thomas Henzinger & Eduardo Sontag: Hybrid Systems III, LNCS 1066. Springer, pp. 232–243, doi:10.1007/BFb0020949.
  7. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri & Stefano Tonetta (2014): The nuXmv Symbolic Model Checker. In: Armin Biere & Roderick Bloem: Computer Aided Verification, Lecture Notes in Computer Science 8559. Springer International Publishing, pp. 334–342, doi:10.1007/978-3-319-08867-9_22.
  8. Xin Chen, Erika Abraham & Sriram Sankaranarayanan (2013): Flow*: An Analyzer for Non-linear Hybrid Systems. In: Natasha Sharygina & Helmut Veith: Computer Aided Verification, Lecture Notes in Computer Science 8044. Springer Berlin Heidelberg, pp. 258–263, doi:10.1007/978-3-642-39799-8_18.
  9. Alessandro Cimatti, Alberto Griggio, Sergio Mover & Stefano Tonetta (2015): HyComp: An SMT-Based Model Checker for Hybrid Systems. In: Christel Baier & Cesare Tinelli: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 9035. Springer Berlin Heidelberg, pp. 52–67, doi:10.1007/978-3-662-46681-0_4.
  10. Alessandro Cimatti, Alberto Griggio, Sergio Mover & Stefano Tonetta (2015): HyComp: An SMT-Based Model Checker for Hybrid Systems. In: Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp. 52–67, doi:10.1007/978-3-662-46681-0_4.
  11. Alessandro Cimatti, Sergio Mover & Stefano Tonetta (2013): SMT-based scenario verification for hybrid systems. Formal Methods in System Design 42(1), pp. 46–66, doi:10.1007/s10703-012-0158-0.
  12. Leonardo De Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08/ETAPS '08. Springer-Verlag, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  13. Andreas Eggers, Martin Fränzle & Christian Herde (2008): SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems. In: Sungdeok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee & Mahesh Viswanathan: Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 5311. Springer Berlin / Heidelberg, pp. 171–185, doi:10.1007/978-3-540-88387-6_14.
  14. Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang & Oded Maler (2011): SpaceEx: Scalable Verification of Hybrid Systems. In: Computer Aided Verification (CAV), LNCS. Springer, doi:10.1007/978-3-642-22110-1_30.
  15. Sicun Gao, J. Avigad & E.M. Clarke (2012): Delta-Decidability over the Reals. In: Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on, pp. 305–314, doi:10.1109/LICS.2012.41.
  16. Sicun Gao, Soonho Kong & Edmund Clarke (2013): Satisfiability Modulo ODEs. In: International Conference on Formal Methods in Computer-Aided Design (FMCAD), doi:10.1109/FMCAD.2008.ECP.14.
  17. Sicun Gao, Soonho Kong & Edmund M Clarke (2013): dReal: An SMT solver for nonlinear theories over the reals. In: Automated Deduction–CADE-24. Springer, pp. 208–214, doi:10.1007/978-3-642-38574-2_14.
  18. Silvio Ghilardi & Silvio Ranise (2010): MCMT: A Model Checker Modulo Theories.. In: IJCAR 10. Springer, pp. 22–29, doi:10.1007/978-3-642-14203-1_3.
  19. T. A. Henzinger (1996): The theory of hybrid automata. In: IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Washington, DC, USA, pp. 278, doi:10.1109/LICS.1996.561342.
  20. Thomas A. Henzinger, Pei-Hsin Ho & Howard Wong-Toi (1997): HyTech: A model checker for hybrid systems. Journal on Software Tools for Technology Transfer 1, pp. 110–122, doi:10.1007/s100090050008.
  21. Mikoláš Janota, William Klieber, Joao Marques-Silva & Edmund Clarke (2012): Solving QBF with counterexample guided refinement. In: Theory and Applications of Satisfiability Testing–SAT 2012. Springer, pp. 114–128, doi:10.1007/978-3-642-31612-8_10.
  22. Taylor T. Johnson & Sayan Mitra (2012): A Small Model Theorem for Rectangular Hybrid Automata Networks. In: Proceedings of the IFIP International Conference on Formal Techniques for Distributed Systems, Joint 14th Formal Methods for Open Object-Based Distributed Systems and 32nd Formal Techniques for Networked and Distributed Systems (FMOODS-FORTE), LNCS 7273. Springer, doi:10.1007/978-3-642-30793-5_2.
  23. Taylor T. Johnson & Sayan Mitra (2013): Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems. In: Proceedings of the AIAA Infotech at Aerospace Conference (AIAA Infotech 2013), Boston, MA, doi:10.2514/6.2013-4811.
  24. Taylor T. Johnson & Sayan Mitra (2014): Anonymized Reachability of Rectangular Hybrid Automata Networks. In: Formal Modeling and Analysis of Timed Systems (FORMATS), doi:10.1007/978-3-319-10512-3_10.
  25. Toni Jussila & Armin Biere (2007): Compressing BMC encodings with QBF. Electronic Notes in Theoretical Computer Science 174(3), pp. 45–56, doi:10.1016/j.entcs.2006.12.022.
  26. Soonho Kong, Sicun Gao, Wei Chen & Edmund Clarke (2015): dReach: Delta-reachability analysis for hybrid systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp. 200–205, doi:10.1007/978-3-662-46681-0_15.
  27. Nancy Lynch & Nir Shavit (1992): Timing-based mutual exclusion. In: Real-Time Systems Symposium, 1992. IEEE, pp. 2–11, doi:10.1109/REAL.1992.242681.
  28. H. Mangassarian, A. Veneris & M. Benedetti (2010): Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test. Computers, IEEE Transactions on 59(7), pp. 981–994, doi:10.1109/TC.2010.74.
  29. C. Miller, K. Gitina & B. Becker (2011): Bounded Model Checking of Incomplete Real-time Systems Using Quantified SMT Formulas. In: Microprocessor Test and Verification (MTV), 2011 12th International Workshop on, pp. 22–27, doi:10.1109/MTV.2011.13.
  30. Fedor Shmarov, Nicola Paoletti, Ezio Bartocci, Shan Lin, Scott A Smolka & Paolo Zuliani (2017): SMT-based synthesis of safe and robust PID controllers for stochastic hybrid systems. In: Haifa Verification Conference. Springer, pp. 131–146, doi:10.1007/978-3-319-70389-3_9.
  31. Ashish Tiwari (2012): HybridSAL Relational Abstracter. In: P. Madhusudan & SanjitA. Seshia: Computer Aided Verification, Lecture Notes in Computer Science 7358. Springer Berlin Heidelberg, pp. 725–731, doi:10.1007/978-3-642-31424-7_56.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org