442
S. Wimmer and J. von Mutius
14. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions
for timed automata. Information and Computation 251, 67–90 (2016).
https://doi.org/10.1016/j.ic.2016.07.004
15. Herbreteau, F., Point, G.: TChecker (2019), https://github.com/fredher/tchecker
16. Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In:
SPIN 2014. p. 30–39. Association for Computing Machinery, New York, NY, USA
(2014). https://doi.org/10.1145/2632362.2632372
17. Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification
of a dual chamber implantable pacemaker. In: Flanagan, C., K¨ onig, B. (eds.) TACAS
2012. pp. 188–203. Springer Berlin Heidelberg (2012). https://doi.org/10.1007/9783-642-28756-5 14
18. Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multicore emptiness checking of timed b¨ uchi automata using inclusion abstraction. In:
Sharygina, N., Veith, H. (eds.) CAV 2013. pp. 968–983. Springer Berlin Heidelberg
(2013). https://doi.org/10.1007/978-3-642-39799-8 69
19. Lammich, P.: Collections framework. Archive of Formal Proofs (Nov 2009), http:
//isa-afp.org/entries/Collections.html, Formal proof development
20. Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X.
(eds.) ITP 2015, Proceedings. LNCS, vol. 9236, pp. 253–269. Springer (2015).
https://doi.org/10.1007/978-3-319-22102-1 17
21. Launchbury, J., Peyton Jones, S.: Lazy functional state threads. PLDI 1998 29 (07
1998). https://doi.org/10.1145/178243.178246
22. M¨ oller, M.O.: Uppaal benchmarks (2017), https://www.it.uu.se/research/group/
darts/uppaal/benchmarks
23. Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.)
CAV 2001. pp. 2–13. Springer Berlin Heidelberg (2001). https://doi.org/10.1007/3540-44585-4 2
24. Neumann, R.: Using promela in a fully verified executable LTL model checker.
In: Giannakopoulou, D., Kroening, D. (eds.) Verified Software: Theories, Tools
and Experiments. pp. 105–114. Springer International Publishing, Cham (2014).
https://doi.org/10.1007/978-3-319-12154-3 7
25. Nipkow, T., Lawrence C. Paulson, Wenzel, M.: Isabelle/HOL - A Proof Assistant for
Higher-Order Logic, LNCS, vol. 2283. Springer (2002). https://doi.org/10.1007/3540-45949-9
26. Paulin-Mohring, C.: Modelisation of timed automata in Coq. In: STACS 2001. pp.
298–315. LNCS 2215 (2001). https://doi.org/10.1007/3-540-45500-0 15
27. Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan,
R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. pp. 292–304. Springer Berlin
Heidelberg (2001). https://doi.org/10.1007/3-540-45294-X 25
28. Sprenger, C.: A verified model checker for the modal μ-calculus in
Coq. In: TACAS 1998. pp. 167–183. Springer, London, UK (1998).
https://doi.org/10.1007/BFb0054171
29. Wimmer, S.: Formalized timed automata. In: Blanchette, J.C., Merz, S. (eds.) ITP
2016. LNCS, vol. 9807, pp. 425–440. Springer (2016). https://doi.org/10.1007/9783-319-43144-4 26
30. Wimmer, S.: Munta: A fully verified model checker for realtime systems. https:
//github.com/wimmers/munta (2019)
31. Wimmer, S., Lammich, P.: Verified model checking of timed automata. In:
Beyer, D., Huisman, M. (eds.) TACAS 2018. pp. 61–78. Springer, Cham (2018).
https://doi.org/10.1007/978-3-319-89960-2 4
S. Wimmer and J. von Mutius
14. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions
for timed automata. Information and Computation 251, 67–90 (2016).
https://doi.org/10.1016/j.ic.2016.07.004
15. Herbreteau, F., Point, G.: TChecker (2019), https://github.com/fredher/tchecker
16. Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In:
SPIN 2014. p. 30–39. Association for Computing Machinery, New York, NY, USA
(2014). https://doi.org/10.1145/2632362.2632372
17. Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification
of a dual chamber implantable pacemaker. In: Flanagan, C., K¨ onig, B. (eds.) TACAS
2012. pp. 188–203. Springer Berlin Heidelberg (2012). https://doi.org/10.1007/9783-642-28756-5 14
18. Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multicore emptiness checking of timed b¨ uchi automata using inclusion abstraction. In:
Sharygina, N., Veith, H. (eds.) CAV 2013. pp. 968–983. Springer Berlin Heidelberg
(2013). https://doi.org/10.1007/978-3-642-39799-8 69
19. Lammich, P.: Collections framework. Archive of Formal Proofs (Nov 2009), http:
//isa-afp.org/entries/Collections.html, Formal proof development
20. Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X.
(eds.) ITP 2015, Proceedings. LNCS, vol. 9236, pp. 253–269. Springer (2015).
https://doi.org/10.1007/978-3-319-22102-1 17
21. Launchbury, J., Peyton Jones, S.: Lazy functional state threads. PLDI 1998 29 (07
1998). https://doi.org/10.1145/178243.178246
22. M¨ oller, M.O.: Uppaal benchmarks (2017), https://www.it.uu.se/research/group/
darts/uppaal/benchmarks
23. Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.)
CAV 2001. pp. 2–13. Springer Berlin Heidelberg (2001). https://doi.org/10.1007/3540-44585-4 2
24. Neumann, R.: Using promela in a fully verified executable LTL model checker.
In: Giannakopoulou, D., Kroening, D. (eds.) Verified Software: Theories, Tools
and Experiments. pp. 105–114. Springer International Publishing, Cham (2014).
https://doi.org/10.1007/978-3-319-12154-3 7
25. Nipkow, T., Lawrence C. Paulson, Wenzel, M.: Isabelle/HOL - A Proof Assistant for
Higher-Order Logic, LNCS, vol. 2283. Springer (2002). https://doi.org/10.1007/3540-45949-9
26. Paulin-Mohring, C.: Modelisation of timed automata in Coq. In: STACS 2001. pp.
298–315. LNCS 2215 (2001). https://doi.org/10.1007/3-540-45500-0 15
27. Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan,
R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. pp. 292–304. Springer Berlin
Heidelberg (2001). https://doi.org/10.1007/3-540-45294-X 25
28. Sprenger, C.: A verified model checker for the modal μ-calculus in
Coq. In: TACAS 1998. pp. 167–183. Springer, London, UK (1998).
https://doi.org/10.1007/BFb0054171
29. Wimmer, S.: Formalized timed automata. In: Blanchette, J.C., Merz, S. (eds.) ITP
2016. LNCS, vol. 9807, pp. 425–440. Springer (2016). https://doi.org/10.1007/9783-319-43144-4 26
30. Wimmer, S.: Munta: A fully verified model checker for realtime systems. https:
//github.com/wimmers/munta (2019)
31. Wimmer, S., Lammich, P.: Verified model checking of timed automata. In:
Beyer, D., Huisman, M. (eds.) TACAS 2018. pp. 61–78. Springer, Cham (2018).
https://doi.org/10.1007/978-3-319-89960-2 4