{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,24]],"date-time":"2025-04-24T04:32:20Z","timestamp":1745469140272,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357459"},{"type":"electronic","value":"9783642357466"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35746-6_2","type":"book-chapter","created":{"date-parts":[[2012,12,14]],"date-time":"2012-12-14T01:38:40Z","timestamp":1355449120000},"page":"31-44","source":"Crossref","is-referenced-by-count":1,"title":["From Program to Logic: An Introduction"],"prefix":"10.1007","author":[{"given":"Patrice","family":"Godefroid","sequence":"first","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-540-78800-3_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Anand","year":"2008","unstructured":"Anand, S., Godefroid, P., Tillmann, N.: Demand-Driven Compositional Symbolic Execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 367\u2013381. Springer, Heidelberg (2008)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-73368-3_50","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2007","unstructured":"Ball, T., Kupferman, O., Sagiv, M.: Leaping Loops in the Presence of Abstraction. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 491\u2013503. Springer, Heidelberg (2007)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest Precondition of Unstructured Programs. In: Proceedings of PASTE 2005 (Program Analysis For Software Tools and Engineering), pp. 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of LICS 1990 (5th Symposium on Logic in Computer Science), Philadelphia, pp. 428\u2013439 (June 1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11537328_2","volume-title":"Model Checking Software","author":"C. Cadar","year":"2005","unstructured":"Cadar, C., Engler, D.: Execution Generated Test Cases: How to Make Systems Code Crash Itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 2\u201323. Springer, Heidelberg (2005)"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"2_CR7","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral Consistency of C and Verilog Programs using Bounded Model Checking. In: Design Automation Conference (DAC), pp. 368\u2013371. ACM (2003)","DOI":"10.21236\/ADA461052"},{"issue":"4","key":"2_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. Program. Lang. Syst. (TOPLAS)\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an Annotation Assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"2_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. In: Proceedings of PLDI 2002 (ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation), pp. 234\u2013245 (2002)","DOI":"10.1145\/512557.512558"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding Exponential Explosion: Generating Compact Verification Conditions. In: Proceedings of POPL 2001 (28th ACM Symposium on Principles of Programming Languages), pp. 193\u2013205 (2001)","DOI":"10.1145\/373243.360220"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning Meaning to Programs. In: Mathematical Aspects of Computer Science, pp. 19\u201332. XIX American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proceedings of POPL 1997 (24th ACM Symposium on Principles of Programming Languages), Paris, pp. 174\u2013186 (January 1997)","DOI":"10.1145\/263699.263717"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional Dynamic Test Generation. In: Proceedings of POPL 2007 (34th ACM Symposium on Principles of Programming Languages), Nice, pp. 47\u201354 (January 2007)","DOI":"10.1145\/1190216.1190226"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Higher-Order Test Generation. In: Proceedings of PLDI 2011 (ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation), San Jose, pp. 258\u2013269 (2011)","DOI":"10.1145\/1993316.1993529"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed Automated Random Testing. In: Proceedings of PLDI 2005 (ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation), Chicago, pp. 213\u2013223 (June 2005)","DOI":"10.1145\/1065010.1065036"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Levin, M., Molnar, D.: Active Property Checking. In: Proceedings of EMSOFT 2008 (8th Annual ACM & IEEE Conference on Embedded Software), Atlanta, pp. 207\u2013216. ACM Press (October 2008)","DOI":"10.1145\/1450058.1450087"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Luchaup, D.: Automatic Partial Loop Summarization in Dynamic Test Generation. In: Proceedings of ISSTA 2011 (ACM SIGSOFT International Symposium on Software Testing and Analysis), Toronto, pp. 23\u201333 (July 2011)","DOI":"10.1145\/2001420.2001424"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A., Rajamani, S., Tetali, S.: Compositional Must Program Analysis: Unleashing The Power of Alternation. In: Proceedings of POPL 2010 (37th ACM Symposium on Principles of Programming Languages), Madrid, pp. 43\u201355 (January 2010)","DOI":"10.1145\/1706299.1706307"},{"issue":"10","key":"2_CR22","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Approach to Computer Programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"issue":"7","key":"2_CR23","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic Execution and Program Testing. Journal of the ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Journal of the ACM"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Korel, B.: A Dynamic Approach of Test Data Generation. In: IEEE Conference on Software Maintenance, San Diego, pp. 311\u2013317 (November 1990)","DOI":"10.1109\/ICSM.1990.131379"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-24732-6_13","volume-title":"Model Checking Software","author":"C.S. P\u0103s\u0103reanu","year":"2004","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: Verification of Java Programs Using Symbolic Execution and Invariant Generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 164\u2013181. Springer, Heidelberg (2004)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A Concolic Unit Testing Engine for C. In: Proceedings of FSE 2005 (13th International Symposium on the Foundations of Software Engineering) (September 2005)","DOI":"10.21236\/ADA482657"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013White Box Test Generation for.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-19835-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tsitovich","year":"2011","unstructured":"Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop Summarization and Termination Analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 81\u201395. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Tools for Practical Software Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35746-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T17:53:53Z","timestamp":1745430833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35746-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642357459","9783642357466"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35746-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}