{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T06:39:14Z","timestamp":1761979154566,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642541070"},{"type":"electronic","value":"9783642541087"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_16","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T10:09:36Z","timestamp":1389780576000},"page":"304-325","source":"Crossref","is-referenced-by-count":3,"title":["Result Certification of Static Program Analysers with Automated Theorem Provers"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Emmanuel","family":"Cornilleau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: Verified resource guarantees using COSTA and KeY. In: PEPM 2011, SIGPLAN, pp. 73\u201376. ACM (2011)","DOI":"10.1145\/1929501.1929513"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: LICS 2001, pp. 247\u2013256. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"16_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., Leino, K.R.M.: 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.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"16_CR5","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., Leino, K.R.M., 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.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: Cvc3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"16_CR7","unstructured":"Besson, F., Cornilleau, P.-E., Jensen, T.: Why3 and Coq source of the development (2012), http:\/\/www.irisa.fr\/celtique\/ext\/chk-sa"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-25379-9_13","volume-title":"Certified Programs and Proofs","author":"F. Besson","year":"2011","unstructured":"Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 151\u2013166. Springer, Heidelberg (2011)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-642-15640-3_17","volume-title":"Trustworthly Global Computing","author":"F. Besson","year":"2010","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Certified result checking for polyhedral analysis of bytecode programs. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010, LNCS, vol.\u00a06084, pp. 253\u2013267. Springer, Heidelberg (2010)"},{"key":"16_CR10","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011, pp. 53\u201364 (2011)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T. Bouton","year":"2009","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: VeriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"issue":"1","key":"16_CR13","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.tcs.2005.06.004","volume":"342","author":"D. Cachera","year":"2005","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theoretical Computer Science\u00a0342(1), 56\u201378 (2005)","journal-title":"Theoretical Computer Science"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Chlipala, A., Necula, G.C., Schneck, R.R.: The Open Verifier framework for foundational verifiers. In: TLDI 2005, pp. 1\u201312. ACM (2005)","DOI":"10.1145\/1040294.1040295"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"16_CR16","unstructured":"Cornilleau, P.-E.: Prototyping static analysis certification using Why3. In: Boogie 2012 (2012)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-17164-2_8","volume-title":"Programming Languages and Systems","author":"D. Demange","year":"2010","unstructured":"Demange, D., Jensen, T.P., Pichardie, D.: A provably correct stackless intermediate representation for java bytecode. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 97\u2013113. Springer, Heidelberg (2010)"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA 2003, pp. 302\u2013312 (2003)","DOI":"10.1145\/949343.949332"},{"key":"16_CR21","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":"16_CR22","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 2002, pp. 234\u2013245. ACM (2002)","DOI":"10.1145\/512529.512558"},{"key":"16_CR23","unstructured":"Fontaine, P.: Combinations of Theories and the Bernays-Sch\u00f6nfinkel-Ramsey Class. In: VERIFY. CEUR Workshop Proceedings, vol.\u00a0259. CEUR-WS.org (2007)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-18070-5_7","volume-title":"Formal Verification of Object-Oriented Software","author":"L. Hubert","year":"2011","unstructured":"Hubert, L., Barr\u00e9, N., Besson, F., Demange, D., Jensen, T.P., Monfort, V., Pichardie, D., Turpin, T.: Sawja: Static analysis workshop for java. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 92\u2013106. Springer, Heidelberg (2011)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-68863-1_9","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"L. Hubert","year":"2008","unstructured":"Hubert, L., Jensen, T., Pichardie, D.: Semantic foundations and inference of non-null annotations. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 132\u2013149. Springer, Heidelberg (2008)"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"issue":"3","key":"16_CR27","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified bytecode verifiers. Theoretical Computer Science\u00a0298(3), 583\u2013626 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"3-4","key":"16_CR28","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1025055424017","volume":"30","author":"X. Leroy","year":"2003","unstructured":"Leroy, X.: Java bytecode verification: Algorithms and formalizations. Journal of Automated Reasoning\u00a030(3-4), 235\u2013269 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"16_CR30","unstructured":"Lindholm, T., Yellin, F.: Java Virtual Machine Specification, 2nd edn. Addison-Wesley Longman Publishing Co., Inc. (1999)"},{"key":"16_CR31","unstructured":"March\u00e9, C., Tafat, A.: Weakest Precondition Calculus, Revisited using Why3. Research report RR-8185, INRIA (December 2012)"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997, pp. 106\u2013119. ACM (1997)","DOI":"10.1145\/263699.263712"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10721959_3","volume-title":"Automated Deduction - CADE-17","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C., Lee, P.: Proof generation in the Touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 25\u201344. Springer, Heidelberg (2000)"},{"key":"16_CR34","unstructured":"Pichardie, D.: Interpr\u00e9tation abstraite en logique intuitionniste: extraction d\u2019analyseurs Java certifi\u00e9s. PhD thesis, Universit\u00e9 Rennes 1 (2005) (in French)"},{"issue":"4","key":"16_CR35","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R. Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reasoning\u00a044(4), 401\u2013424 (2010)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"16_CR36","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/AIC-2010-0483","volume":"24","author":"G. Sutcliffe","year":"2011","unstructured":"Sutcliffe, G.: The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5. AI Communications\u00a024(1), 75\u201389 (2011)","journal-title":"AI Communications"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-540-70592-5_28","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"E. Tempero","year":"2008","unstructured":"Tempero, E., Boyland, J., Melton, H.: How do java programs use inheritance? an empirical study of inheritance in java software. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 667\u2013691. Springer, Heidelberg (2008)"},{"issue":"6","key":"16_CR38","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H. Wasserman","year":"1997","unstructured":"Wasserman, H., Blum, M.: Software reliability via run-time result-checking. Journal of the ACM\u00a044(6), 826\u2013849 (1997)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T14:49:55Z","timestamp":1746110995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}