{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:20Z","timestamp":1784837780417,"version":"3.55.0"},"reference-count":233,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,10,1]],"date-time":"2009-10-01T00:00:00Z","timestamp":1254355200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CCF-0546170CCF-0702743CNS-0720881"],"award-info":[{"award-number":["CCF-0546170CCF-0702743CNS-0720881"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0546170CCF-0702743CNS-0720881"],"award-info":[{"award-number":["CCF-0546170CCF-0702743CNS-0720881"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2009,10]]},"abstract":"<jats:p>We survey recent progress in software model checking.<\/jats:p>","DOI":"10.1145\/1592434.1592438","type":"journal-article","created":{"date-parts":[[2009,10,8]],"date-time":"2009-10-08T17:31:08Z","timestamp":1255023068000},"page":"1-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":293,"title":["Software model checking"],"prefix":"10.1145","volume":"41","author":[{"given":"Ranjit","family":"Jhala","sequence":"first","affiliation":[{"name":"University of California, San Diego, La Jolla, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"University of California, Los Angeles, Los Angeles, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_2_1_3_1","volume-title":"Tech. Rep. 83","author":"Agerwala T.","year":"1978","unstructured":"Agerwala , T. and Misra , J . 1978 . Assertion graphs for verifying and synthesizing programs. Tech. Rep. 83 , University of Texas , Austin, TX . Agerwala, T. and Misra, J. 1978. Assertion graphs for verifying and synthesizing programs. Tech. Rep. 83, University of Texas, Austin, TX."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.026"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Mocha: Modularity in model checking. In CAV 98: Computer-Aided Verification","author":"Alur R.","year":"1998","unstructured":"Alur , R. , Henzinger , T. , Mang , F. , Qadeer , S. , Rajamani , S. , and Tasiran , S . 1998 . Mocha: Modularity in model checking. In CAV 98: Computer-Aided Verification . Lecture Notes in Computer Science , vol. 1427 . Springer-Verlag , Berlin, Germany , 521--525. Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., and Tasiran, S. 1998. Mocha: Modularity in model checking. In CAV 98: Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 521--525."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1059"},{"key":"e_1_2_1_10_1","volume-title":"-R","author":"Apt K.","year":"1991","unstructured":"Apt , K. and Olderog , E . -R . 1991 . Verification of Sequential and Concurrent Programs. Springer-Verlag , Berlin, Germany. Apt, K. and Olderog, E.-R. 1991. Verification of Sequential and Concurrent Programs. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368118"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_3"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217943"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057391"},{"key":"e_1_2_1_18_1","volume-title":"TACAS 01: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"2031","author":"Ball T.","unstructured":"Ball , T. , Podelski , A. , and Rajamani , S. K . 2001. Boolean and Cartesian abstractions for model checking C programs . In TACAS 01: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 2031 . Springer-Verlag, New York, 268--283. Ball, T., Podelski, A., and Rajamani, S. K. 2001. Boolean and Cartesian abstractions for model checking C programs. In TACAS 01: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer-Verlag, New York, 268--283."},{"key":"e_1_2_1_19_1","volume-title":"TACAS 02: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"2280","author":"Ball T.","unstructured":"Ball , T. , Podelski , A. , and Rajamani , S. K . 2002. Relative completeness of abstraction refinement for software model checking . In TACAS 02: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 2280 . Springer-Verlag, New York, 158--172. Ball, T., Podelski, A., and Rajamani, S. K. 2002. Relative completeness of abstraction refinement for software model checking. In TACAS 02: Proceedings of the Symposium on Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2280. Springer-Verlag, New York, 158--172."},{"key":"e_1_2_1_20_1","volume-title":"Tech. Rep. MSR-TR-2002-09, Microsoft Research.","author":"Ball T.","year":"2002","unstructured":"Ball , T. and Rajamani , S . 2002 a. Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09, Microsoft Research. Ball, T. and Rajamani, S. 2002a. Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09, Microsoft Research."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Computer Science","volume-title":"Bebop: A symbolic model checker for Boolean programs. In SPIN 00: Proceedings of the SPIN Workshop","author":"Ball T.","year":"2000","unstructured":"Ball , T. and Rajamani , S. K . 2000 a. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: Proceedings of the SPIN Workshop . Lecture Notes in Computer Science 1885. Springer-Verlag , 113--130. Ball, T. and Rajamani, S. K. 2000a. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: Proceedings of the SPIN Workshop. Lecture Notes in Computer Science 1885. Springer-Verlag, 113--130."},{"key":"e_1_2_1_23_1","volume-title":"Tech. Rep. MSR Technical Report 2000-14, Microsoft Research.","author":"Ball T.","year":"2000","unstructured":"Ball , T. and Rajamani , S. K . 2000 b. Boolean programs: a model and process for software analysis. Tech. Rep. MSR Technical Report 2000-14, Microsoft Research. Ball, T. and Rajamani, S. K. 2000b. Boolean programs: a model and process for software analysis. Tech. Rep. MSR Technical Report 2000-14, Microsoft Research."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"e_1_2_1_25_1","volume-title":"ICSE 04: Proceedings of the International Conference on Software Engineering. ACM","author":"Beyer D.","unstructured":"Beyer , D. , Chlipala , A. J. , Henzinger , T. A. , Jhala , R. , and Majumdar , R . 2004. Generating tests from counterexamples . In ICSE 04: Proceedings of the International Conference on Software Engineering. ACM , New York, 326--335. Beyer, D., Chlipala, A. J., Henzinger, T. A., Jhala, R., and Majumdar, R. 2004. Generating tests from counterexamples. In ICSE 04: Proceedings of the International Conference on Software Engineering. ACM, New York, 326--335."},{"key":"e_1_2_1_26_1","volume-title":"VMCAI 07: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science","volume":"4349","author":"Beyer D.","unstructured":"Beyer , D. , Henzinger , T. , Majumdar , R. , and Rybalchenko , A . 2007a. Invariant synthesis in combination theories . In VMCAI 07: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science , vol. 4349 . Springer-Verlag, Berlin, Germany, 378--394. Beyer, D., Henzinger, T., Majumdar, R., and Rybalchenko, A. 2007a. Invariant synthesis in combination theories. In VMCAI 07: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4349. Springer-Verlag, Berlin, Germany, 378--394."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250769"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1296691.1296695"},{"key":"e_1_2_1_29_1","volume-title":"CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"4590","author":"Beyer D.","unstructured":"Beyer , D. , Henzinger , T. A. , and Th\u00e9oduloz , G . 2007. Configurable software verification: Concretizing the convergence of model checking and program analysis . In CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 4590 . Springer-Verlag, Berlin, Germany, 504--518. Beyer, D., Henzinger, T. A., and Th\u00e9oduloz, G. 2007. Configurable software verification: Concretizing the convergence of model checking and program analysis. In CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 504--518."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"Analysis, Transformation: Essays Dedicated to Neil D. Jones","author":"Blanchet B.","year":"2002","unstructured":"Blanchet , B. , Cousot , P. , Cousot , R. , Feret , J. , Mauborgne , L. , Mine , A. , Monniaux , D. , and Rival , X . 2002 . Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation, Complexity, Analysis, Transformation: Essays Dedicated to Neil D. Jones . Lecture Notes in Computer Science , vol. 2566 . Springer-Verlag , Berlin, Germany, 85--108. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation, Complexity, Analysis, Transformation: Essays Dedicated to Neil D. Jones. Lecture Notes in Computer Science, vol. 2566. Springer-Verlag, Berlin, Germany, 85--108."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_33_1","volume-title":"CONCUR 97: Proceedings of the Symposium on Concurrency Theory. Lecture Notes in Computer Science","volume":"1243","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Maler , O . 1994. Reachability analysis of pushdown automata: application to model checking . In CONCUR 97: Proceedings of the Symposium on Concurrency Theory. Lecture Notes in Computer Science , vol. 1243 . Springer-Verlag, Berlin, Germany, 135--150. Bouajjani, A., Esparza, J., and Maler, O. 1994. Reachability analysis of pushdown automata: application to model checking. In CONCUR 97: Proceedings of the Symposium on Concurrency Theory. Lecture Notes in Computer Science, vol. 1243. Springer-Verlag, Berlin, Germany, 135--150."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_1_35_1","volume-title":"CAV 90: Proceedings of the Symposium on Computer-aided Verification. Lecture Notes in Computer Science","volume":"531","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Fernandez , J.-C. , and Halbwachs , N . 1990. Minimal model generation . In CAV 90: Proceedings of the Symposium on Computer-aided Verification. Lecture Notes in Computer Science , vol. 531 . Springer-Verlag, Berlin, Germany, 197--203. Bouajjani, A., Fernandez, J.-C., and Halbwachs, N. 1990. Minimal model generation. In CAV 90: Proceedings of the Symposium on Computer-aided Verification. Lecture Notes in Computer Science, vol. 531. Springer-Verlag, Berlin, Germany, 197--203."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040027.28662.a4"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/635499.635502"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040026.56959.91"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_22"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Chaki S. Clarke E. M. Groce A. and Strichman O. 2003. Predicate abstraction with minimum predicates. In CHARME. 19--34.  Chaki S. Clarke E. M. Groce A. and Strichman O. 2003. Predicate abstraction with minimum predicates. In CHARME. 19--34.","DOI":"10.1007\/978-3-540-39724-3_5"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/581339.581393"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93585"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/586110.586142"},{"key":"e_1_2_1_51_1","volume-title":"Logic of Programs. Lecture Notes in Computer Science","volume":"131","author":"Clarke E. M.","unstructured":"Clarke , E. M. and Emerson , E. A . 1981. Synthesis of synchronization skeletons for branching time temporal logic . In Logic of Programs. Lecture Notes in Computer Science , vol. 131 . Springer-Verlag, Berlin, Germany, 52--71. Clarke, E. M. and Emerson, E. A. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs. Lecture Notes in Computer Science, vol. 131. Springer-Verlag, Berlin, Germany, 52--71."},{"key":"e_1_2_1_52_1","volume-title":"CAV 93: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"697","author":"Clarke E. M.","unstructured":"Clarke , E. M. , Filkorn , T. , and Jha , S . 1993. Exploiting symmetry in temporal logic model checking . In CAV 93: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 697 . Springer-Verlag, Berlin, Germany, 450--462. Clarke, E. M., Filkorn, T., and Jha, S. 1993. Exploiting symmetry in temporal logic model checking. In CAV 93: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 697. Springer-Verlag, Berlin, Germany, 450--462."},{"key":"e_1_2_1_53_1","volume-title":"CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1855","author":"Clarke E. M.","unstructured":"Clarke , E. M. , Grumberg , O. , Jha , S. , Lu , Y. , and Veith , H . 2000. Counterexample-guided abstraction refinement . In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1855 . Springer-Verlag, Berlin, Germany, 154--169. Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-guided abstraction refinement. In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, Berlin, Germany, 154--169."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233817"},{"key":"e_1_2_1_56_1","volume-title":"TACAS 01: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"2031","author":"Col\u00f3n M.","unstructured":"Col\u00f3n , M. and Sipma , H . 2001. Synthesis of linear ranking functions . In TACAS 01: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 2031 . Springer-Verlag, Berlin, Germany, 67--81. Col\u00f3n, M. and Sipma, H. 2001. Synthesis of linear ranking functions. In TACAS 01: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer-Verlag, Berlin, Germany, 67--81."},{"key":"e_1_2_1_57_1","volume-title":"CAV 02: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"2404","author":"Col\u00f3n M.","unstructured":"Col\u00f3n , M. and Sipma , H . 2002. Practical methods for proving program termination . In CAV 02: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 2404 . Springer-Verlag, Berlin, Germany, 442--454. Col\u00f3n, M. and Sipma, H. 2002. Practical methods for proving program termination. In CAV 02: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany, 442--454."},{"key":"e_1_2_1_58_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable R.","unstructured":"Constable , R. 1986. Implementing Mathematics with the Nuprl Proof Development System . Prentice-Hall, Englewood Cliffs , NJ. Constable, R. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"e_1_2_1_63_1","unstructured":"Cousot P. and Cousot R. 1976. Static determination of dynamic properties of programs. In ISOP. 106--130.  Cousot P. and Cousot R. 1976. Static determination of dynamic properties of programs. In ISOP. 106--130."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325699"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_70_1","volume-title":"CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1633","author":"Das S.","unstructured":"Das , S. , Dill , D. L. , and Park , S . 1999. Experience with predicate abstraction . In CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1633 . Springer-Verlag, Berlin, Germany, 160--171. Das, S., Dill, D. L., and Park, S. 1999. Experience with predicate abstraction. In CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, Berlin, Germany, 160--171."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"e_1_2_1_72_1","volume-title":"TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"4963","author":"de Moura L.","unstructured":"de Moura , L. and Bj\u00f8rner , N . 2008. Z3: An efficient SMT solver . In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 4963 . Springer-Verlag, Berlin, Germany, 337--340. de Moura, L. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 337--340."},{"key":"e_1_2_1_73_1","volume-title":"CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"2725","author":"de Moura L.","unstructured":"de Moura , L. and Ruess , H . 2003. Bounded model checking and induction: From refutation to verification . In CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 2725 . Springer-Verlag, Berlin, Germany, 14--26. de Moura, L. and Ruess, H. 2003. Bounded model checking and induction: From refutation to verification. In CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, Berlin, Germany, 14--26."},{"key":"e_1_2_1_74_1","volume-title":"CADE 02: Proceedings of the Symposium on Automated Deduction. Lecture Notes in Computer Science","volume":"2392","author":"de Moura L.","unstructured":"de Moura , L. , Ruess , H. , and Sorea , M . 2002. Lazy theorem proving for bounded model checking over infinite domains . In CADE 02: Proceedings of the Symposium on Automated Deduction. Lecture Notes in Computer Science , vol. 2392 . Springer-Verlag, Berlin, Germany, 438--455. de Moura, L., Ruess, H., and Sorea, M. 2002. Lazy theorem proving for bounded model checking over infinite domains. In CADE 02: Proceedings of the Symposium on Automated Deduction. Lecture Notes in Computer Science, vol. 2392. Springer-Verlag, Berlin, Germany, 438--455."},{"key":"e_1_2_1_75_1","volume-title":"A Discipline of Programming","author":"Dijkstra E.","unstructured":"Dijkstra , E. 1976. A Discipline of Programming . Prentice-Hall, Englewood Cliffs , NJ. Dijkstra, E. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_76_1","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 96: Proceedings of the Symposium on Computer-Aided Verification","author":"Dill D.","unstructured":"Dill , D. 1996. The Murphi verification system . In CAV 96: Proceedings of the Symposium on Computer-Aided Verification . Lecture Notes in Computer Science , vol. 1102 . Springer-Verlag , Berlin, Germany , 390--393. Dill, D. 1996. The Murphi verification system. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 390--393."},{"key":"e_1_2_1_77_1","volume-title":"Lecture Notes in Computer Science","volume":"4905","author":"Dimitrova R.","unstructured":"Dimitrova , R. and Podelski , A . 2008. Is lazy abstraction a decision procedure for broadcast protocols&quest; In VMCAI 08: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation . Lecture Notes in Computer Science , vol. 4905 . Springer-Verlag, Berlin, Germany, 98--111. Dimitrova, R. and Podelski, A. 2008. Is lazy abstraction a decision procedure for broadcast protocols&quest; In VMCAI 08: Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4905. Springer-Verlag, Berlin, Germany, 98--111."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_79_1","first-page":"365","article-title":"Decidability of the weak second-order theory of two successors","volume":"12","author":"Doner J. E.","year":"1965","unstructured":"Doner , J. E. 1965 . Decidability of the weak second-order theory of two successors . Notices Amer. Math. Soc. 12 , 365 -- 468 . Doner, J. E. 1965. Decidability of the weak second-order theory of two successors. Notices Amer. Math. Soc. 12, 365--468.","journal-title":"Notices Amer. Math. Soc."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/193173.195295"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.5555\/3049063.3049099"},{"key":"e_1_2_1_83_1","volume-title":"SAT 2003: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science","volume":"2919","author":"Een N.","unstructured":"Een , N. and Sorensson , N . 2003. An extensible SAT solver . In SAT 2003: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science , vol. 2919 . Springer-Verlag, Berlin, Germany, 502--518. Een, N. and Sorensson, N. 2003. An extensible SAT solver. In SAT 2003: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science, vol. 2919. Springer-Verlag, Berlin, Germany, 502--518."},{"key":"e_1_2_1_84_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E.","unstructured":"Emerson , E. 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science , J. van Leeuwen, Ed. vol. B. Elsevier Science Publishers , Amsterdam , the Netherlands, 995--1072. Emerson, E. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. vol. B. Elsevier Science Publishers, Amsterdam, the Netherlands, 995--1072."},{"key":"e_1_2_1_85_1","volume-title":"Proceedings of the 1st Annual Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Emerson E.","unstructured":"Emerson , E. and Lei , C . 1986. Efficient model checking in fragments of the propositional &mu;-calculus . In Proceedings of the 1st Annual Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 267--278. Emerson, E. and Lei, C. 1986. Efficient model checking in fragments of the propositional &mu;-calculus. In Proceedings of the 1st Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 267--278."},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625970"},{"key":"e_1_2_1_87_1","doi-asserted-by":"crossref","unstructured":"Esparza J. and Schwoon S. 2001. A BDD-based model checker for recursive programs. In CAV. 324--336.   Esparza J. and Schwoon S. 2001. A BDD-based model checker for recursive programs. In CAV. 324--336.","DOI":"10.1007\/3-540-44585-4_30"},{"key":"e_1_2_1_88_1","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 04: Proceedings of the Symposium on Object-Oriented Programming","author":"Fahndrich M.","unstructured":"Fahndrich , M. and DeLine , R. 2004. Typestates for objects . In ECOOP 04: Proceedings of the Symposium on Object-Oriented Programming . Lecture Notes in Computer Science , vol. 3086 . Springer-Verlag , Berlin, Germany , 465--490. Fahndrich, M. and DeLine, R. 2004. Typestates for objects. In ECOOP 04: Proceedings of the Symposium on Object-Oriented Programming. Lecture Notes in Computer Science, vol. 3086. Springer-Verlag, Berlin, Germany, 465--490."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081742"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_2_1_91_1","volume-title":"ESOP 02: Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science","volume":"2305","author":"Flanagan C.","unstructured":"Flanagan , C. , Freund , S. and Qadeer , S . 2002. Thread-modular verification for shared-memory programs . In ESOP 02: Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science , vol. 2305 . Springer-Verlag, Berlin, Germany, 262--277. Flanagan, C., Freund, S. and Qadeer, S. 2002. Thread-modular verification for shared-memory programs. In ESOP 02: Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 2305. Springer-Verlag, Berlin, Germany, 262--277."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.006"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_2_1_97_1","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd R.","unstructured":"Floyd , R. 1967. Assigning meanings to programs . In Mathematical Aspects of Computer Science . American Mathematical Society , 19--32. Floyd, R. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science. American Mathematical Society, 19--32."},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"e_1_2_1_99_1","doi-asserted-by":"crossref","unstructured":"Francez N. 1986. Fairness. Springer-Verlag Berlin Germany.   Francez N. 1986. Fairness. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_100_1","volume-title":"CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1855","author":"Fraser R.","unstructured":"Fraser , R. , Kamhi , G. , Ziv , B. , Vardi , M. , and Fix , L . 2000. Prioritized traversal: efficient reachability analysis for verification and falsification . In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1855 . Springer-Verlag, Berlin, Germany, 389--402. Fraser, R., Kamhi, G., Ziv, B., Vardi, M., and Fix, L. 2000. Prioritized traversal: efficient reachability analysis for verification and falsification. In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, Berlin, Germany, 389--402."},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233664"},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237724"},{"key":"e_1_2_1_103_1","volume-title":"IJCAR 2001: Proceedings of the International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science","volume":"2083","author":"Giesl J.","unstructured":"Giesl , J. and Kapur , D . 2001. Decidable classes of inductive theorems . In IJCAR 2001: Proceedings of the International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science , vol. 2083 . Springer-Verlag, Berlin, Germany, 469--484. Giesl, J. and Kapur, D. 2001. Decidable classes of inductive theorems. In IJCAR 2001: Proceedings of the International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 2083. Springer-Verlag, Berlin, Germany, 469--484."},{"key":"e_1_2_1_104_1","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem","author":"Godefroid P.","unstructured":"Godefroid , P. 1996. Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem . Lecture Notes in Computer Science , vol. 1032 . Springer-Verlag , Berlin, Germany . Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040333"},{"key":"e_1_2_1_108_1","volume-title":"CAV. Lecture Notes in Computer Science","volume":"1254","author":"Graf S.","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with PVS . In CAV. Lecture Notes in Computer Science , vol. 1254 . Springer-Verlag, Berlin, Germany, 72--83. Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In CAV. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany, 72--83."},{"key":"e_1_2_1_109_1","volume-title":"TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"4963","author":"Gulavani B. S.","unstructured":"Gulavani , B. S. , Chakraborty , S. , Nori , A. V. , and Rajamani , S. K . 2008. Automatically refining abstract interpretations . In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 4963 . Springer-Verlag, Berlin, Germany, 443--458. Gulavani, B. S., Chakraborty, S., Nori, A. V., and Rajamani, S. K. 2008. Automatically refining abstract interpretations. In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 443--458."},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134026"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_24"},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181785"},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250767"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSSC.1968.300136"},{"key":"e_1_2_1_118_1","first-page":"72","article-title":"Model checking Java programs using Java Pathfinder","volume":"2","author":"Havelund K.","year":"2000","unstructured":"Havelund , K. and Pressburger , T. 2000 . Model checking Java programs using Java Pathfinder . Softw. Tools Tech. Trans. (STTT) 2 , 4, 72 -- 84 . Havelund, K. and Pressburger, T. 2000. Model checking Java programs using Java Pathfinder. Softw. Tools Tech. Trans. (STTT) 2, 4, 72--84.","journal-title":"Softw. Tools Tech. Trans. (STTT)"},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_1_120_1","volume-title":"CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag","author":"Henzinger T.","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , and Qadeer , S . 2003. Thread-modular abstraction refinement . In CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany. Henzinger, T., Jhala, R., Majumdar, R., and Qadeer, S. 2003. Thread-modular abstraction refinement. In CAV 03: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_122_1","doi-asserted-by":"crossref","unstructured":"Henzinger T. Qadeer S. and \n      Rajamani S\n  . \n  1998\n  . You assume we guarantee: methodology and case studies. In CAV 98: Proceedings of the Symposium on Computer-Aided Verification Lecture Notes in Computer Science vol. \n  1427\n  . \n  Springer-Verlag Berlin Germany 440--451.   Henzinger T. Qadeer S. and Rajamani S. 1998. You assume we guarantee: methodology and case studies. In CAV 98: Proceedings of the Symposium on Computer-Aided Verification Lecture Notes in Computer Science vol. 1427. Springer-Verlag Berlin Germany 440--451.","DOI":"10.1007\/BFb0028765"},{"key":"e_1_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996844"},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_2_1_125_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_127_1","doi-asserted-by":"crossref","unstructured":"Immerman N. Rabinovich A. Reps T. Sagiv M. and Yorsh G. 2004. The boundary between decidability and undecidability for transitive-closure logics. In CSL. 160--174.  Immerman N. Rabinovich A. Reps T. Sagiv M. and Yorsh G. 2004. The boundary between decidability and undecidability for transitive-closure logics. In CSL. 160--174.","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625968"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.013"},{"key":"e_1_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_31"},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_15"},{"key":"e_1_2_1_132_1","volume-title":"Proceedings of the 12th ACM International Conference on Hybrid Systems: Computation and Control. ACM","author":"Jha S. K.","unstructured":"Jha , S. K. , Krogh , B. H. , Weimer , J. E. , and Clarke , E. M . 2007. Reachability for linear hybrid automata using iterative relaxation abstraction . In Proceedings of the 12th ACM International Conference on Hybrid Systems: Computation and Control. ACM , New York, 287--300. Jha, S. K., Krogh, B. H., Weimer, J. E., and Clarke, E. M. 2007. Reachability for linear hybrid automata using iterative relaxation abstraction. In Proceedings of the 12th ACM International Conference on Hybrid Systems: Computation and Control. ACM, New York, 287--300."},{"key":"e_1_2_1_133_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065016"},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_6"},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_137_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190262"},{"key":"e_1_2_1_138_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02252682"},{"key":"e_1_2_1_139_1","volume-title":"Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI). ACM","author":"Killian C. E.","unstructured":"Killian , C. E. , Anderson , J. W. , Jhala , R. , and Vahdat , A . 2007. Life, death, and the critical transition: Finding liveness bugs in systems code (awarded best paper) . In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI). ACM , New York, 243--256. Killian, C. E., Anderson, J. W., Jhala, R., and Vahdat, A. 2007. Life, death, and the critical transition: Finding liveness bugs in systems code (awarded best paper). In Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI). ACM, New York, 243--256."},{"key":"e_1_2_1_140_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90084-0"},{"key":"e_1_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_143_1","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"Kurshan R.","unstructured":"Kurshan , R. 1994. Computer-Aided Verification of Coordinating Processes . Princeton University Press, Princeton , NJ. Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ."},{"key":"e_1_2_1_144_1","volume-title":"Proceedings of the 5th International Conference on Verification Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Springer-Verlag","author":"Lahiri S. K.","unstructured":"Lahiri , S. K. and Bryant , R. E . 2004. Constructing quantified invariants via predicate abstraction . In Proceedings of the 5th International Conference on Verification Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany, 267--281. Lahiri, S. K. and Bryant, R. E. 2004. Constructing quantified invariants via predicate abstraction. In Proceedings of the 5th International Conference on Verification Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 267--281."},{"key":"e_1_2_1_145_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_2_1_146_1","volume-title":"TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"4963","author":"Lal A.","unstructured":"Lal , A. , Touili , T. , Kidd , N. , and Reps , T. W . 2008. Interprocedural analysis of concurrent programs under a context bound . In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 4963 . Springer-Verlag, Berlin, Germany, 282--298. Lal, A., Touili, T., Kidd, N., and Reps, T. W. 2008. Interprocedural analysis of concurrent programs under a context bound. In TACAS 08: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 282--298."},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1145\/69624.357207"},{"key":"e_1_2_1_148_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129738"},{"key":"e_1_2_1_149_1","volume-title":"ICALP 81: Proceedings of the International Conference on Automata, Languages, and Programming. Lecture Notes in Computer Science 115","author":"Lehmann D.","unstructured":"Lehmann , D. , Pnueli , A. , and Stavi , J . 1982. Impartiality, justice, and fairness: The ethics of concurrent termination . In ICALP 81: Proceedings of the International Conference on Automata, Languages, and Programming. Lecture Notes in Computer Science 115 . Springer-Verlag, Berlin, Germany, 264--277. Lehmann, D., Pnueli, A., and Stavi, J. 1982. Impartiality, justice, and fairness: The ethics of concurrent termination. In ICALP 81: Proceedings of the International Conference on Automata, Languages, and Programming. Lecture Notes in Computer Science 115. Springer-Verlag, Berlin, Germany, 264--277."},{"key":"e_1_2_1_150_1","volume-title":"CC 98: Proceedings of the Symposium on Compiler Construction. Lecture Notes in Computer Science","volume":"1383","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and Nelson , G . 1998. An extended static checker for Modula-3 . In CC 98: Proceedings of the Symposium on Compiler Construction. Lecture Notes in Computer Science , vol. 1383 . Springer-Verlag, Berlin, Germany, 302--305. Leino, K. R. M. and Nelson, G. 1998. An extended static checker for Modula-3. In CC 98: Proceedings of the Symposium on Compiler Construction. Lecture Notes in Computer Science, vol. 1383. Springer-Verlag, Berlin, Germany, 302--305."},{"key":"e_1_2_1_151_1","series-title":"Lecture Notes in Computer Science","volume-title":"TVLA: A system for implementing static analyses. In Proceedings of the 5th International Symposium on Static Analysis (SAS)","author":"Lev-Ami T.","year":"2000","unstructured":"Lev-Ami , T. and Sagiv , S . 2000 . TVLA: A system for implementing static analyses. In Proceedings of the 5th International Symposium on Static Analysis (SAS) . Lecture Notes in Computer Science , vol. 1824 . Springer-Verlag , Berlin, Germany , 280--301. Lev-Ami, T. and Sagiv, S. 2000. TVLA: A system for implementing static analyses. In Proceedings of the 5th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 1824. Springer-Verlag, Berlin, Germany, 280--301."},{"key":"e_1_2_1_153_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384313"},{"key":"e_1_2_1_154_1","volume-title":"Proceedings of the 14th International Symposium on Static Analysis. Lecture Notes in Computer Science, Springer-Verlag","author":"Magill S.","unstructured":"Magill , S. , Berdine , J. , Clarke , E. M. , and Cook , B . 2007. Arithmetic strengthening for shape analysis . In Proceedings of the 14th International Symposium on Static Analysis. Lecture Notes in Computer Science, Springer-Verlag , Berlin, Germany, 419--436. Magill, S., Berdine, J., Clarke, E. M., and Cook, B. 2007. Arithmetic strengthening for shape analysis. In Proceedings of the 14th International Symposium on Static Analysis. Lecture Notes in Computer Science, Springer-Verlag, Berlin, Germany, 419--436."},{"key":"e_1_2_1_155_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag Berlin Germany.   Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_156_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1984.0073"},{"key":"e_1_2_1_157_1","volume-title":"Symbolic Model Checking: An Approach to the State-Explosion Problem","author":"McMillan K.","unstructured":"McMillan , K. 1993. Symbolic Model Checking: An Approach to the State-Explosion Problem . Kluwer Academic Publishers . McMillan, K. 1993. Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic Publishers."},{"key":"e_1_2_1_158_1","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems","author":"McMillan K. L.","unstructured":"McMillan , K. L. 2004. An interpolating theorem prover . In TACAS: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science . Springer-Verlag, Berlin , Germany , 16--30. McMillan, K. L. 2004. An interpolating theorem prover. In TACAS: Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 16--30."},{"key":"e_1_2_1_159_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_1_160_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems","author":"McMillan K. L.","unstructured":"McMillan , K. L. 2008. Quantified invariant generation using an interpolating saturation prover . In Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science . Springer-Verlag, Berlin , Germany , 413--427. McMillan, K. L. 2008. Quantified invariant generation using an interpolating saturation prover. In Proceedings of the Symposium on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 413--427."},{"key":"e_1_2_1_161_1","doi-asserted-by":"publisher","DOI":"10.1007\/11921240_23"},{"key":"e_1_2_1_162_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_163_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_1_164_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_1_165_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_166_1","volume-title":"Advanced Compiler Design and Implementation. Morgan-Kaufman","author":"Muchnick S.","unstructured":"Muchnick , S. 1997. Advanced Compiler Design and Implementation. Morgan-Kaufman , San Francisco, CA . Muchnick, S. 1997. Advanced Compiler Design and Implementation. Morgan-Kaufman, San Francisco, CA."},{"key":"e_1_2_1_167_1","unstructured":"Musuvathi M. and Engler D. R. 2004. Model checking large network protocol implementations. In NSDI. 155--168.   Musuvathi M. and Engler D. R. 2004. Model checking large network protocol implementations. In NSDI. 155--168."},{"key":"e_1_2_1_168_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_169_1","volume-title":"CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag","author":"Namjoshi K. S.","unstructured":"Namjoshi , K. S. and Kurshan , R. P . 2000. Syntactic program transformations for automatic abstraction . In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany, 435--449. Namjoshi, K. S. and Kurshan, R. P. 2000. Syntactic program transformations for automatic abstraction. In CAV 00: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 435--449."},{"key":"e_1_2_1_170_1","volume-title":"Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP. ACM","author":"Nanevski A.","unstructured":"Nanevski , A. , Morrisett , G. , Shinnar , A. , Govereau , P. , and Birkedal , L . 2008. Ynot: Reasoning with the awkward squad . In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP. ACM , New York. Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., and Birkedal, L. 2008. Ynot: Reasoning with the awkward squad. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP. ACM, New York."},{"key":"e_1_2_1_171_1","volume-title":"CADE 00: Proceedings of the Symposium on Computer-Aided Deduction. Lecture Notes in Computer Science","volume":"1831","author":"Necula G. C.","unstructured":"Necula , G. C. and Lee , P . 2000. Proof generation in the Touchstone theorem prover . In CADE 00: Proceedings of the Symposium on Computer-Aided Deduction. Lecture Notes in Computer Science , vol. 1831 . Springer-Verlag, Berlin, Germany, 25--44. Necula, G. C. and Lee, P. 2000. Proof generation in the Touchstone theorem prover. In CADE 00: Proceedings of the Symposium on Computer-Aided Deduction. Lecture Notes in Computer Science, vol. 1831. Springer-Verlag, Berlin, Germany, 25--44."},{"key":"e_1_2_1_173_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567073"},{"key":"e_1_2_1_174_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_175_1","series-title":"Lecture Notes in Computer Science","volume-title":"PVS: Combining specification, proof checking, and model checking. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification","author":"Owre S.","year":"1996","unstructured":"Owre , S. , Rajan , S. , Rushby , J. , Shankar , N. , and Srivas , M . 1996 . PVS: Combining specification, proof checking, and model checking. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification . Lecture Notes in Computer Science , vol. 1102 . Springer-Verlag, Berlin , Germany , 411--414. Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. 1996. PVS: Combining specification, proof checking, and model checking. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 411--414."},{"key":"e_1_2_1_176_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0049-6"},{"key":"e_1_2_1_177_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1490-4"},{"key":"e_1_2_1_178_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_179_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_9"},{"key":"e_1_2_1_180_1","doi-asserted-by":"crossref","unstructured":"Podelski A. and Rybalchenko A. 2004a. A complete method for the synthesis of linear ranking functions. In VMCAI. 239--251.  Podelski A. and Rybalchenko A. 2004a. A complete method for the synthesis of linear ranking functions. In VMCAI. 239--251.","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_181_1","volume-title":"LICS 04: Proceedings of the Symposium on Logic in Computer Science. IEEE, Computer Society Press","author":"Podelski A.","unstructured":"Podelski , A. and Rybalchenko , A . 2004b. Transition invariants . In LICS 04: Proceedings of the Symposium on Logic in Computer Science. IEEE, Computer Society Press , Los Alamitos, CA. Podelski, A. and Rybalchenko, A. 2004b. Transition invariants. In LICS 04: Proceedings of the Symposium on Logic in Computer Science. IEEE, Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_182_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"e_1_2_1_183_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_19"},{"key":"e_1_2_1_184_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964022"},{"key":"e_1_2_1_185_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_186_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_2_1_187_1","volume-title":"Proceedings of the 5th International Symposium on Programming, M. Dezani-Ciancaglini and U. Montanari, Eds. Lecture Notes in Computer Science","volume":"137","author":"Queille J.","unstructured":"Queille , J. and Sifakis , J . 1981. Specification and verification of concurrent systems in CESAR . In Proceedings of the 5th International Symposium on Programming, M. Dezani-Ciancaglini and U. Montanari, Eds. Lecture Notes in Computer Science , vol. 137 . Springer-Verlag, Berlin, Germany, 337--351. Queille, J. and Sifakis, J. 1981. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming, M. Dezani-Ciancaglini and U. Montanari, Eds. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, Berlin, Germany, 337--351."},{"key":"e_1_2_1_188_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_1_189_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_190_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_191_1","series-title":"Lecture Notes in Computer Science","volume-title":"Separation logic: A logic for shared mutable data structures","author":"Reynolds J. C.","unstructured":"Reynolds , J. C. 2002. Separation logic: A logic for shared mutable data structures . Lecture Notes in Computer Science . Springer-Verlag, Berlin , Germany , 55--74. Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 55--74."},{"key":"e_1_2_1_192_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_193_1","volume-title":"Artificial Intelligence: A Modern Approach","author":"Russell S.","year":"2003","unstructured":"Russell , S. and Norvig , P . 2003 . Artificial Intelligence: A Modern Approach , 2 nd ed. Prentice-Hall , Englewood Cliffs, NJ . Russell, S. and Norvig, P. 2003. Artificial Intelligence: A Modern Approach, 2nd ed. Prentice-Hall, Englewood Cliffs, NJ.","edition":"2"},{"key":"e_1_2_1_194_1","doi-asserted-by":"crossref","unstructured":"Rybalchenko A. and Sofronie-Stokkermans V. 2007. Constraint solving for interpolation. In VMCAI. 346--362.   Rybalchenko A. and Sofronie-Stokkermans V. 2007. Constraint solving for interpolation. In VMCAI. 346--362.","DOI":"10.1007\/978-3-540-69738-1_25"},{"key":"e_1_2_1_195_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_196_1","series-title":"Lecture Notes in Computer Science","volume-title":"SAS 00: Proceedings of the Static-Analysis Symposium","author":"Saidi H.","unstructured":"Saidi , H. 2000. Model checking guided abstraction and analysis . In SAS 00: Proceedings of the Static-Analysis Symposium . Lecture Notes in Computer Science , vol. 1824 , Springer-Verlag , Berlin, Germany , 377--396. Saidi, H. 2000. Model checking guided abstraction and analysis. In SAS 00: Proceedings of the Static-Analysis Symposium. Lecture Notes in Computer Science, vol. 1824, Springer-Verlag, Berlin, Germany, 377--396."},{"key":"e_1_2_1_197_1","volume-title":"CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1633","author":"Sa\u00efdi H.","unstructured":"Sa\u00efdi , H. and Shankar , N . 1999. Abstract and model check while you prove . In CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1633 . Springer-Verlag, Berlin, Germany, 443--454. Sa\u00efdi, H. and Shankar, N. 1999. Abstract and model check while you prove. In CAV 99: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, Berlin, Germany, 443--454."},{"key":"e_1_2_1_198_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"e_1_2_1_199_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268950"},{"key":"e_1_2_1_200_1","volume-title":"SAS 98: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science","volume":"1503","author":"Schmidt D. A.","unstructured":"Schmidt , D. A. and Steffen , B . 1998. Program analysis as model checking of abstract interpretations . In SAS 98: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science , vol. 1503 . Springer-Verlag, ACM, New York, 351--380. Schmidt, D. A. and Steffen, B. 1998. Program analysis as model checking of abstract interpretations. In SAS 98: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 1503. Springer-Verlag, ACM, New York, 351--380."},{"key":"e_1_2_1_201_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_202_1","unstructured":"Sharir M. and Pnueli A. 1981. Two approaches to interprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall Englewood Cliffs NJ 189--233.  Sharir M. and Pnueli A. 1981. Two approaches to interprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall Englewood Cliffs NJ 189--233."},{"key":"e_1_2_1_203_1","volume-title":"FMCAD 00: Proceedings of the Symposium on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science","volume":"1954","author":"Sheeran M.","unstructured":"Sheeran , M. , Singh , S. , and Stalmarck , G . 2000. Checking safety properties using induction and a SAT-solver . In FMCAD 00: Proceedings of the Symposium on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science , vol. 1954 . Springer-Verlag, Berlin, Germany, 108--125. Sheeran, M., Singh, S., and Stalmarck, G. 2000. Checking safety properties using induction and a SAT-solver. In FMCAD 00: Proceedings of the Symposium on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1954. Springer-Verlag, Berlin, Germany, 108--125."},{"key":"e_1_2_1_204_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_2_1_205_1","volume-title":"ICCAD 96: Proceedings of the International Conference on Computer-Aided Design. ACM","author":"Silva J. P. M.","unstructured":"Silva , J. P. M. and Sakallah , K. A . 1996. Grasp\u2014A new search algorithm for satisfiability . In ICCAD 96: Proceedings of the International Conference on Computer-Aided Design. ACM , New York, 220--227. Silva, J. P. M. and Sakallah, K. A. 1996. Grasp\u2014A new search algorithm for satisfiability. In ICCAD 96: Proceedings of the International Conference on Computer-Aided Design. ACM, New York, 220--227."},{"key":"e_1_2_1_206_1","doi-asserted-by":"publisher","DOI":"10.1145\/350887.350891"},{"key":"e_1_2_1_207_1","unstructured":"Somenzi F. 1998. Colorado University decision diagram package. http:\/\/vlsi.colorado.edu\/pub\/.  Somenzi F. 1998. Colorado University decision diagram package. http:\/\/vlsi.colorado.edu\/pub\/."},{"key":"e_1_2_1_208_1","doi-asserted-by":"publisher","DOI":"10.5555\/646823.706907"},{"key":"e_1_2_1_209_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_1_210_1","series-title":"Lecture Notes in Computer Science","volume-title":"TACS 91: Proceedings of the Symposium on Theoretical Aspects of Computer Science","author":"Steffen B.","unstructured":"Steffen , B. 1991. Data flow analysis as model checking . In TACS 91: Proceedings of the Symposium on Theoretical Aspects of Computer Science . Lecture Notes in Computer Science , vol. 536 . Springer-Verlag , Berlin, Germany , 346--365. Steffen, B. 1991. Data flow analysis as model checking. In TACS 91: Proceedings of the Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 536. Springer-Verlag, Berlin, Germany, 346--365."},{"key":"e_1_2_1_211_1","volume-title":"CAV 98: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag","author":"Stern U.","unstructured":"Stern , U. and Dill , D. L . 1998. Using magnetic disk instead of main memory in the murhi verifier . In CAV 98: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany, 172--183. Stern, U. and Dill, D. L. 1998. Using magnetic disk instead of main memory in the murhi verifier. In CAV 98: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 172--183."},{"key":"e_1_2_1_212_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_213_1","first-page":"346","article-title":"Survey of protocol definition and verification techniques","volume":"2","author":"Sunshine C.","year":"1978","unstructured":"Sunshine , C. 1978 . Survey of protocol definition and verification techniques . Comput. Netw. 2 , 346 -- 350 . Sunshine, C. 1978. Survey of protocol definition and verification techniques. Comput. Netw. 2, 346--350.","journal-title":"Comput. Netw."},{"key":"e_1_2_1_214_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1982.235736"},{"key":"e_1_2_1_215_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_19"},{"key":"e_1_2_1_216_1","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 04: Proceedings of the Symposium on Computer-Aided Verification","author":"Tiwari A.","unstructured":"Tiwari , A. 2004. Termination of linear programs . In CAV 04: Proceedings of the Symposium on Computer-Aided Verification . Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag , Berlin, Germany , 70--82. Tiwari, A. 2004. Termination of linear programs. In CAV 04: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 70--82."},{"key":"e_1_2_1_217_1","volume-title":"Proceedings of the London Mathematical Soceity. 230--265","author":"Turing A. M.","year":"1936","unstructured":"Turing , A. M. 1936 . On computable numbers, with an application to the eintscheidungsproblem . In Proceedings of the London Mathematical Soceity. 230--265 . Turing, A. M. 1936. On computable numbers, with an application to the eintscheidungsproblem. In Proceedings of the London Mathematical Soceity. 230--265."},{"key":"e_1_2_1_218_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709154"},{"key":"e_1_2_1_219_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_2_1_220_1","series-title":"Lecture Notes in Computer Science","volume-title":"Logics for Concurrency\u2014Structure versus Automata (8th Banff Higher Order Workshop Proceedings)","author":"Vardi M.","unstructured":"Vardi , M. 1995. An automata-theoretic approach to linear temporal logic . In Logics for Concurrency\u2014Structure versus Automata (8th Banff Higher Order Workshop Proceedings) . Lecture Notes in Computer Science , vol. 1043 . Springer-Verlag , Berlin, Germany , 238--266. Vardi, M. 1995. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency\u2014Structure versus Automata (8th Banff Higher Order Workshop Proceedings). Lecture Notes in Computer Science, vol. 1043. Springer-Verlag, Berlin, Germany, 238--266."},{"key":"e_1_2_1_221_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"e_1_2_1_222_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_1_223_1","volume-title":"TAP: Tests and Proofs. Lecture Notes in Computer Science","volume":"4966","author":"Velroyen H.","unstructured":"Velroyen , H. and R\u00fcmmer , P . 2008. Non-termination checking for imperative programs . In TAP: Tests and Proofs. Lecture Notes in Computer Science , vol. 4966 . Springer-Verlag, Berlin, Germany, 154--170. Velroyen, H. and R\u00fcmmer, P. 2008. Non-termination checking for imperative programs. In TAP: Tests and Proofs. Lecture Notes in Computer Science, vol. 4966. Springer-Verlag, Berlin, Germany, 154--170."},{"key":"e_1_2_1_224_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_1_225_1","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 96: Proceedings of the Symposium on Computer-Aided Verification","author":"Walukiewicz I.","unstructured":"Walukiewicz , I. 1996. Pushdown processes: Games and model checking . In CAV 96: Proceedings of the Symposium on Computer-Aided Verification . Lecture Notes in Computer Science , vol. 1102 . Springer-Verlag, Berlin , Germany , 62--74. Walukiewicz, I. 1996. Pushdown processes: Games and model checking. In CAV 96: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 62--74."},{"key":"e_1_2_1_226_1","volume-title":"CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag","author":"Wang C.","unstructured":"Wang , C. , Yang , Z. , Gupta , A. , and Ivancic , F . 2007. Using counterexamples for improving the precision of reachability computation with polyhedra . In CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany, 352--365. Wang, C., Yang, Z., Gupta, A., and Ivancic, F. 2007. Using counterexamples for improving the precision of reachability computation with polyhedra. In CAV 07: Proceedings of the Symposium on Computer-Aided Verification. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 352--365."},{"key":"e_1_2_1_227_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996859"},{"key":"e_1_2_1_228_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_229_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101908.1101951"},{"key":"e_1_2_1_230_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040334"},{"key":"e_1_2_1_231_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"},{"key":"e_1_2_1_232_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277201"},{"key":"e_1_2_1_233_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"e_1_2_1_234_1","volume-title":"OSDI 04: Proceedings of the Symposium on Operating System Design and Implementation. Usenix Association.","author":"Yang J.","unstructured":"Yang , J. , Twohey , P. , Engler , D. , and Musuvathi , M . 2004. Using model checking to find serious file system errors . In OSDI 04: Proceedings of the Symposium on Operating System Design and Implementation. Usenix Association. Yang, J., Twohey, P., Engler, D., and Musuvathi, M. 2004. Using model checking to find serious file system errors. In OSDI 04: Proceedings of the Symposium on Operating System Design and Implementation. Usenix Association."},{"key":"e_1_2_1_235_1","unstructured":"Yang Z. Wang C. Gupta A. and Ivancic F. 2006. Mixed symbolic representations for model checking software programs. In MEMOCODE. 17--26.  Yang Z. Wang C. Gupta A. and Ivancic F. 2006. Mixed symbolic representations for model checking software programs. In MEMOCODE. 17--26."},{"key":"e_1_2_1_236_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1592434.1592438","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1592434.1592438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:17:47Z","timestamp":1750249067000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1592434.1592438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10]]},"references-count":233,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["10.1145\/1592434.1592438"],"URL":"https:\/\/doi.org\/10.1145\/1592434.1592438","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10]]},"assertion":[{"value":"2008-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}