{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:27Z","timestamp":1762459347265,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662494974"},{"type":"electronic","value":"9783662494981"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_3","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"41-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach"],"prefix":"10.1007","author":[{"given":"Cl\u00e1udio","family":"Belo Louren\u00e7o","sequence":"first","affiliation":[]},{"given":"Maria Jo\u00e3o","family":"Frade","sequence":"additional","affiliation":[]},{"given":"Jorge","family":"Sousa Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90037-I","volume":"84","author":"P America","year":"1990","unstructured":"America, P., de Boer, F.: Proving total correctness of recursive procedures. Inf. Comput. 84(2), 129\u2013162 (1990)","journal-title":"Inf. Comput."},{"issue":"4","key":"3_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR3","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)"},{"key":"3_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108768.1108813","volume":"31","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. ACM SIGSOFT Softw. Eng. Notes 31(1), 82\u201387 (2006)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., M. Leino, K.R., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"3_CR7","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language. In: CEA LIST and INRIA (2010)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"1","key":"3_CR9","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"A Stephen","year":"1978","unstructured":"Stephen, A.: Cook: soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"key":"3_CR10","unstructured":"Correnson, L., Cuoq, P., Puccetti, A., Signoles, J.: Frama-C user manual (2010). http:\/\/frama-c.com"},{"issue":"4","key":"3_CR11","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. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer, Scholten (1990)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Proceedings of POpPL, pp. 193\u2013205. ACM (2001)","DOI":"10.1145\/373243.360220"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-1-84882-912-1_5","volume-title":"Reflections on the Work of C.A.R. Hoare: History of Computing","author":"M Gordon","year":"2010","unstructured":"Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare: History of Computing, pp. 101\u2013121. Springer, London (2010)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: Proceedings of FTfJP, pp. 6:1\u20136:7. ACM (2009)","DOI":"10.1145\/1557898.1557904"},{"issue":"10","key":"3_CR17","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"3_CR18","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Proceeedings of Symposium on Semantics of Algorithmic Languages","author":"CAR Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Proceeedings of Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188, pp. 102\u2013116. Springer, Heidelberg (1971)"},{"issue":"4","key":"3_CR19","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21 (2009)","journal-title":"ACM Comput. Surv."},{"issue":"5","key":"3_CR20","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11(5), 541\u2013566 (1999)","journal-title":"Formal Aspects Comput."},{"key":"3_CR21","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"505","volume-title":"Handbook of Satisfiability","author":"D Kroening","year":"2009","unstructured":"Kroening, D.: Software verification. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 505\u2013532. IOS Press, Amsterdam (2009)"},{"key":"3_CR22","unstructured":"Rustan, K., Leino, M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. In: Proceedings of ECOOP, pp. 110\u2013111. Springer (1999)"},{"issue":"6","key":"3_CR23","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K Rustan","year":"2005","unstructured":"Rustan, K., Leino, M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"3_CR24","unstructured":"Loureno, C.B., Frade, M.J., Pinto, J.S.: A single-assignment translation for annotated programs. ArXiv e-prints (2016). http:\/\/arxiv.org\/abs\/1601.00584"},{"issue":"1\u20132","key":"3_CR25","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Logic Algebraic Program. 58(1\u20132), 89\u2013106 (2004)","journal-title":"J. Logic Algebraic Program."},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"4","key":"3_CR27","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1278349.1278353","volume":"12","author":"P Vanbroekhoven","year":"2007","unstructured":"Vanbroekhoven, P., Janssens, G., Bruynooghe, M., Catthoor, F.: A practical dynamic single assignment transformation. ACM Trans. Des. Autom. Electron. Syst. 12(4), 40 (2007)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:35:13Z","timestamp":1748813713000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}