{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:40:07Z","timestamp":1737063607287,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001416"},{"type":"electronic","value":"9783540361350"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36135-9_17","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:43:21Z","timestamp":1180665801000},"page":"260-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["C Wolf - A Toolset for Extracting Models from C Programs"],"prefix":"10.1007","author":[{"given":"Daniel C.","family":"Du Varney","sequence":"first","affiliation":[]},{"given":"S.","family":"Purushothaman Iyer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram Rajamani. Automatic predicate abstraction of c programs. In Proceedings of the ACM SIGPLAN 2001 Conference of Programming Language Design and Implementation (PLDI 2001). ACM Press, June 2001.","DOI":"10.1145\/378795.378846"},{"key":"17_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45420-9","volume-title":"Automatically validating temporal safety properties of interfaces","author":"T. Ball","year":"2001","unstructured":"Thomas Ball and Sriram K. Rajamani. Automatically validating temporal safety properties of interfaces. In The 8th International SPIN Workshop on Model Checking of Software (SPIN 2001), volume 2057 of LNCS, pages 103\u2013122, New York-Berlin-Heidelberg, May 2001. Springer-Verlag."},{"key":"17_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45420-9","volume-title":"The slam toolkit","author":"T. Ball","year":"2001","unstructured":"Thomas Ball and Sriram K. Rajamani. The slam toolkit. In 13th Conference on Computer Aided Verification (CAV\u2019 01), volume 2102 of LNCS, New York-Berlin-Heidelberg, July 2001. Springer-Verlag."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Rachid Echahed, and Peter Habermehl. Verifying in.nite state processes with sequential and parallel composition. In Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201995), pages 95\u2013106, San Francisco, California, January 22\u201325, 1995. ACM Press.","DOI":"10.1145\/199448.199470"},{"key":"17_CR5","unstructured":"Guillaume Brat, Klaus Havelund, SeungJoon Park, and William Visser. Java pathfinder: Second generation of a java modelc hecker, July 2000."},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming (ICALP\u2019 97)","author":"O. Burkart","year":"1997","unstructured":"O. Burkart and B. Steffen. Model-checking the full-modal mu-calculus for infinite sequentialpro cesses. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Automata, Languages and Programming (ICALP\u2019 97), volume 1256 of Lecture Notes in Computer Science, pages 419\u2013429, Bologna, Italy, July 1997. Springer-Verlag. Full version to appear in Theoretical Computer science."},{"issue":"11","key":"17_CR7","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1145\/356989.356995","volume":"35","author":"A. Chou","year":"2000","unstructured":"Andy Chou, Benjamin Chelf, Dawson Engler, and Mark Heinrich. Using meta-level compilation to check FLASH protocol code. ACM SIGPLAN Notices, 35(11):59\u201370, November 2000.","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"17_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporall ogic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke and J. M. Wing. Formal methods: state of the art and future directio ns. ACM Computing Surveys, 28(4):626\u2013643, December 1996.","journal-title":"ACM Computing Surveys"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"James Corbett, Matthew Dwyer, John Hatcli., Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: extracting.nite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439\u2013448, Limerick, Ireland, June 2000. IEEE Computer Society.","DOI":"10.1145\/337180.337234"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth ACM Symposium on Principles of Programming Languages, pages 238\u2013252, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"C.R. Ramakrishnan, I.V. Ramakrishnan, S. A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V.N. Venkatakrishnan. XMC: A logic-programming-based verification toolset. In Computer Aided Verification (CAV 2000), Chicago, Illinois, June 2000.","DOI":"10.1007\/10722167_48"},{"issue":"7","key":"17_CR13","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"Claudio Demartini, Radu Iosif, and Riccardo Sisto. A deadlock detection tool for concurrent java programs. Software: Practice and Experience, 29(7):577\u2013603, June 1999.","journal-title":"Software: Practice and Experience"},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/3-540-49059-0_6","volume-title":"Fighting livelock in the i-protocol: A comparative study of verification tools","author":"Y. Dong","year":"1999","unstructured":"Yifei Dong, Xiaoqun Du, Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, Eugene W. Stark, and David Scott Warren. Fighting livelock in the i-protocol: A comparative study of verification tools. In Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99), volume 1579 of Lecture Notes in Computer science, pages 74\u201388. Springer-Verlag, 1999."},{"key":"17_CR15","unstructured":"Daniel C. Du Varney. Abstraction-Based Generation of Finite State Models from C Programs. PhD thesis, North Carolina State University, 2002."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"M. B. Dwyer, J. Hatcli., R. Joehanes, S. Laubach, Robby, C. S. Pasareanu, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of the 23rd International Conference on Software Engineering (ICSE-01), pages 177\u2013187, Los Alamitos, California, May 12\u201319 2001. IEEE Computer Society.","DOI":"10.1109\/ICSE.2001.919092"},{"key":"17_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-61474-5_93","volume-title":"Symbolic modelc hecking","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke, K. L. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic modelc hecking. In Proceedings of the Eighth International Conference on Computer Aided Veri.cation CAV, volume 1102 of Lecture Notes in Computer Science, pages 419\u2013422. Springer Verlag, July\/August 1996."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In 4th Symposium on Operating System Design and Implementation, Berkeley, CA, October 2000. USENIX Association.","DOI":"10.21236\/ADA419626"},{"key":"17_CR19","series-title":"Lect Notes Comput Sci","first-page":"266","volume-title":"Graph Drawing","author":"M. Fr\u00f6hlich","year":"1994","unstructured":"M. Fr\u00f6hlich and M. Werner. Demonstration of the interactive graph-visualization system davinci. In R. Tamassia and I. G. Tollis, editors, Graph Drawing, volume 894 of Lecture Notes in Computer Science, pages 266\u2013269. DIMACS, Springer-Verlag, October 1994. ISBN 3-540-58950-3."},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid. Modelc hecking for programming languages using VeriSoft. In The 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), pages 174\u2013186, Paris, France, 1997. ACM SIGACT and SIGPLAN, ACM Press.","DOI":"10.1145\/263699.263717"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid, Bob Hanmer, and Lalita Jagadeesan. Model checking without a model: An analysis of the heart-beat monitor of a telephone switch using verisoft. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA\u2019 98), pages 124\u2013133, Clearwater Beach, FL, March 1998. ACM Press.","DOI":"10.1145\/271771.271800"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid, Bob Hanmer, and Lalita Jagadeesan. Systematic software testing using verisoft: An analysis of the 4ess heart-beat monitor. Bell Labs Technical Journal, 3(2), April-June 1998.","DOI":"10.1002\/bltj.2103"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4), april1998.","DOI":"10.1007\/s100090050043"},{"key":"17_CR24","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cli.s, New Jersey, 1991."},{"key":"17_CR25","series-title":"Lect Notes Comput Sci","volume-title":"The engineering of a modelc hecker: the gnu i-protocolcase study revisited","author":"G. J. Holzmann","year":"1999","unstructured":"Gerard J. Holzmann. The engineering of a modelc hecker: the gnu i-protocolcase study revisited. In Proceedings of the 6th Spin Workshop, volume 1680 of LNCS, Toulouse, France, Sept. 1999. Springer Verlag."},{"key":"17_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Logic verification of ANSI-C code with SPIN","author":"G. J. Holzmann","year":"2000","unstructured":"Gerard J. Holzmann. Logic verification of ANSI-C code with SPIN. In Proceedings of the 7th International SPIN Workshop, volume 1885 of LNCS. Springer-Verlag, September 2000."},{"issue":"2","key":"17_CR27","first-page":"481","volume":"11","author":"G.J. Holzmann","year":"2001","unstructured":"G.J. Holzmann and Margaret H. Smith. Software model checking-extracting verification models from source code. In Formal Methods for Protocol Engineering and Distributed Systems, pages 481\u2013497, Kluwer Academic Publ., Oct. 1999. also in: Software Testing, Veri.cation and Reliability, Vol. 11, No. 2, June 2001, pp. 65\u201379.","journal-title":"Formal Methods for Protocol Engineering and Distributed Systems"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Radu Iosif. Formalv erification applied to java concurrent software. In Proceedings of the 22nd International Conference on Software Engineering, pages 707\u2013709, June 2000.","DOI":"10.1145\/337180.337594"},{"key":"17_CR29","unstructured":"Eleftherios Koutsofios. Drawing graphs with dot. Technicalrep ort, AT&T Bell Laboratories, Murray Hill, NJ, USA, November 1996. This report, and the program, is included in the graphviz package, available for non-commercial use at URL http:\/\/www.research.att.com\/sw\/tools\/graphviz\/ ."},{"key":"17_CR30","unstructured":"David Ladd, Satish Chandra, Michael Siff, Nevin Heintze, Dino Oliva, and Dave MacQueen. Ckit: A front end for c in sml, March 2000. Available from URL http:\/\/cm.bell-labs.com\/cm\/cs\/what\/smlnj\/doc\/ckit\/index.html ."},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"David Lie, Andy Chou, Dawson Engler, and David L. Dill. A simple method for extracting models from protocol code. In Proceedings of the 28th Annual International Symposium on Computer Architecture, pages 192\u2013203, G\u00f6teborg, Sweden, June 30-July 4, 2001. IEEE Computer Society and ACM SIGARCH.","DOI":"10.1145\/384285.379263"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"17_CR33","unstructured":"R. Milner. Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, 1989."},{"key":"17_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"The NCSU concurrency workbench","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland and S. Sims. The NCSU concurrency workbench. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Veri.cation CAV, volume 1102 of Lecture Notes in Computer Science, pages 394\u2013397, New Brunswick, NJ, USA, July\/August 1996. Springer Verlag."},{"key":"17_CR35","unstructured":"G. Sander. Vcg-visualization of compiler graphs. Technical Report A01-95, Universit\u00e4t des Saarlande, FB 14 Informatik, 1995."},{"key":"17_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/10722468_14","volume-title":"Model checking multi-threaded distributed java programs","author":"S. Stoller","year":"2000","unstructured":"Scott Stoller. Model checking multi-threaded distributed java programs. In Proceedings of the 7th International SPIN Workshop, volume 1885 of LNCS, pages 224\u2013244. Springer-Verlag, 2000."},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"William Visser, Kluas Havelund, Guillaume Brat, and SeungJoon Park. Model checking programs. In P Alexander and Pierre Flener, editors, Proceedings of ASE-2000: The 15th IEEE Conference on Automated Software Engineering, Grenoble, France, September 2000. IEEE Computer Society Press.","DOI":"10.1109\/ASE.2000.873645"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"David Wagner and Drew Dean. Intrusion detection via static analysis. In Francis M. Titsworth, editor, Proceedings of the 2001 IEEE Symposium on Security and Privacy (S&P-01), pages 156\u2013169, Los Alamitos, CA, May 14\u201316 2001. IEEE Computer Society.","DOI":"10.1109\/SECPRI.2001.924296"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36135-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:00:00Z","timestamp":1737061200000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36135-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001416","9783540361350"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-36135-9_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"5 November 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}