19. G. Holzmann, D. Peled, and M. Yannakakis. On Nested Depth First Search. In
The Spin Verification System, volume 32 of DIMACS, pages 23–32, 1996. doi:
10.1090/dimacs/032/03.
20. B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens.
VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NFM,
2011. doi:10.1007/978-3-642-20398-5_4.
21. B. Jacobs, J. Smans, and F. Piessens. VeriFast: Imperative Programs as Proofs.
In VS-Tools workshop at VSTTE, 2010.
22. S. Joosten, W. Oortwijn, M. Safari, and M. Huisman. An Exercise in Verifying
Sequential Programs with VerCors. In FTfJP, pages 40–45, 2018. doi:10.1145/
3236454.3236479.
23. G. Kant, A. Laarman, J. Meijer, J. van de Pol, S. Blom, and T. van Dijk. LTSmin:
High-Performance Language-Independent Model Checking. In TACAS, pages 692–
707. Springer, 2015. doi:10.1007/978-3-662-46681-0_61.
24. J. K¨ ubler. Comparing Deductive Program Verification of Graph Data-Structures.
Bachelor’s thesis, KIT, 2018.
25. A. Laarman, R. Langerak, J. van de Pol, M. Weber, and A. Wijs. Multi-core
Nested Depth-First Search. In ATVA, LNCS, pages 321–335. Springer, 2011. doi:
10.1007/978-3-642-24372-1_23.
26. A. Laarman, M. Olesen, A. Dalsgaard, K. Larsen, and J. van de Pol. Multi-core
Emptiness Checking of Timed B¨ uchi Automata Using Inclusion Abstraction. In
CAV, pages 968–983. Springer, 2013. doi:10.1007/978-3-642-39799-8_69.
27. P. Lammich and R. Neumann. A Framework for Verifying Depth-First Search
Algorithms. In CPP, pages 137–146. ACM, 2015. doi:10.1145/2676724.2693165.
28. P. Lammich and S. Wimmer. IMP2 – Simple Program Verification in Isabelle/HOL.
Archive of Formal Proofs, 2019. http://isa-afp.org/entries/IMP2.html, Formal
proof development.
29. K.R.M. Leino. Data groups: Specifying the modification of extended state. In
OOPSLA, pages 144–153. ACM, 1998. doi:10.1145/286942.286953.
30. K.R.M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness.
In LPAR, pages 348–370. Springer, 2010. doi:10.1007/978-3-642-17511-4_20.
31. L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS, pages
337–340, 2008. doi:10.1007/978-3-540-78800-3_24.
32. P. M¨ uller, M. Schwerhoff, and A. Summers. Viper: A Verification Infrastructure
for Permission-Based Reasoning. In VMCAI, pages 41–62. Springer, 2016. doi:
10.1007/978-3-662-49122-5_2.
33. K. Namjoshi. Certifying Model Checkers. In CAV, LNCS, pages 2–13. Springer,
2001. doi:10.1007/3-540-44585-4_2.
34. P. O’Hearn. Resources, Concurrency and Local Reasoning. Theoretical Computer
Science, 375(1–3):271–307, 2007. doi:10.1016/j.tcs.2006.12.035.
35. W. Oortwijn, M. Huisman, S. Joosten, and J. van de Pol. Artifact for Automated
Verification of Parallel Nested DFS, TACAS 2020. 4TU.ResearchData. doi:10.
4121/uuid:36c00955-5574-44d9-9b26-340f7a1ea03b.
36. A. Pnueli. The Temporal Logic of Programs. In FOCS, pages 46–57. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.32.
37. J. van de Pol. Automated Verification of Nested DFS. In FMICS, LNCS, pages
181–197. Springer, 2015. doi:10.1007/978-3-319-19458-5_12.
38. A. Raad, A. Hobor, J. Villard, and P. Gardner. Verifying Concurrent Graph
Algorithms. In Programming Languages and Systems, pages 314–334. Springer,
2016. doi:10.1007/978-3-319-47958-3_17.
264
W. Oortwijn et al.
The Spin Verification System, volume 32 of DIMACS, pages 23–32, 1996. doi:
10.1090/dimacs/032/03.
20. B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens.
VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NFM,
2011. doi:10.1007/978-3-642-20398-5_4.
21. B. Jacobs, J. Smans, and F. Piessens. VeriFast: Imperative Programs as Proofs.
In VS-Tools workshop at VSTTE, 2010.
22. S. Joosten, W. Oortwijn, M. Safari, and M. Huisman. An Exercise in Verifying
Sequential Programs with VerCors. In FTfJP, pages 40–45, 2018. doi:10.1145/
3236454.3236479.
23. G. Kant, A. Laarman, J. Meijer, J. van de Pol, S. Blom, and T. van Dijk. LTSmin:
High-Performance Language-Independent Model Checking. In TACAS, pages 692–
707. Springer, 2015. doi:10.1007/978-3-662-46681-0_61.
24. J. K¨ ubler. Comparing Deductive Program Verification of Graph Data-Structures.
Bachelor’s thesis, KIT, 2018.
25. A. Laarman, R. Langerak, J. van de Pol, M. Weber, and A. Wijs. Multi-core
Nested Depth-First Search. In ATVA, LNCS, pages 321–335. Springer, 2011. doi:
10.1007/978-3-642-24372-1_23.
26. A. Laarman, M. Olesen, A. Dalsgaard, K. Larsen, and J. van de Pol. Multi-core
Emptiness Checking of Timed B¨ uchi Automata Using Inclusion Abstraction. In
CAV, pages 968–983. Springer, 2013. doi:10.1007/978-3-642-39799-8_69.
27. P. Lammich and R. Neumann. A Framework for Verifying Depth-First Search
Algorithms. In CPP, pages 137–146. ACM, 2015. doi:10.1145/2676724.2693165.
28. P. Lammich and S. Wimmer. IMP2 – Simple Program Verification in Isabelle/HOL.
Archive of Formal Proofs, 2019. http://isa-afp.org/entries/IMP2.html, Formal
proof development.
29. K.R.M. Leino. Data groups: Specifying the modification of extended state. In
OOPSLA, pages 144–153. ACM, 1998. doi:10.1145/286942.286953.
30. K.R.M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness.
In LPAR, pages 348–370. Springer, 2010. doi:10.1007/978-3-642-17511-4_20.
31. L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS, pages
337–340, 2008. doi:10.1007/978-3-540-78800-3_24.
32. P. M¨ uller, M. Schwerhoff, and A. Summers. Viper: A Verification Infrastructure
for Permission-Based Reasoning. In VMCAI, pages 41–62. Springer, 2016. doi:
10.1007/978-3-662-49122-5_2.
33. K. Namjoshi. Certifying Model Checkers. In CAV, LNCS, pages 2–13. Springer,
2001. doi:10.1007/3-540-44585-4_2.
34. P. O’Hearn. Resources, Concurrency and Local Reasoning. Theoretical Computer
Science, 375(1–3):271–307, 2007. doi:10.1016/j.tcs.2006.12.035.
35. W. Oortwijn, M. Huisman, S. Joosten, and J. van de Pol. Artifact for Automated
Verification of Parallel Nested DFS, TACAS 2020. 4TU.ResearchData. doi:10.
4121/uuid:36c00955-5574-44d9-9b26-340f7a1ea03b.
36. A. Pnueli. The Temporal Logic of Programs. In FOCS, pages 46–57. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.32.
37. J. van de Pol. Automated Verification of Nested DFS. In FMICS, LNCS, pages
181–197. Springer, 2015. doi:10.1007/978-3-319-19458-5_12.
38. A. Raad, A. Hobor, J. Villard, and P. Gardner. Verifying Concurrent Graph
Algorithms. In Programming Languages and Systems, pages 314–334. Springer,
2016. doi:10.1007/978-3-319-47958-3_17.
264
W. Oortwijn et al.