Automated Verification of Parallel Nested DFS
265
39. J. Reif. Depth-First Search is Inherently Sequential. Information Processing Letters, 20(5):229–234, 1985. doi:10.1016/0020-0190(85)90024-9.
40. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Variations on Parallel
Explicit Emptiness Checks for Generalized B¨ uchi Automata. STTT, 19(6):653–
673, 2017. doi:10.1007/s10009-016-0422-5.
41. S. Schwoon and J. Esparza.
A Note on On-the-Fly Verification Algorithms. In TACAS, LNCS, pages 174–190. Springer, 2005. doi:10.1007/
978-3-540-31980-1_12.
42. I. Sergey, A. Nanevski, and A. Banerjee. Mechanized Verification of Fine-Grained
Concurrent Programs. In PLDI, pages 77–87. ACM, 2015. doi:10.1145/2813885.
2737964.
43. C. Sprenger. A Verified Model Checker for the Modal μ-calculus in Coq. In TACAS,
LNCS, pages 167–183. Springer, 1998. doi:10.1007/bfb0054171.
44. V. Vafeiadis. Concurrent Separation Logic and Operational Semantics. In MFPS,
ENTCS, pages 335–351, 2011. doi:10.1016/j.entcs.2011.09.029.
45. M. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of
Programs. Journal of Computer and System Sciences, 32(2):183–221, 1986. doi:
10.1016/0022-0000(86)90026-7.
46. Why3 gallery of formally verified programs. http://toccata.lri.fr/gallery/graph.en.
html (accessed on February 2020).
47. S. Wimmer and P. Lammich. Verified Model Checking of Timed Automata. In
TACAS, LNCS, pages 61–78. Springer, 2018. doi:10.1007/978-3-319-89960-2_4.
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.
265
39. J. Reif. Depth-First Search is Inherently Sequential. Information Processing Letters, 20(5):229–234, 1985. doi:10.1016/0020-0190(85)90024-9.
40. E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud. Variations on Parallel
Explicit Emptiness Checks for Generalized B¨ uchi Automata. STTT, 19(6):653–
673, 2017. doi:10.1007/s10009-016-0422-5.
41. S. Schwoon and J. Esparza.
A Note on On-the-Fly Verification Algorithms. In TACAS, LNCS, pages 174–190. Springer, 2005. doi:10.1007/
978-3-540-31980-1_12.
42. I. Sergey, A. Nanevski, and A. Banerjee. Mechanized Verification of Fine-Grained
Concurrent Programs. In PLDI, pages 77–87. ACM, 2015. doi:10.1145/2813885.
2737964.
43. C. Sprenger. A Verified Model Checker for the Modal μ-calculus in Coq. In TACAS,
LNCS, pages 167–183. Springer, 1998. doi:10.1007/bfb0054171.
44. V. Vafeiadis. Concurrent Separation Logic and Operational Semantics. In MFPS,
ENTCS, pages 335–351, 2011. doi:10.1016/j.entcs.2011.09.029.
45. M. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of
Programs. Journal of Computer and System Sciences, 32(2):183–221, 1986. doi:
10.1016/0022-0000(86)90026-7.
46. Why3 gallery of formally verified programs. http://toccata.lri.fr/gallery/graph.en.
html (accessed on February 2020).
47. S. Wimmer and P. Lammich. Verified Model Checking of Timed Automata. In
TACAS, LNCS, pages 61–78. Springer, 2018. doi:10.1007/978-3-319-89960-2_4.
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.