{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:02:49Z","timestamp":1773478969198,"version":"3.50.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_19","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"324-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Angelic Verification: Precise Verification Modulo Unknowns"],"prefix":"10.1007","author":[{"given":"Ankush","family":"Das","sequence":"first","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"767","DOI":"10.1007\/978-3-642-31424-7_62","volume-title":"Computer Aided Verification","author":"S Arlt","year":"2012","unstructured":"Arlt, S., Sch\u00e4f, M.: Joogie: infeasible code detection for java. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 767\u2013773. Springer, Heidelberg (2012)"},{"key":"19_CR2","unstructured":"Lahiri, S.K., Vaswani, K., Hoare, C.A.R.: Differential static analysis: opportunities, applications, and challenges. In: Proceedings of the Workshop on Future of Software Engineering Research, FoSER 2010, at the 18th ACM SIGSOFT, International Symposium on Foundations of Software Engineering, November 7-11, 2010, pp. 201\u20132014, Santa Fe, NM, USA (2010)"},{"issue":"7","key":"19_CR3","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Program Analysis For Software Tools and Engineering (PASTE 2005), pp. 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"19_CR5","unstructured":"Barnett, M., Qadeer, S.: BCT: a translator from MSIL to Boogie. In: Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (2012)"},{"issue":"2","key":"19_CR6","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A Bessey","year":"2010","unstructured":"Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66\u201375 (2010)","journal-title":"Commun. ACM"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Blackshear, S., Lahiri, S.K.: Almost-correct specifications: a modular semantic framework for assigning confidence to warnings. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 209\u2013218, Seattle, WA, USA, 16\u201319 Jun 2013","DOI":"10.1145\/2499370.2462188"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Bod\u00edk, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: Principles of Programming Languages (POPL 2010), pp. 339\u2013352 (2010)","DOI":"10.1145\/1707801.1706339"},{"issue":"7","key":"19_CR9","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"WR Bush","year":"2000","unstructured":"Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Softw. Pract. Exper. 30(7), 775\u2013802 (2000)","journal-title":"Softw. Pract. Exper."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 289\u2013300, Savannah, GA, USA, 21\u201323 Jan 2009","DOI":"10.1145\/1480881.1480917"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: Programming Language Design and Implementation (PLDI 2009), pp. 363\u2013374 (2009)","DOI":"10.1145\/1542476.1542517"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Chandra, S., Torlak, E., Barman, S., Bodik, R.: Angelic debugging. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 121\u2013130. ACM, New York, NY, USA (2011)","DOI":"10.1145\/1985793.1985811"},{"key":"19_CR13","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Proceedings of the 40th Design Automation Conference, DAC 2003, pp. 368\u2013371, Anaheim, CA, USA, 2\u20136 Jun 2003","DOI":"10.1145\/775832.775928"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Principles of Programming Languages (POPL 2009), pp. 302\u2013314 (2009)","DOI":"10.1145\/1594834.1480921"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation : a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Languages (POPL 1977), ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"19_CR17","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"issue":"8","key":"19_CR18","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: Programming Language Design and Implementation (PLDI 2007), pp. 435\u2013445 (2007)","DOI":"10.1145\/1250734.1250784"},{"key":"19_CR20","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, pp. 181\u2013192. ACM, New York, NY, USA, (2012)"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Chen, D.Y., Chou, A.: Bugs as inconsistent behavior: a general approach to inferring errors in systems code. In: Symposium on Operating Systems Principles (SOSP 2001), pp. 57\u201372 (2001)","DOI":"10.1145\/502059.502041"},{"key":"19_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer-Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"2\u20133","key":"19_CR23","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s10703-010-0102-0","volume":"37","author":"J Hoenicke","year":"2010","unstructured":"Hoenicke, J., Leino, K.R.M., Podelski, A., Sch\u00e4f, M., Wies, T.: Doomed program points. Form. Meth. Syst. Des. 37(2\u20133), 171\u2013199 (2010)","journal-title":"Form. Meth. Syst. Des."},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Path slicing. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pp. 38\u201347, Chicago, IL, USA, 12\u201315 Jun 2005","DOI":"10.1145\/1065010.1065016"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 437\u2013446, San Jose, CA, USA, 4\u20138 Jun 2011","DOI":"10.1145\/1993498.1993550"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Joshi, S., Lahiri, S.K., Lal, A.: Underspecified harnesses and interleaved bugs. In: Principles of Programming Languages (POPL 2012), pp. 19\u201330, ACM (2012)","DOI":"10.1145\/2103621.2103662"},{"key":"19_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/3-540-44898-5_16","volume-title":"Static Analysis Symposium","author":"T Kremenek","year":"2003","unstructured":"Kremenek, T., Engler, D.R.: Z-ranking: using statistical analysis to counter the impact of static analysis approximations. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 295\u2013315. Springer, Heidelberg (2003)"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC\/FSE 2013, pp. 345\u2013355, Saint Petersburg, Russian Federation, 18\u201326 Aug 2013","DOI":"10.1145\/2491411.2491452"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 493\u2013508. Springer, Heidelberg (2009)"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Lahiri, S.K., F\u00e4hndrich, M., Blackshear, S.: Verification modulo versions: towards usable verification. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, p. 32, Edinburgh, United Kingdom, 09\u201311 Jun 2014","DOI":"10.1145\/2594291.2594326"},{"key":"19_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"key":"19_CR34","unstructured":"Satisfiability modulo theories library (SMT-LIB). http:\/\/goedel.cs.uiowa.edu\/smtlib\/"},{"key":"19_CR35","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: IEEE Symposium of Logic in Computer Science (LICS 2001) (2001)"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: International Symposium on Software Testing and Analysis (ISSTA 2012) (2012)","DOI":"10.1145\/2338965.2336788"}],"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-319-21690-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T03:09:34Z","timestamp":1652843374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}