{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:19Z","timestamp":1775873599053,"version":"3.50.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>\n            A new method for software safety analysis is presented which uses program slicing and constraint solving to construct and analyze\n            <jats:italic>path conditions<\/jats:italic>\n            , conditions defined on a program's input variables which must hold for information flow between two points in a program. Path conditions are constructed from subgraphs of a program's dependence graph, specifically, slices and chops. The article describes how constraint solvers can be used to determine if a path condition is satisfiable and, if so, to construct a witness for a safety violation, such as an information flow from a program point at one security level to another program point at a different security level. Such a witness can prove useful in legal matters.The article reviews previous research on path conditions in program dependence graphs; presents new extensions of path conditions for arrays, pointers, abstract data types, and multithreaded programs; presents new decomposition formulae for path conditions; demonstrates how interval analysis and BDDs (binary decision diagrams) can be used to reduce the scalability problem for path conditions; and presents case studies illustrating the use of path conditions in safety analysis. Applying interval analysis and BDDs is shown to overcome the combinatorial explosion that can occur in constructing path conditions. Case studies and empirical data demonstrate the usefulness of path conditions for analyzing practical programs, in particular, how illegal influences on safety-critical programs can be discovered and analyzed.\n          <\/jats:p>","DOI":"10.1145\/1178625.1178628","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"410-457","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":106,"title":["Efficient path conditions in dependence graphs for software safety analysis"],"prefix":"10.1145","volume":"15","author":[{"given":"Gregor","family":"Snelting","sequence":"first","affiliation":[{"name":"Universit\u00e4t Passau, Passau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Torsten","family":"Robschink","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Passau, Passau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Krinke","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Passau, Passau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the ACM 4th Symposium on Testing, Analysis and Verification (TAV4). ACM Press","author":"Agrawal H.","year":"2080"},{"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 UK.   Baader F. and Nipkow T. 1998. Term rewriting and All That. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 29th ACM Symposium on Principles of Programming Languages. ACM Press, 1--4. 10","author":"Ball T."},{"key":"e_1_2_1_4_1","unstructured":"Bell D. and La Padula L. 1973. Secure computer systems: Mathematical foundations. MITRE Tech. rep. 2547.  Bell D. and La Padula L. 1973. Secure computer systems: Mathematical foundations. MITRE Tech. rep. 2547."},{"key":"e_1_2_1_5_1","unstructured":"Benhamou F. and Colmerauer A. 1993. Constraint Logic Programming: Selected Research. MIT Press Cambridge MA.   Benhamou F. and Colmerauer A. 1993. Constraint Logic Programming: Selected Research. MIT Press Cambridge MA."},{"key":"e_1_2_1_6_1","volume-title":"CS2000-0643","author":"Bent L."},{"key":"e_1_2_1_7_1","unstructured":"Bergstra J. Heering J. and Klint P. 1989. Algebraic specifications. ACM Press\/Addison Wesley CA.   Bergstra J. Heering J. and Klint P. 1989. Algebraic specifications. ACM Press\/Addison Wesley CA."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_9_1","volume-title":"Lecture Notes in Computer Science","volume":"892","author":"Burke M."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Canfora G. Cimitile A. a. De Lucia and Lucca G. 1998. Conditioned program slicing. Inform. Softw. Techn. 40 (Special Issue on Program Slicing). 595--607.  Canfora G. Cimitile A. a. De Lucia and Lucca G. 1998. Conditioned program slicing. Inform. Softw. Techn. 40 (Special Issue on Program Slicing). 595--607.","DOI":"10.1016\/S0950-5849(98)00086-X"},{"key":"e_1_2_1_12_1","unstructured":"Common Criteria Project Sponsoring Organizations. 2004. Common criteria for information technology security evaluation. CCIMB-2004-01-001 Version 2.2 Revision 2561 (Jan.).  Common Criteria Project Sponsoring Organizations. 2004. Common criteria for information technology security evaluation. CCIMB-2004-01-001 Version 2.2 Revision 2561 (Jan.)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.92910"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/261320.261324"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 22nd Symposium on Principles of Programming Languages (POPL'95)","author":"Field J.","year":"1994"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press. 10","author":"Foster J."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the Symposium on Security and Privacy. IEEE, 75--86","author":"Goguen J."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis. ACM Press, 80--94","author":"Goldberg A.","year":"1862"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis. ACM, 53--62","author":"Gotlieb A."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Symposium on Foundations of Software Engineering. ACM, 231--244","author":"Gupta N."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/77606.77608"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229545"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the SIGPLAN\/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. 35--42","author":"Krinke J.","year":"1998"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the International Conference on Software Maintenance. IEEE, 22--31","author":"Krinke J.","year":"2002"},{"key":"e_1_2_1_29_1","unstructured":"Krinke J. 2003a. Advanced slicing of sequential and concurrent programs. Ph.D. thesis Universit\u00e4t Passau.  Krinke J. 2003a. Advanced slicing of sequential and concurrent programs. Ph.D. thesis Universit\u00e4t Passau."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the FSE\/ESEC. ACM Press, 178--187","author":"Krinke J.","year":"2003"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:SQJO.0000039792.93414.a5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Krinke J. and Snelting G. 1998. Validation of measurement software as an application of slicing and constraint solving. Infor. Softw. Techn. (Special issue on Program Slicing). 661--675.  Krinke J. and Snelting G. 1998. Validation of measurement software as an application of slicing and constraint solving. Infor. Softw. Techn. (Special issue on Program Slicing). 661--675.","DOI":"10.1016\/S0950-5849(98)00090-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357071"},{"key":"e_1_2_1_34_1","volume-title":"Static Analysis Symposium. 280--301","author":"Lev-Ami T."},{"key":"e_1_2_1_35_1","unstructured":"Lind-Nielsen J. 2001. BuDDy---A binary decision diagram package. Tech. rep. University of Copenhagen. http:\/\/www.itu.dk\/reserach\/buddy.  Lind-Nielsen J. 2001. BuDDy---A binary decision diagram package. Tech. rep. University of Copenhagen. http:\/\/www.itu.dk\/reserach\/buddy."},{"key":"e_1_2_1_36_1","unstructured":"Mantel H. Stephan W. Ullmann M. and Vogt R. 2000. Leitfaden f\u00fcr die Erstellung und Pr\u00fcfung formaler Sicherheitsmodelle im Rahmen von ITSEC und Common Criteria. Tech. rep. Bundesamt f\u00fcr Sicherheit in der Informationstechnik und Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz. Version 0.8.  Mantel H. Stephan W. Ullmann M. and Vogt R. 2000. Leitfaden f\u00fcr die Erstellung und Pr\u00fcfung formaler Sicherheitsmodelle im Rahmen von ITSEC und Common Criteria. Tech. rep. Bundesamt f\u00fcr Sicherheit in der Informationstechnik und Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz. Version 0.8."},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Marriott K. and Stuckey P. 1998. Programming with Constraints. MIT Press Cambridge MA.  Marriott K. and Stuckey P. 1998. Programming with Constraints. MIT Press Cambridge MA.","DOI":"10.7551\/mitpress\/5625.001.0001"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/s100090050017","article-title":"PAG---An efficient program analyzer generator","volume":"2","author":"Martin F.","year":"1998","journal-title":"Int. J. Softw. Tools Techn. Transfer"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/76894.76897"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234744"},{"key":"e_1_2_1_41_1","volume-title":"Proceddings of the 6th ACM Symposium on Foundations of Software Engineering (FSE'98)","author":"Naumovich G."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/800020.808263"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/291889.291900"},{"key":"e_1_2_1_44_1","first-page":"627","article-title":"A way to simplify truth functions","volume":"62","author":"Quine W.","year":"1955","journal-title":"Amer. Mathemat. Soc."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/316686.316687"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Reps T. 1998. Program analysis via graph reachability. Inform. Softw. Techn. (Special issue on program slicing). 701--726.  Reps T. 1998. Program analysis via graph reachability. Inform. Softw. Techn. (Special issue on program slicing). 701--726.","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 2nd ACM SIGSOFT Symposium on the Foundations of Software Engineering (SIGSOFT '94)","author":"Reps T. W.","year":"1931"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the 3rd ACM SIGSOFT Symposium on the Foundations of Software Engineering (SIGSOFT '95)","author":"Reps T. W."},{"key":"e_1_2_1_50_1","unstructured":"Robschink T. 2005. Pfadbedingungen in Abh\u00e4ngigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik. Ph.D. thesis Universit\u00e4t Passau.  Robschink T. 2005. Pfadbedingungen in Abh\u00e4ngigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik. Ph.D. thesis Universit\u00e4t Passau."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the International ACM\/IEEE Conference on Software Engineering (ICSE'02)","author":"Robschink T."},{"key":"e_1_2_1_52_1","volume-title":"Compiler Construction: 7th International Conference (CC'98)","volume":"1383","author":"Rustan K."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 25th ACM Symposium on Principles of Programming Languages","author":"Smith G."},{"key":"e_1_2_1_55_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Static Analysis Symposium","author":"Snelting G."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/236114.236115"},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Sturm T. and Weispfenning V. 1996. Computational geometry problems in REDLOG. In Automated Deduction in Geometry. 58--86.   Sturm T. and Weispfenning V. 1996. Computational geometry problems in REDLOG. In Automated Deduction in Geometry. 58--86.","DOI":"10.1007\/BFb0022720"},{"key":"e_1_2_1_58_1","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/S0022-0000(74)80049-8","article-title":"Testing flow graph reducibility","volume":"9","author":"Tarjan R. E.","year":"1974","journal-title":"J. Comput. Syst. Science"},{"key":"e_1_2_1_59_1","unstructured":"Teitelbaum T. 2001. Code surfer user guide and reference. Tech. rep. Gramma Tech Product Documentation. http:\/\/www.grammatech.com\/csurf-doc\/manual.html.  Teitelbaum T. 2001. Code surfer user guide and reference. Tech. rep. Gramma Tech Product Documentation. http:\/\/www.grammatech.com\/csurf-doc\/manual.html."},{"key":"e_1_2_1_60_1","first-page":"3","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","journal-title":"J. Program. Lang."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1997.0122"},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the ACM SIGSAM International Symposium on Symbolic and Algebraic Computation (ISSAC '99)","author":"Weispfenning V.","year":"1999"},{"key":"e_1_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Wolfram S. 1999. The Mathematica Book. Wolfram Research.   Wolfram S. 1999. The Mathematica Book. Wolfram Research.","DOI":"10.1108\/aa.1999.19.1.77.1"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1178625.1178628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T18:11:39Z","timestamp":1672251099000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1178625.1178628"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":64,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1178625.1178628"],"URL":"https:\/\/doi.org\/10.1145\/1178625.1178628","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}