{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:25:23Z","timestamp":1757312723077},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_41","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T18:29:34Z","timestamp":1188412174000},"page":"366-378","source":"Crossref","is-referenced-by-count":24,"title":["Structural Abstraction of Software Verification Conditions"],"prefix":"10.1007","author":[{"given":"Domagoj","family":"Babi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"41_CR1","unstructured":"Babi\u0107, D., Hu, A.: Fast Symbolic Execution for Static Checking (submitted for publication)"},{"key":"41_CR2","unstructured":"Babi\u0107, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Technical Report TR-2005-114, Microsoft Research Redmond (2005)"},{"key":"41_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic Predicate Abstraction of C Programs. Programming Language Design and Implementation, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. Programming Language Design and Implementation, pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"issue":"8","key":"41_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"41_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conference, pp. 368\u2013371 (2003)","DOI":"10.21236\/ADA461052"},{"key":"41_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"4","key":"41_CR9","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans Programming Languages and Systems\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Trans Programming Languages and Systems"},{"volume-title":"Predicate Calculus and Program Semantics","year":"1990","key":"41_CR10","unstructured":"Dijkstra, E.W., Scholten, C.S. (eds.): Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)"},{"key":"41_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. Programming Language Design and Implementation, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. Principles of Programming Languages, pp. 193\u2013205 (2001)","DOI":"10.1145\/360204.360220"},{"key":"41_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"41_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. Principles of Programming Languages, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"41_CR17","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/CGO.2004.1281665","volume-title":"CGO 2004","author":"C. Lattner","year":"2004","unstructured":"Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: CGO 2004. Proceedings of the International Symposium on Code Generation and Optimization, p. 75. IEEE Computer Society, Washington, DC, USA (2004)"},{"key":"41_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"European Symposium on Programming","author":"K.R.M. Leino","year":"2006","unstructured":"Leino, K.R.M., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"issue":"6","key":"41_CR19","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett.\u00a093(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"41_CR20","doi-asserted-by":"crossref","unstructured":"Livshits, V.B., Lam, M.S.: Tracking Pointers with Path and Context Sensitivity for Bug Detection in C Programs. In: European Software Engineering Conference\/International Symposium on Foundations of Software Engineering, pp. 317\u2013326 (2003)","DOI":"10.1145\/940071.940114"},{"key":"41_CR21","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. Principles of Programming Languages, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"41_CR22","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970","author":"G.S. Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. Programming Language Design and Implementation, pp. 131\u2013144 (2004)","DOI":"10.1145\/996841.996859"},{"key":"41_CR24","doi-asserted-by":"crossref","unstructured":"Wilson, C., Dill, D.L.: Reliable verification using symbolic simulation with scalar values. In: 37th Design Automation Conference, pp. 124\u2013129. ACM\/IEEE (2000)","DOI":"10.1145\/337292.337336"},{"key":"41_CR25","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. Principles of Programming Languages, pp. 351\u2013363 (2005)","DOI":"10.1145\/1040305.1040334"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:08:35Z","timestamp":1619503715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_41","relation":{},"subject":[]}}