{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T13:07:42Z","timestamp":1777640862692,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642338250","type":"print"},{"value":"9783642338267","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33826-7_16","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T22:46:25Z","timestamp":1348613185000},"page":"233-247","source":"Crossref","is-referenced-by-count":244,"title":["Frama-C"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Cuoq","sequence":"first","affiliation":[]},{"given":"Florent","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Signoles","sequence":"additional","affiliation":[]},{"given":"Boris","family":"Yakobowski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"16_CR1","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1002\/stvr.423","volume":"21","author":"S. Bardin","year":"2011","unstructured":"Bardin, S., Herrmann, P.: OSMOSE: automatic structural testing of executables. Software Testing, Verification and Reliability\u00a021(1), 29\u201354 (2011)","journal-title":"Software Testing, Verification and Reliability"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-18275-4_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Bardin","year":"2011","unstructured":"Bardin, S., Herrmann, P., V\u00e9drine, F.: Refinement-Based CFG Reconstruction from Unstructured Programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 54\u201369. Springer, Heidelberg (2011)"},{"key":"16_CR3","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C Specification Language Preliminary design, version 1.5 (2010), http:\/\/frama-c.com\/downloads\/acsl_1.5.pdf"},{"issue":"4","key":"16_CR4","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1109\/TSE.2010.49","volume":"36","author":"N. Beckman","year":"2010","unstructured":"Beckman, N., et al.: Proofs from tests. IEEE Trans. Software Eng.\u00a036(4), 495\u2013508 (2010)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Berthom\u00e9, P., et al.: Attack model for verification of interval security properties for smart card c codes. In: PLAS, pp. 2:1\u20132:12. ACM (2010)","DOI":"10.1145\/1814217.1814219"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving Pointer Programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)","DOI":"10.1007\/10722010_8"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Botella, B., et al.: Automating structural testing of C programs: Experience with PathCrawler. In: AST, pp. 70\u201378 (2009)","DOI":"10.1109\/IWAST.2009.5069043"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., et al.: On inter-procedural analysis of programs with lists and data. In: PLDI, pp. 578\u2013589 (2011)","DOI":"10.1145\/1993498.1993566"},{"issue":"3","key":"16_CR9","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"Software Tools for Technology Transfer"},{"key":"16_CR10","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Ceara, D., Mounier, L., Potet, M.-L.: Taint dependency sequences: A characterization of insecure execution paths based on input-sensitive cause sequences. In: ICSTW, Washington, DC, USA, pp. 371\u2013380 (2010)","DOI":"10.1109\/ICSTW.2010.28"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Chatzieleftheriou, G., Katsaros, P.: Test-driving static analysis tools in search of C code vulnerabilities. In: COMPSAC Workshops, pp. 96\u2013103. IEEE (2011)","DOI":"10.1109\/COMPSACW.2011.26"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Chebaro, O., et al.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC (to appear, 2012)","DOI":"10.1145\/2245276.2231980"},{"key":"16_CR14","unstructured":"Conchon, S., et al.: The Alt-Ergo Automated Theorem Prover, http:\/\/alt-ergo.lri.fr"},{"key":"16_CR15","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual, v8.3 edition (2011), http:\/\/coq.inria.fr\/"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-32469-7_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"L. Correnson","year":"2012","unstructured":"Correnson, L., Signoles, J.: Combining Analyses for C Program Verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol.\u00a07437, pp. 108\u2013130. Springer, Heidelberg (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)","DOI":"10.1145\/512950.512973"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Cuoq, P., et al.: Experience report: OCaml for an industrial-strength static analysis framework. In: ICFP, pp. 281\u2013286. ACM (2009)","DOI":"10.1145\/1631687.1596591"},{"key":"16_CR20","unstructured":"Delmas, D., et al.: Taster, a Frama-C plug-in to encode Coding Standards. In: ERTSS (May 2010)"},{"key":"16_CR21","unstructured":"Delmas, D., et al.: Fan-C, a Frama-C plug-in for data flow verification. In: ERTSS (2012)"},{"key":"16_CR22","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., 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_CR23","doi-asserted-by":"crossref","unstructured":"Demay, J.-C., Totel, E., Tronel, F.: Sidan: A tool dedicated to software instrumentation for detecting attacks on non-control-data. In: CRiSIS (October 2009)","DOI":"10.1109\/CRISIS.2009.5411977"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: A constructive approach to program correctness. BIT Numerical Mathematics. Springer (1968)","DOI":"10.1007\/BF01933419"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., et al.: VCC: Contract-based modular verification of concurrent C. In: ICSE Companion. IEEE (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"issue":"3","key":"16_CR26","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J. Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst.\u00a09(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR27","unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics\u00a019 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-53982-4_10","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development","author":"P. Granger","year":"1991","unstructured":"Granger, P.: Static Analysis of Linear Congruence Equalities Among Variables of a Program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 169\u2013192. Springer, Heidelberg (1991)"},{"key":"16_CR31","unstructured":"Groslambert, J., Stouls, N.: V\u00e9rification de propri\u00e9t\u00e9s LTL sur des programmes C par g\u00e9n\u00e9ration d\u2019annotations. In: AFADL (2009) (in French)"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10) (1969)","DOI":"10.1145\/363235.363259"},{"issue":"7","key":"16_CR33","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1145\/960116.53994","volume":"23","author":"S. Horwitz","year":"1988","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. PLDI, SIGPLAN Notices\u00a023(7), 35\u201346 (1988)","journal-title":"PLDI, SIGPLAN Notices"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"IEEE Std 754-2008. IEEE standard for floating-point arithmetic. Technical report (2008), http:\/\/dx.doi.org\/10.1109\/IEEESTD.2008.4610935","DOI":"10.1109\/IEEESTD.2008.4610935"},{"key":"16_CR35","unstructured":"ISO\/IEC JTC1\/SC22\/WG14. 9899:TC3: Programming Languages\u2014C (2007), http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1256.pdf"},{"key":"16_CR36","unstructured":"Kosmatov, N.: Online version of PathCrawler, http:\/\/pathcrawler-online.com\/"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Kosmatov, N.: XI: Constraint-Based Techniques for Software Testing. In: Artificial Intelligence Applications for Improved Software Engineering Development: New Prospects, IGI Global (2010)","DOI":"10.4018\/978-1-60566-758-4.ch011"},{"key":"16_CR38","unstructured":"Leino, K.R.M.: This is Boogie 2. Microsoft Research (2008)"},{"key":"16_CR39","unstructured":"March\u00e9, C., Moy, Y.: The Jessie plugin for Deduction Verification in Frama-C, version 2.30. INRIA (2012), http:\/\/krakatoa.lri.fr\/jessie.pdf"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Marre, B., Arnould, A.: Test sequences generation from Lustre descriptions: GATeL. In: ASE, Grenoble, France, pp. 229\u2013237 (September 2000)","DOI":"10.1109\/ASE.2000.873667"},{"key":"16_CR41","unstructured":"MathWorks. Polyspace, http:\/\/www.mathworks.com\/products\/polyspace"},{"key":"16_CR42","unstructured":"Meyer, B.: Object-oriented Software Construction. Prentice-Hall (1997)"},{"key":"16_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: CC 2002. LNCS, vol.\u00a02304, p. 213. Springer, Heidelberg (2002)"},{"key":"16_CR44","unstructured":"Pariente, D., Ledinot, E.: Formal Verification of Industrial C Code using Frama-C: a Case Study. In: FoVeOOS (2010)"},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1798","DOI":"10.1007\/3-540-48118-4_45","volume-title":"FM\u201999 - Formal Methods","author":"F. Randimbivololona","year":"1999","unstructured":"Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, J., Schoen, D.: Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1798\u20131815. Springer, Heidelberg (1999)"},{"issue":"1-2","key":"16_CR47","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1017\/S1471068411000469","volume":"12","author":"J. Schimpf","year":"2011","unstructured":"Schimpf, J., Shen, K.: ECLiPSe - from LP to CLP. Theory and Practice of Logic Programming\u00a012(1-2), 127\u2013156 (2011)","journal-title":"Theory and Practice of Logic Programming"},{"key":"16_CR48","unstructured":"Signoles, J.: Foncteurs imp\u00e9ratifs et compos\u00e9s: la notion de projet dans Frama-C. In: JFLA, Studia Informatica Universalis, vol.\u00a07(2) (2009) (in French)"},{"key":"16_CR49","unstructured":"Signoles, J., Correnson, L., Prevosto, V.: Frama-C Plug-in Development Guide (October 2011), http:\/\/frama-c.com\/download\/plugin-developer.pdf"},{"key":"16_CR50","unstructured":"Stouls, N., Prevosto, V.: Aora\u00ed plug-in tutorial, version Nitrogen-20111001 (October 2011), http:\/\/frama-c.com\/download\/frama-c-aorai-manual.pdf"},{"key":"16_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11408901_21","volume-title":"Dependable Computing - EDCC 2005","author":"N. Williams","year":"2005","unstructured":"Williams, N., Marre, B., Mouy, P., Roger, M.: PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis. In: Dal Cin, M., Ka\u00e2niche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol.\u00a03463, pp. 281\u2013292. Springer, Heidelberg (2005)"},{"key":"16_CR52","unstructured":"Yakobowski, B., et al.: Formal verification of software important to safety using the Frama-C tool suite. In: NPIC (July 2012)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33826-7_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,29]],"date-time":"2022-01-29T15:55:51Z","timestamp":1643471751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33826-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642338250","9783642338267"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}