{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:26:51Z","timestamp":1743110811061,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319194578"},{"type":"electronic","value":"9783319194585"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19458-5_12","type":"book-chapter","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T11:41:14Z","timestamp":1431344474000},"page":"181-197","source":"Crossref","is-referenced-by-count":5,"title":["Automated Verification of Nested DFS"],"prefix":"10.1007","author":[{"given":"Jaco C.","family":"van de Pol","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"12_CR1","first-page":"1","volume":"4","author":"D. Beyer","year":"2014","unstructured":"Beyer, D., Huisman, M., Klebanov, V., Monahan, R.: Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171). Dagstuhl Reports\u00a04(4), 1\u201319 (2014)","journal-title":"Dagstuhl Reports"},{"issue":"2\/3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design\u00a01(2\/3), 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 463\u2013478. Springer, Heidelberg (2013)"},{"key":"12_CR5","unstructured":"Gaiser, A., Schwoon, S.: Comparison of Algorithms for Checking Emptiness on B\u00fcchi Automata. CoRR, abs\/0910.3766 (2009)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-38613-8_9","volume-title":"Integrated Formal Methods","author":"F. Gava","year":"2013","unstructured":"Gava, F., Fortin, J., Guedj, M.: Deductive verification of state-space algorithms. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 124\u2013138. Springer, Heidelberg (2013)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: The Spin Verification System, pp. 23\u201332. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-24372-1_23","volume-title":"Automated Technology for Verification and Analysis","author":"A.W. Laarman","year":"2011","unstructured":"Laarman, A.W., Langerak, R., van de Pol, J.C., Weber, M., Wijs, A.: Multi-Core Nested Depth-First Search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 321\u2013335. Springer, Heidelberg (2011)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-08970-6_21","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2014","unstructured":"Lammich, P.: Verified efficient implementation of Gabow\u2019s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol.\u00a08558, pp. 325\u2013340. Springer, Heidelberg (2014)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"12_CR11","unstructured":"Pottier, F.: Depth-first search and strong connectivity in Coq. Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2015) (January 2015)"},{"key":"12_CR12","unstructured":"Ray, S., Matthews, J., Tuttle, M.: Certifying compositional model checking algorithms in ACL2. In: IW on ACL2 Theorem Prover and its Applications (2003)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Schwoon","year":"2005","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 174\u2013190. Springer, Heidelberg (2005)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Sprenger, C.: A verified model checker for the modal \u03bc-calculus in Coq. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 167\u2013183. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0054171"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-642-16901-4_34","volume-title":"Formal Methods and Software Engineering","author":"J. Sun","year":"2010","unstructured":"Sun, J., Liu, Y., Cheng, B.: Model checking a model checker: A code contract combined approach. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 518\u2013533. Springer, Heidelberg (2010)"},{"key":"12_CR16","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332\u2013344. Cambridge (1986)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19458-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T09:05:01Z","timestamp":1676451901000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19458-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319194578","9783319194585"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19458-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}