{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T10:12:21Z","timestamp":1672308741994},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,5]]},"abstract":"\n Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We extend predicate abstraction to\n transition predicate<\/jats:italic>\n abstraction. Transition predicate abstraction goes beyond the idea of finite\n abstract-state<\/jats:italic>\n programs (and checking the absence of loops). Instead, our abstraction algorithm transforms a program into a finite\n abstract-transition<\/jats:italic>\n program. Then a second algorithm checks fair termination. The two algorithms together yield an automated method for the verification of liveness properties under full fairness assumptions (impartiality, justice, and compassion). In summary, we exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of temporal properties.\n <\/jats:p>","DOI":"10.1145\/1232420.1232422","type":"journal-article","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T14:37:11Z","timestamp":1181140631000},"page":"15","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Transition predicate abstraction and fair termination"],"prefix":"10.1145","volume":"29","author":[{"given":"Andreas","family":"Podelski","sequence":"first","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Freiburg, Germany"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne and Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Lausanne, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2007,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge U.K. Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge U.K.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378846"},{"key":"e_1_2_1_5_1","volume-title":"TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"2031","author":"Ball T.","unstructured":"Ball , T. , Podelski , A. , and Rajamani , S. K . 2001b. Boolean and Cartesian abstractions for model checking C programs . In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 2031 . Springer, Berlin, Germany, 268--283. Ball, T., Podelski, A., and Rajamani, S. K. 2001b. Boolean and Cartesian abstractions for model checking C programs. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer, Berlin, Germany, 268--283."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155095"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_1_8_1","volume-title":"FSTTCS'1995: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science","volume":"1026","author":"Browne I.","unstructured":"Browne , I. , Manna , Z. , and Sipma , H . 1995. Generalized verification diagrams . In FSTTCS'1995: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science , vol. 1026 . Springer, Berlin, Germany, 484--498. Browne, I., Manna, Z., and Sipma, H. 1995. Generalized verification diagrams. In FSTTCS'1995: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 1026. Springer, Berlin, Germany, 484--498."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Congress on Logic, Methodology and Philosophy of Science","author":"B\u00fcchi J. R.","year":"1960","unstructured":"B\u00fcchi , J. R. 1960 . On a decision method in restricted second order arithmeric . In Proceedings of the International Congress on Logic, Methodology and Philosophy of Science . Stanford University Press, Stanford, CA, 1--11. B\u00fcchi, J. R. 1960. On a decision method in restricted second order arithmeric. In Proceedings of the International Congress on Logic, Methodology and Philosophy of Science. Stanford University Press, Stanford, CA, 1--11."},{"key":"e_1_2_1_10_1","volume-title":"ICSE'2003: Proceedings of the International Conference on Software Engineering. IEEE Computer Society Press","author":"Chaki S.","unstructured":"Chaki , S. , Clarke , E. , Groce , A. , Jha , S. , and Veith , H . 2003. Modular verification of software components in C . In ICSE'2003: Proceedings of the International Conference on Software Engineering. IEEE Computer Society Press , Los Alamitos, CA, 385--395. Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In ICSE'2003: Proceedings of the International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 385--395."},{"key":"e_1_2_1_11_1","volume-title":"6th International Workshop on Termination (WST","author":"Codish M.","year":"2003","unstructured":"Codish , M. , Genaim , S. , Bruynooghe , M. , Gallagher , J. , and Vanhoof , W . 2003. One loop at a time . In 6th International Workshop on Termination (WST 2003 ). Universidad Polit\u00e9cnica de Valencia, Valencia, Spain. Codish, M., Genaim, S., Bruynooghe, M., Gallagher, J., and Vanhoof, W. 2003. One loop at a time. In 6th International Workshop on Termination (WST 2003). Universidad Polit\u00e9cnica de Valencia, Valencia, Spain."},{"key":"e_1_2_1_12_1","volume-title":"TACAS'2001: 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'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 2031 . Springer, Berlin, Germany, 67--81. Col\u00f3n, M. and Sipma, H. 2001. Synthesis of linear ranking functions. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer, Berlin, Germany, 67--81."},{"key":"e_1_2_1_13_1","volume-title":"CAV'1998: Computer Aided Verification. Lecture Notes in Computer Science","volume":"1427","author":"Col\u00f3n M.","unstructured":"Col\u00f3n , M. and Uribe , T . 1998. Generating finite-state abstractions of reactive systems using decision procedures . In CAV'1998: Computer Aided Verification. Lecture Notes in Computer Science , vol. 1427 . Springer, Berlin, Germany, 293--304. Col\u00f3n, M. and Uribe, T. 1998. Generating finite-state abstractions of reactive systems using decision procedures. In CAV'1998: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1427. Springer, Berlin, Germany, 293--304."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_17_1","volume-title":"ICCL'1994: Proceedings of the International Conference on Computer Languages. IEEE Computer Society Press","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 1994. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages) . In ICCL'1994: Proceedings of the International Conference on Computer Languages. IEEE Computer Society Press , Los Alamitos, CA, 95--112. Cousot, P. and Cousot, R. 1994. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In ICCL'1994: Proceedings of the International Conference on Computer Languages. IEEE Computer Society Press, Los Alamitos, CA, 95--112."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100049"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100065"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Francez N. 1986. Fairness. Springer Berlin Germany. Francez N. 1986. Fairness. Springer Berlin Germany.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_22_1","volume-title":"CAV'1997: Computer Aided Verification. 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'1997: Computer Aided Verification. Lecture Notes in Computer Science , vol. 1254 . Springer, Berlin, Germany, 72--83. Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In CAV'1997: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254. Springer, Berlin, Germany, 72--83."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3000"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1744"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/135419.135462"},{"key":"e_1_2_1_27_1","volume-title":"CAV'2003: Computer Aided Verification. Lecture Notes in Computer Science","volume":"2725","author":"Lahiri S. K.","unstructured":"Lahiri , S. K. , Bryant , R. E. , and Cook , B . 2003. A symbolic approach to predicate abstraction . In CAV'2003: Computer Aided Verification. Lecture Notes in Computer Science , vol. 2725 . Springer, Berlin, Germany, 141--153. Lahiri, S. K., Bryant, R. E., and Cook, B. 2003. A symbolic approach to predicate abstraction. In CAV'2003: Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725. Springer, Berlin, Germany, 141--153."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360210"},{"key":"e_1_2_1_29_1","volume-title":"ICALP'1981: International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science","volume":"115","author":"Lehmann D.","unstructured":"Lehmann , D. , Pnueli , A. , and Stavi , J . 1981. Impartiality, justice and fairness: The ethics of concurrent termination . In ICALP'1981: International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science , vol. 115 . Springer, Berlin, Germany, 264--277. Lehmann, D., Pnueli, A., and Stavi, J. 1981. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP'1981: International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 115. Springer, Berlin, Germany, 264--277."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1995. Temporal verification of reactive systems: Safety. Springer Berlin Germany. Manna Z. and Pnueli A. 1995. Temporal verification of reactive systems: Safety. Springer Berlin Germany.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1996. Temporal verification of reactive systems: Progress. unpublished article. Manna Z. and Pnueli A. 1996. Temporal verification of reactive systems: Progress. unpublished article.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_1_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"ASIAN'1997: Advances in Computer Science","author":"Merz S.","unstructured":"Merz , S. 1997. Rules for abstraction . In ASIAN'1997: Advances in Computer Science . Lecture Notes in Computer Science , vol. 1345 . Springer , Berlin, Germany , 32--45. Merz, S. 1997. Rules for abstraction. In ASIAN'1997: Advances in Computer Science. Lecture Notes in Computer Science, vol. 1345. Springer, Berlin, Germany, 32--45."},{"key":"e_1_2_1_33_1","volume-title":"CAV'2002: Computer Aided Verification. Lecture Notes in Computer Science","volume":"2404","author":"Pnueli A.","unstructured":"Pnueli , A. , Xu , J. , and Zuck , L . 2002. Liveness with (0, 1, \u221e)-counter abstraction . In CAV'2002: Computer Aided Verification. Lecture Notes in Computer Science , vol. 2404 . Springer, Berlin, Germany, 107--122. Pnueli, A., Xu, J., and Zuck, L. 2002. Liveness with (0, 1, \u221e)-counter abstraction. In CAV'2002: Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404. Springer, Berlin, Germany, 107--122."},{"key":"e_1_2_1_34_1","volume-title":"VMCAI'2004: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science","volume":"2937","author":"Podelski A.","unstructured":"Podelski , A. and Rybalchenko , A . 2004a. A complete method for the synthesis of linear ranking functions . In VMCAI'2004: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science , vol. 2937 . Springer, Berlin, Germany, 239--251. Podelski, A. and Rybalchenko, A. 2004a. A complete method for the synthesis of linear ranking functions. In VMCAI'2004: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer, Berlin, Germany, 239--251."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_2_1_37_1","volume-title":"ISLP'1991: Proceedings of the International Logic Programming Symposium, 518--532","author":"Sagiv Y.","year":"1991","unstructured":"Sagiv , Y. 1991 . A termination test for logic programs . In ISLP'1991: Proceedings of the International Logic Programming Symposium, 518--532 . Sagiv, Y. 1991. A termination test for logic programs. In ISLP'1991: Proceedings of the International Logic Programming Symposium, 518--532."},{"key":"e_1_2_1_38_1","volume-title":"CAV'1996: Computer Aided Verification. Lecture Notes in Computer Science","volume":"1102","author":"Sipma H.","unstructured":"Sipma , H. , Uribe , T. , and Manna , Z . 1996. Deductive model checking . In CAV'1996: Computer Aided Verification. Lecture Notes in Computer Science , vol. 1102 . Springer, Berlin, Germany, 208--219. Sipma, H., Uribe, T., and Manna, Z. 1996. Deductive model checking. In CAV'1996: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Germany, 208--219."},{"key":"e_1_2_1_39_1","series-title":"Lecture Notes in Computer Science","volume-title":"CAV'2004: Computer Aided Verification","author":"Tiwari A.","unstructured":"Tiwari , A. 2004. Termination of linear programs . In CAV'2004: Computer Aided Verification . Lecture Notes in Computer Science , vol. 3114 . Springer , Berlin, Germany , 70--82. Tiwari, A. 2004. Termination of linear programs. In CAV'2004: Computer Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer, Berlin, Germany, 70--82."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"},{"key":"e_1_2_1_43_1","volume-title":"ESOP'2003: European Symposium on Programming. Lecture Notes in Computer Science","volume":"2618","author":"Yahav E.","unstructured":"Yahav , E. , Reps , T. , Sagiv , M. , and Wilhelm , R . 2003. Verifying temporal heap properties specified via evolution logic . In ESOP'2003: European Symposium on Programming. Lecture Notes in Computer Science , vol. 2618 . Springer, Berlin, Germany, 204--222. Yahav, E., Reps, T., Sagiv, M., and Wilhelm, R. 2003. Verifying temporal heap properties specified via evolution logic. In ESOP'2003: European Symposium on Programming. Lecture Notes in Computer Science, vol. 2618. Springer, Berlin, Germany, 204--222."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1232420.1232422","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T19:06:11Z","timestamp":1672254371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1232420.1232422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,5]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,5]]}},"alternative-id":["10.1145\/1232420.1232422"],"URL":"https:\/\/doi.org\/10.1145\/1232420.1232422","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,5]]},"assertion":[{"value":"2007-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}