References

  1. Parosh Aziz Abdulla, Johann Deneux & Pritha Mahata (2004): Multi-Clock Timed Networks. In: LICS. IEEE Computer Society, pp. 345–354, doi:10.1109/LICS.2004.1319629.
  2. Parosh Aziz Abdulla & Bengt Jonsson (2003): Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1), pp. 241–264, doi:10.1016/S0304-3975(01)00330-9.
  3. Gourinath Banda & John P. Gallagher (2008): Analysis of Linear Hybrid Systems in CLP. In: Michael Hanus: LOPSTR, Lecture Notes in Computer Science 5438. Springer, pp. 55–70, doi:10.1007/978-3-642-00515-2_5.
  4. Saddek Bensalem, Marius Bozga, Joseph Sifakis & Thanh-Hung Nguyen (2008): Compositional Verification for Component-Based Systems and Application. In: Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee & Mahesh Viswanathan: ATVA, Lecture Notes in Computer Science 5311. Springer, pp. 64–79, doi:10.1007/978-3-540-88387-6_7.
  5. Nikolaj Bjørner, Kenneth L. McMillan & Andrey Rybalchenko (2013): On Solving Universally Quantified Horn Clauses. In: Francesco Logozzo & Manuel Fähndrich: SAS, Lecture Notes in Computer Science 7935. Springer, pp. 105–125, doi:10.1007/978-3-642-38856-9_8.
  6. Alessandro Carioni, Silvio Ghilardi & Silvio Ranise (2010): MCMT in the Land of Parametrized Timed Automata. In: Markus Aderhold, Serge Autexier & Heiko Mantel: VERIFY@IJCAR, EPiC Series 3. EasyChair, pp. 47–64.
  7. William Craig (1957): Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem. The Journal of Symbolic Logic 22(3), pp. 250–268, doi:10.2307/2963593.
  8. Arnaud Fietzke & Christoph Weidenbach (2012): Superposition as a Decision Procedure for Timed Automata. Mathematics in Computer Science 6(4), pp. 409–425, doi:10.1007/s11786-012-0134-5.
  9. Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti & Valerio Senni (2013): Generalization strategies for the verification of infinite state systems. TPLP 13(2), pp. 175–199, doi:10.1017/S1471068411000627.
  10. Cormac Flanagan & Shaz Qadeer (2003): Thread-Modular Model Checking. In: Thomas Ball & Sriram K. Rajamani: SPIN, Lecture Notes in Computer Science 2648. Springer, pp. 213–224, doi:10.1007/3-540-44829-2_14.
  11. Susanne Graf & Hassen Saïdi (1997): Construction of Abstract State Graphs with PVS. In: Orna Grumberg: CAV, Lecture Notes in Computer Science 1254. Springer, pp. 72–83, doi:10.1007/3-540-63166-6_10.
  12. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing software verifiers from proof rules. In: Jan Vitek, Haibo Lin & Frank Tip: PLDI. ACM, pp. 405–416, doi:10.1145/2254064.2254112.
  13. Ashutosh Gupta, Corneliu Popeea & Andrey Rybalchenko (2011): Predicate abstraction and refinement for verifying multi-threaded programs. In: Thomas Ball & Mooly Sagiv: POPL. ACM, pp. 331–344, doi:10.1145/1926385.1926424.
  14. Gopal Gupta & Enrico Pontelli (1997): A constraint-based approach for specification and verification of real-time systems. In: RTSS. IEEE Computer Society, pp. 230–239, doi:10.1109/REAL.1997.641285.
  15. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar & Kenneth L. McMillan (2004): Abstractions from proofs. In: Neil D. Jones & Xavier Leroy: POPL. ACM, pp. 232–244, doi:10.1145/964001.964021.
  16. Krystof Hoder & Nikolaj Bjørner (2012): Generalized Property Directed Reachability. In: Alessandro Cimatti & Roberto Sebastiani: SAT, Lecture Notes in Computer Science 7317. Springer, pp. 157–171, doi:10.1007/978-3-642-31612-8_13.
  17. Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak & Philipp Rümmer (2012): A Verification Toolkit for Numerical Transition Systems - Tool Paper. In: Dimitra Giannakopoulou & Dominique Méry: FM, Lecture Notes in Computer Science 7436. Springer, pp. 247–251, doi:10.1007/978-3-642-32759-9_21.
  18. Joxan Jaffar, Andrew E. Santosa & Razvan Voicu (2004): A CLP Proof Method for Timed Automata. In: RTSS. IEEE Computer Society, pp. 175–186, doi:10.1109/REAL.2004.5.
  19. Roland Kindermann, Tommi A. Junttila & Ilkka Niemelä (2012): SMT-Based Induction Methods for Timed Systems. In: Marcin Jurdzinski & Dejan Nickovic: FORMATS, Lecture Notes in Computer Science 7595. Springer, pp. 171–187, doi:10.1007/978-3-642-33365-1_13.
  20. Kim Guldstrand Larsen, Paul Pettersson & Wang Yi (1997): UPPAAL in a Nutshell. STTT 1(1-2), pp. 134–152, doi:10.1007/s100090050010.
  21. Mario Méndez-Lojo, Jorge A. Navas & Manuel V. Hermenegildo (2007): A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In: Andy King: LOPSTR, Lecture Notes in Computer Science 4915. Springer, pp. 154–168, doi:10.1007/978-3-540-78769-3_11.
  22. Susan S. Owicki & David Gries (1976): An Axiomatic Proof Technique for Parallel Programs I. Acta Inf. 6, pp. 319–340, doi:10.1007/BF00268134.
  23. Philipp Rümmer, Hossein Hojjat & Viktor Kuncak (2013): Disjunctive Interpolants for Horn-Clause Verification. In: Natasha Sharygina & Helmut Veith: CAV, Lecture Notes in Computer Science 8044. Springer, pp. 347–363, doi:10.1007/978-3-642-39799-8_24.
  24. Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez & Bor-Yuh Evan Chang (2012): Invariant Generation for Parametrized Systems Using Self-reflection - (Extended Version). In: Antoine Miné & David Schmidt: SAS, Lecture Notes in Computer Science 7460. Springer, pp. 146–163, doi:10.1007/978-3-642-33125-1_12.
  25. Tawhid Bin Waez, Jürgen Dingel & Karen Rudie (2013): A survey of timed automata for the development of real-time systems. Computer Science Review 9, pp. 1–26, doi:10.1016/j.cosrev.2013.05.001.
  26. Wang Yi, Paul Pettersson & Mats Daniels (1994): Automatic verification of real-time communicating systems by constraint-solving. In: Dieter Hogrefe & Stefan Leue: FORTE, IFIP Conference Proceedings 6. Chapman & Hall, pp. 243–258.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org