{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:44:47Z","timestamp":1757313887265},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540779643"},{"type":"electronic","value":"9783540779667"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77966-7_15","type":"book-chapter","created":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T03:59:24Z","timestamp":1201838364000},"page":"169-184","source":"Crossref","is-referenced-by-count":1,"title":["Exploiting Shared Structure in Software Verification Conditions"],"prefix":"10.1007","author":[{"given":"Domagoj","family":"Babi\u0107","sequence":"first","affiliation":[]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","first-page":"371","volume-title":"Computer Aided Verification","author":"D. Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 371\u2013383. Springer, Heidelberg (2007)"},{"key":"15_CR2","unstructured":"Babi\u0107, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Technical Report TR-2005-114, Microsoft Research Redmond (2005)"},{"key":"15_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11591191_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T. Ball","year":"2005","unstructured":"Ball, T., Lahiri, S.K., Musuvathi, M.: Zap: Automated theorem proving for software analysis. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 2\u201322. Springer, Heidelberg (2005)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, ACM SIGPLAN Notices, vol.\u00a036, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/11513988_45","volume-title":"Computer Aided Verification","author":"C.L. Conway","year":"2005","unstructured":"Conway, C.L., Namjoshi, K.S., Dams, D., Edwards, S.A.: Incremental Algorithms for Inter-procedural Analysis of Safety Properties. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 449\u2013461. Springer, Heidelberg (2005)"},{"key":"15_CR7","unstructured":"Detlefs, D., Nelson, G., Saxe, J.S.: Simplify: A Theorem Prover for Program Checking. Technical report, HP Laboratories Palo Alto, Technical Report HPL-2003-148 (2003)"},{"key":"15_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer, New York (1990)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"15_CR10","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. In: PLDI, ACM SIGPLAN Notices, pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/360204.360220","volume-title":"POPL","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: POPL, pp. 193\u2013205. ACM Press, New York (2001)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"15_CR13","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0743-1066(93)90018-C","volume":"15","author":"J.N. Hooker","year":"1993","unstructured":"Hooker, J.N.: Solving the incremental satisfiability problem. J. Log. Program.\u00a015(1-2), 177\u2013186 (1993)","journal-title":"J. Log. Program."},{"key":"15_CR14","first-page":"368","volume-title":"DAC","author":"D. Kroening","year":"2003","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. In: DAC, pp. 368\u2013371. ACM Press, New York (2003)"},{"issue":"6","key":"15_CR15","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":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/11575467_9","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 119\u2013134. Springer, Heidelberg (2005)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","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":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T. Lengauer","year":"1979","unstructured":"Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst.\u00a01(1), 121\u2013141 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR19","first-page":"530","volume-title":"DAC","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., et al.: Chaff: Engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"15_CR20","unstructured":"Nelson, G.: Techniques for program verification. PhD thesis, Stanford University (1979)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Prosser, R.T.: Applications of boolean matrices to the analysis of flow diagrams. In: Proceedings of the Eastern Joint Computer Conference, pp. 133\u2013138. Spartan Books (1959)","DOI":"10.1145\/1460299.1460314"},{"key":"15_CR22","first-page":"12","volume-title":"POPL","author":"B.K. Rosen","year":"1988","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: POPL, pp. 12\u201327. ACM Press, New York (1988)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11688839_2","volume-title":"Compiler Construction","author":"A. Rountev","year":"2006","unstructured":"Rountev, A., Kagan, S., Marlowe, T.J.: Interprocedural dataflow analysis in the presence of large libraries. In: Mycroft, A., Zeller, A. (eds.) CC 2006 and ETAPS 2006. LNCS, vol.\u00a03923, pp. 2\u201316. Springer, Heidelberg (2006)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C., Dill, D.: CVC: A Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"15_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1007\/3-540-45620-1_32","volume-title":"Automated Deduction - CADE-18","author":"A. Stump","year":"2002","unstructured":"Stump, A., Dill, D.L.: Faster Proof Checking in the Edinburgh Logical Framework. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 392\u2013407. Springer, Heidelberg (2002)"},{"key":"15_CR26","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":"15_CR27","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/1040305.1040334","volume-title":"POPL","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: POPL, pp. 351\u2013363. ACM Press, New York (2005)"},{"key":"15_CR28","first-page":"279","volume-title":"ICCAD","author":"L. Zhang","year":"2001","unstructured":"Zhang, L., et al.: Efficient conflict driven learning in a boolean satisfiability solver. In: ICCAD, pp. 279\u2013285. IEEE Press, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77966-7_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:57:24Z","timestamp":1619506644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77966-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540779643","9783540779667"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77966-7_15","relation":{},"subject":[]}}