Verified Certification of Reachability Checking for Timed Automata
441
Data Availability Statement
The datasets generated and/or analyzed during the current study are available in
the Zenodo repository [32]: https://doi.org/10.5281/zenodo.3679245. The artifact
has been tested on the TACAS artifact evaluation VM [12].
References
1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science
126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
2. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed
automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. pp. 254–270.
Springer Berlin Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X 18
3. Behrmann, G., Bouyer, P., Larsen, K.G., Pel´ anek, R.: Lower and upper
bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. pp. 312–326. Springer Berlin Heidelberg (2004).
https://doi.org/10.1007/978-3-540-24730-2 25
4. Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In:
Lectures on Concurrency and Petri Nets: Advances in Petri Nets. LNCS, vol. 3908,
pp. 87–124. Springer (2004). https://doi.org/10.1007/978-3-540-27755-2 3
5. Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: FSE 2016. p.
326–337. Association for Computing Machinery, New York, NY, USA (2016).
https://doi.org/10.1145/2950290.2950351
6. Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker
with partial order reduction. Journal of Automated Reasoning 60(1), 3–21 (2018).
https://doi.org/10.1007/s10817-017-9418-4
7. Bulwahn, L., Krauss, A., Haftmann, F., Erk¨ ok, L., Matthews, J.: Imperative
functional programming with Isabelle/HOL. In: Theorem Proving in Higher Order
Logics (TPHOLs 2008). pp. 134–149 (2008). https://doi.org/10.1007/978-3-54071067-7 14
8. Cast´ eran, P., Rouillard, D.: Towards a generic tool for reasoning about labeled
transition systems. In: TPHOLs 2001: Supplemental Proceedings (2001)
9. Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A
fully verified executable LTL model checker. In: CAV 2013. LNCS, vol. 8044, pp.
463–478. Springer (2013)
10. Garnacho, M., Bodeveix, J., Filali-Amine, M.: A mechanized semantic framework for real-time systems. In: FORMATS 2013. pp. 106–120. LNCS 8053 (2013).
https://doi.org/10.1007/978-3-642-40229-6 8
11. Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. 2018 Formal Methods in Computer Aided Design (FMCAD) pp. 1–9 (2018).
https://doi.org/10.23919/FMCAD.2018.8603022
12. Hartmanns,
A.,
Seidl,
M.:
tacas20ae.ova
(Aug
2019).
https://doi.org/10.6084/m9.figshare.9699839.v2, https://figshare.com/articles/
tacas20ae ova/9699839/2
13. Herbreteau, F., Srivathsan, B., Tran, T.T., Walukiewicz, I.: Why liveness for timed
automata is hard, and what we can do about it. In: Lal, A., Akshay, S., Saurabh,
S., Sen, S. (eds.) FSTTCS 2016. LIPIcs, vol. 65, pp. 48:1–48:14. Schloss Dagstuhl
(2016). https://doi.org/10.4230/LIPIcs.FSTTCS.2016.48
441
Data Availability Statement
The datasets generated and/or analyzed during the current study are available in
the Zenodo repository [32]: https://doi.org/10.5281/zenodo.3679245. The artifact
has been tested on the TACAS artifact evaluation VM [12].
References
1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science
126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
2. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed
automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. pp. 254–270.
Springer Berlin Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X 18
3. Behrmann, G., Bouyer, P., Larsen, K.G., Pel´ anek, R.: Lower and upper
bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. pp. 312–326. Springer Berlin Heidelberg (2004).
https://doi.org/10.1007/978-3-540-24730-2 25
4. Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In:
Lectures on Concurrency and Petri Nets: Advances in Petri Nets. LNCS, vol. 3908,
pp. 87–124. Springer (2004). https://doi.org/10.1007/978-3-540-27755-2 3
5. Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: FSE 2016. p.
326–337. Association for Computing Machinery, New York, NY, USA (2016).
https://doi.org/10.1145/2950290.2950351
6. Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker
with partial order reduction. Journal of Automated Reasoning 60(1), 3–21 (2018).
https://doi.org/10.1007/s10817-017-9418-4
7. Bulwahn, L., Krauss, A., Haftmann, F., Erk¨ ok, L., Matthews, J.: Imperative
functional programming with Isabelle/HOL. In: Theorem Proving in Higher Order
Logics (TPHOLs 2008). pp. 134–149 (2008). https://doi.org/10.1007/978-3-54071067-7 14
8. Cast´ eran, P., Rouillard, D.: Towards a generic tool for reasoning about labeled
transition systems. In: TPHOLs 2001: Supplemental Proceedings (2001)
9. Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A
fully verified executable LTL model checker. In: CAV 2013. LNCS, vol. 8044, pp.
463–478. Springer (2013)
10. Garnacho, M., Bodeveix, J., Filali-Amine, M.: A mechanized semantic framework for real-time systems. In: FORMATS 2013. pp. 106–120. LNCS 8053 (2013).
https://doi.org/10.1007/978-3-642-40229-6 8
11. Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. 2018 Formal Methods in Computer Aided Design (FMCAD) pp. 1–9 (2018).
https://doi.org/10.23919/FMCAD.2018.8603022
12. Hartmanns,
A.,
Seidl,
M.:
tacas20ae.ova
(Aug
2019).
https://doi.org/10.6084/m9.figshare.9699839.v2, https://figshare.com/articles/
tacas20ae ova/9699839/2
13. Herbreteau, F., Srivathsan, B., Tran, T.T., Walukiewicz, I.: Why liveness for timed
automata is hard, and what we can do about it. In: Lal, A., Akshay, S., Saurabh,
S., Sen, S. (eds.) FSTTCS 2016. LIPIcs, vol. 65, pp. 48:1–48:14. Schloss Dagstuhl
(2016). https://doi.org/10.4230/LIPIcs.FSTTCS.2016.48