{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T19:39:33Z","timestamp":1730317173022,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[1998,3]]},"DOI":"10.1145\/271771.271800","type":"proceedings-article","created":{"date-parts":[[2004,2,3]],"date-time":"2004-02-03T17:41:00Z","timestamp":1075830060000},"page":"124-133","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Model checking without a model"],"prefix":"10.1145","author":[{"given":"Patrice","family":"Godefroid","sequence":"first","affiliation":[{"name":"Bell Laboratories, Lucent Technologies, 1000 E. Warrenville Road, Naperville, IL"}]},{"given":"Robert S.","family":"Hanmer","sequence":"additional","affiliation":[{"name":"Lucent Technologies, 2000 N. Naperville Road, Naperville, IL"}]},{"given":"Lalita Jategaonkar","family":"Jagadeesan","sequence":"additional","affiliation":[{"name":"Bell Laboratories, Lucent Technologies, 1000 E. Warrenville Road, Naperville, IL"}]}],"member":"320","published-online":{"date-parts":[[1998,3]]},"reference":[{"key":"e_1_3_2_1_1_2","first-page":"549","volume-title":"F. Keeve, and K. Nicodemus. Fault-Tolerant Telecommunication System Patterns","author":"Adams M.","year":"1996","unstructured":"M. Adams , J. Coplien , R. Gamoke , tL Hanmer , F. Keeve, and K. Nicodemus. Fault-Tolerant Telecommunication System Patterns . In Vlissidesi Coplien, and Kerth, editors, , Pattern Languages of Program Design - 2, pages 549 - 562 . Addison-Wesley , 1996 . M. Adams, J. Coplien, R. Gamoke, tL Hanmer, F. Keeve, and K. Nicodemus. Fault-Tolerant Telecommunication System Patterns. In Vlissidesi Coplien, and Kerth, editors, , Pattern Languages of Program Design - 2, pages 549-562. Addison-Wesley, 1996."},{"key":"e_1_3_2_1_2_2","first-page":"1177","article-title":"Recognizing safeiy and liveness","volume":"2","author":"Alpern B.","year":"1987","unstructured":"B. Alpern and F. B. Schneider . ' Recognizing safeiy and liveness . Distribut~ Computing , 2 : 1177 - 1126 , 1987 . B. Alpern and F. B. Schneider. 'Recognizing safeiy and liveness. Distribut~ Computing, 2:1177-126, 1987.","journal-title":"Distribut~ Computing"},{"volume-title":"Compilers: Principles, Techniques and Tools","year":"1986","author":"A.","key":"e_1_3_2_1_3_2","unstructured":"A. ,Aho, R. Sethl , and J. Ullman . Compilers: Principles, Techniques and Tools . Addison- Wesley , 1986 . A. ,Aho, R. Sethl, and J. Ullman. Compilers: Principles, Techniques and Tools. Addison- Wesley, 1986."},{"key":"e_1_3_2_1_4_2","series-title":"Lecture Notes in Computer Science","first-page":"321","volume-title":"Proceedings of the Third International Woi'kshop on Tools and Algorithms for the Construction and Analysis ofSystems (TA GAS'97)","author":"Godefroid P.","year":"1997","unstructured":"B'. 'Boigelot and P. Godefroid . Automat{c Synthesis of SpecifiCations from the Dynamic Observation of Reactive Programs . In Proceedings of the Third International Woi'kshop on Tools and Algorithms for the Construction and Analysis ofSystems (TA GAS'97) , volume 1217 of Lecture Notes in Computer Science , pages 321 - 333 , Twente, April 1997 . Springer-Verlag . B'. 'Boigelot and P. Godefroid. Automat{c Synthesis of SpecifiCations from the Dynamic Observation of Reactive Programs. In Proceedings of the Third International Woi'kshop on Tools and Algorithms for the Construction and Analysis ofSystems (TA GAS'97), volume 1217 of Lecture Notes in Computer Science, pages 321-333, Twente, April 1997. Springer-Verlag."},{"key":"e_1_3_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115324"},{"key":"e_1_3_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/229000.226323"},{"key":"e_1_3_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"key":"e_1_3_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/229000.226302"},{"key":"e_1_3_2_1_11_2","first-page":"522","volume-title":"1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors","author":"Drexler D. L.","year":"1992","unstructured":"D. L. Dilll A. J. Drexler , A. J. Hu , and C. H. Yang . Protocol verification as a hardware design aid . In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors , pages 522 - 525 , Cambridge, MA , October 1992 . IEEE Computer Society. D. L. Dilll A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522-525, Cambridge, MA, October 1992. IEEE Computer Society."},{"key":"e_1_3_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/195274.195401"},{"key":"e_1_3_2_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/143062.143124"},{"volume-title":"Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Ezplosion Problem","year":"1996","series-title":"Lecture Notes in Computer Science","key":"e_1_3_2_1_14_2","unstructured":"Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Ezplosion Problem , volume 1032 of Lecture Notes in Computer Science . Springer-Verlag , January 1996 . Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Ezplosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996."},{"key":"e_1_3_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"volume-title":"Software for ana~ lyrical development of communication protocols. AT~4T Technical Journal","year":"1990","author":"Kurshan Z.","key":"e_1_3_2_1_16_2","unstructured":"Z. Her'S1 and R. P. Kurshan . Software for ana~ lyrical development of communication protocols. AT~4T Technical Journal , 1990 . Z. Her'S1 and R. P. Kurshan. Software for ana~ lyrical development of communication protocols. AT~4T Technical Journal, 1990."},{"volume-title":"Design and Validation of Computer Protocols","year":"1991","author":"Holzmann G.","key":"e_1_3_2_1_17_2","unstructured":"G. 3. Holzmann . Design and Validation of Computer Protocols . Prentice Hall , 1991 . G. 3. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"e_1_3_2_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/253228.253435"},{"key":"e_1_3_2_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/120807.120810"},{"key":"e_1_3_2_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318622"},{"key":"e_1_3_2_1_21_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan K.L.","year":"1993","unstructured":"K.L. McMillan . Symbolic Model Checking . Kluwer Academic Publishers , 1993 . K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993."},{"volume-title":"Program Flow Analysis: Theory and Applications","year":"1981","author":"Muchnick S.S.","key":"e_1_3_2_1_22_2","unstructured":"S.S. Muchnick and N.D. Jones . Program Flow Analysis: Theory and Applications . Prentice- Hall , 1981 . S.S. Muchnick and N.D. Jones. Program Flow Analysis: Theory and Applications. Prentice- Hall, 1981."},{"key":"e_1_3_2_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/155332.155346"},{"key":"e_1_3_2_1_24_2","series-title":"Lecture Notes in Computer Science","first-page":"337","volume-title":"Proc. 5th Int'l Syrup. on Programming","author":"P.","year":"1981","unstructured":"J. P. q uielle and J. Sifakis. Specification and veriflcation of concurrent systems in CESAR . In Proc. 5th Int'l Syrup. on Programming , volume 137 of Lecture Notes in Computer Science , pages 337 - 351 . Springer-Verlag , 1981 . J.P. q uielle and J. Sifakis. Specification and veriflcation of concurrent systems in CESAR. In Proc. 5th Int'l Syrup. on Programming, volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer-Verlag, 1981."},{"key":"e_1_3_2_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/186258.187158"},{"key":"e_1_3_2_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/69586.69587"},{"key":"e_1_3_2_1_27_2","first-page":"322","volume-title":"Proceedings of the First Symposium on Logic in Computer Science","author":"Vardi M.Y.","year":"1986","unstructured":"M.Y. Vardi and P. Wolper . An automatatheoretic approach to automafAc program verification . In Proceedings of the First Symposium on Logic in Computer Science , pages 322 - 331 , Cambridge , June 1986 . M.Y. Vardi and P. Wolper. An automatatheoretic approach to automafAc program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986."}],"event":{"name":"ISSTA98: International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Clearwater Beach Florida USA","acronym":"ISSTA98"},"container-title":["Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/271771.271800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T19:54:58Z","timestamp":1693857298000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/271771.271800"}},"subtitle":["an analysis of the heart-beat monitor of a telephone switch using VeriSoft"],"short-title":[],"issued":{"date-parts":[[1998,3]]},"references-count":27,"alternative-id":["10.1145\/271771.271800","10.1145\/271771"],"URL":"https:\/\/doi.org\/10.1145\/271771.271800","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/271775.271800","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[1998,3]]},"assertion":[{"value":"1998-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}