{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T13:47:07Z","timestamp":1772113627102,"version":"3.50.1"},"reference-count":100,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T00:00:00Z","timestamp":1430438400000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.<\/jats:p>","DOI":"10.1007\/s00165-014-0326-7","type":"journal-article","created":{"date-parts":[[2015,1,8]],"date-time":"2015-01-08T12:12:36Z","timestamp":1420719156000},"page":"573-609","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":260,"title":["Frama-C: A software analysis perspective"],"prefix":"10.1145","volume":"27","author":[{"given":"Florent","family":"Kirchner","sequence":"first","affiliation":[{"name":"CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[{"name":"CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France"}]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[{"name":"CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France"}]},{"given":"Julien","family":"Signoles","sequence":"additional","affiliation":[{"name":"CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France"}]},{"given":"Boris","family":"Yakobowski","sequence":"additional","affiliation":[{"name":"CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Ayache N Amadio R R\u00e9gis-Gianas Y (2012) Certifying and reasoning on cost annotations in C programs. In: 17th International workshop on formal methods for industrial critical systems (FMICS 2012)","DOI":"10.1007\/978-3-642-32469-7_3"},{"key":"e_1_2_1_2_2_2","unstructured":"Adelard LLP Simple concurrency analysis plugin for Frama-C. https:\/\/bitbucket.org\/adelard\/simple-concurrency\/"},{"key":"e_1_2_1_2_3_2","first-page":"231","volume-title":"The 28th IFIP TC-11 international information security and privacy conference (SEC 2013)","author":"Assaf M","year":"2013"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bishop P Bloomfield R Cyra L (2013) Combining testing and proof to gain high assurance in software: a case study. In: Proceedings of IEEE international symposium on software reliability engineering (ISSRE)","DOI":"10.1109\/ISSRE.2013.6698924"},{"issue":"1","key":"e_1_2_1_2_5_2","first-page":"5","article-title":"A mergeable interval map","volume":"9","author":"Bonichon R","year":"2011","journal-title":"Studia Informatica Universalis"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Barnett M Evan Chang B-Y DeLine R Jacobs B Rustan K Leino M (2006) Boogie: A modular reusable verifier for object-oriented programs. In: Proceedings of 4th international symposium on formal methods components and objects (FMCO 2005) volume 4111 of LNCS. Springer Berlin","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A Dragoi C Enea C Sighireanu M (2011) On inter-procedural analysis of programs with lists and data. In: The 32nd ACM SIGPLAN conference on programming language design and implementation (PLDI 2011) ACM pp 578\u2013589","DOI":"10.1145\/1993316.1993566"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Botella B Delahaye M Hong-Tuan-Ha S Kosmatov N Mouy P Roger M Williams N (2009) Automating structural testing of C programs: experience with PathCrawler. In: The 4th international workshop on automation of software test (AST 2009) IEEE Computer Society pp 70\u201378","DOI":"10.1109\/IWAST.2009.5069043"},{"key":"e_1_2_1_2_10_2","unstructured":"Baudin P Filli\u00e2tre J-C Hubert T March\u00e9 C Monate B Moy Y Prevosto V (2013) ACSL: ANSI\/ISO C specification language v1.6 April 2013. http:\/\/frama-c.com\/acsl.html"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.423"},{"issue":"5","key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker Blast: applications to software engineering","volume":"9","author":"Beyer D","year":"2007","journal-title":"Int J Softw Tools Technol Transf"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Berthom\u00e9 P Heydemann K Kauffmann-Tourkestansky X Lalande J-F (2010) Attack model for verification of interval security properties for smart card C codes. In: The 5th ACM SIGPLAN workshop on programming languages and analysis for security (PLAS 2010) ACM pp 1\u201312","DOI":"10.1145\/1814217.1814219"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Bardin S Herrmann P V\u00e9drine F (2011) Refinement-based CFG reconstruction from unstructured programs. In: The 12th international conference on verification model checking and abstract interpretation (VMCAI 2011) volume 6538 of LNCS. Springer pp 54\u201369","DOI":"10.1007\/978-3-642-18275-4_6"},{"key":"e_1_2_1_2_15_2","unstructured":"Black Paul E (2014) SATE V Ockham sound analysis criteria. http:\/\/samate.nist.gov\/SATE5Workshop.html"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.49"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Bornat R (2000) Proving pointer programs in Hoare logic. In: The 5th international conference on mathematics of program construction (MPC 2000) volume 1837 of LNCS. Springer","DOI":"10.1007\/10722010_8"},{"key":"e_1_2_1_2_18_2","first-page":"23","article-title":"Some techniques for proving correctness of programs which alter data structures","volume":"7","author":"Burstall RM","year":"1972","journal-title":"Mach Intell"},{"key":"e_1_2_1_2_19_2","unstructured":"Conchon S et\u00a0al The Alt-Ergo automated theorem prover http:\/\/alt-ergo.lri.f.."},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: The 4th symposium on principles of programming languages (POPL 1977) pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R Feret J Mauborgne L Min\u00e9 A Monniaux D Rival X (2005) The ASTR\u00c9E analyzer. In: The 14th European symposium on programming (ESOP 2005) part of the joint European conferences on theory and practice of software (ETAPS 2005) volume 3444 of LNCS. Springer Berlin pp 21\u201330","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Chebaro O Cuoq P Kosmatov N Marre B Pacalet A Williams N Yakobowski B (2013) Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom Softw Eng. Published online","DOI":"10.1007\/s10515-013-0127-x"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Cuoq P Doligez D (2008) Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in OCaml 3.10.2.. In: Proceedings of the ACM SigPlan ML workshop pp 13\u201322","DOI":"10.1145\/1411304.1411308"},{"key":"e_1_2_1_2_24_2","unstructured":"Cuoq P Delmas D Duprat S Moya Lamiel V (2012) Fan-C a Frama-C plug-in for data flow verification. In: The embedded real-time software and systems congress (ERTS 2 2012)"},{"key":"e_1_2_1_2_25_2","unstructured":"Cuoq P Doligez D Signoles J (2011) Lightweight typed customizable unmarshaling. In: ACM SIGPLAN Workshop on ML. ACM"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Cuoq P Hilsenkopf P Kirchner F Labb\u00e9 S Thuy N Yakobowski B (2012) Formal verification of software important to safety using the Frama-C tool suite. In: The 8th international conference on nuclear plant instrumentation and control (NPIC 2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Cruanes S Hamon G Owre S Shankar N (2013) Tool integration with the evidential tool bus. In: Proceedings of verification model-checking and abstract interpretation (VMCAI) volume 7737 of LNCS pp 275\u2013294","DOI":"10.1007\/978-3-642-35873-9_18"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Cok David R Kiniry Joseph R (2004) ESC\/Java2: uniting ESC\/Java and JML. In: The international workshop on construction and analysis of safe secure and interoperable smart devices (CASSIS 2004) volume 3362 of LNCS. Springer pp 108\u2013128","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Chatzieleftheriou G Katsaros P (2011) Test-driving static analysis tools in search of C code vulnerabilities. In: COMPSAC workshops. IEEE Computer Society pp 96\u2013103","DOI":"10.1109\/COMPSACW.2011.26"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Chebaro O Kosmatov N Giorgetti A Julliand J (2012) Program slicing enhances a verification technique combining static and dynamic analysis. In: The ACM symposium on applied computing (SAC 2012) ACM pp 1284\u20131291","DOI":"10.1145\/2245276.2231980"},{"key":"e_1_2_1_2_31_2","unstructured":"Comar C Kanig J Moy Y (2012) Integrating formal program verification with testing. In: Proceedings of ERTS 2012"},{"key":"e_1_2_1_2_32_2","unstructured":"Clang Static Analyzer. http:\/\/clang-analyzer.llvm.org\/"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Ceara D Mounier L Potet M-L (2010) Taint dependency sequences: a characterization of insecure execution paths based on input-sensitive cause sequences. In: The 3rd international conference on software testing verification and validation workshops (ICSTW 2010) pp 371\u2013380","DOI":"10.1109\/ICSTW.2010.28"},{"key":"e_1_2_1_2_34_2","unstructured":"Coq Development Team (2011) The Coq proof assistant reference manual v8.3 edition. http:\/\/coq.inria.fr\/"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127900"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.602"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Csallner C Smaragdakis Y (2006) Dynamically discovering likely interface invariants. In: The 28th ACM\/IEEE international conference on software engineering (ICSE 2006) Emerging Results Track ACM pp 861\u2013864","DOI":"10.1145\/1134285.1134435"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Correnson L Signoles J (2012) Combining analyses for C programverification. In: The 17th internationalworkshop on formal methods for industrial critical systems (FMICS 2012)","DOI":"10.1007\/978-3-642-32469-7_8"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Cuoq P Signoles J Baudin P Bonichon R Canet G Correnson L Monate B Prevosto V Puccetti A (2009) Experience report: OCaml for an industrial-strength static analysis framework. In: The 14th ACM SIGPLAN international conference on functional programming (ICFP 2009) ACM pp 281\u2013286","DOI":"10.1145\/1631687.1596591"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Cuoq P Yakobowski B Prevosto V (2013) Frama-C\u2019s value analysis plug-in fluorine-20130601 edition. June http:\/\/frama-c.com\/download\/frama-c-value-analysis.pdf","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_2_1_2_41_2","unstructured":"Delmas D Duprat S Moya Lamiel V Signoles J (2010) Taster a Frama-C plug-in to encode coding standards. In: The embedded real-time software and systems congress (ERTS 2 )"},{"key":"e_1_2_1_2_42_2","unstructured":"Dross C Efstathopoulos P Lesens D Mentr\u00e9 D Moy Y (2014) Rail space security: three case studies for spark 2014. In: Proceedings of ERTS 2014"},{"key":"e_1_2_1_2_43_2","volume-title":"A constructive approach to program correctness","author":"Dijkstra EW","year":"1968"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Demange D Jensen T Pichardie D (2010) A provably correct stackless intermediate representation for java bytecode. In: The 8th Asian symposium on programming languages and systems (APLAS 2010) volume 6461 of LNCS. Springer pp 97\u2013113","DOI":"10.1007\/978-3-642-17164-2_8"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Delahaye M Kosmatov N Signoles J (2013) Common specification language for static and dynamic analysis of C programs. In: The 28th annual ACM symposium on applied computing (SAC) ACM pp 1230\u20131235","DOI":"10.1145\/2480362.2480593"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Dahlweid M Moskal M Santen T Tobies S Schulte W (2009) VCC: Contract-based modular verification of concurrent C. In: ICSE Companion IEEE Computer Society pp 429\u2013430","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Demay J-C Totel E Tronel F (2009) SIDAN: a tool dedicated to software instrumentation for detecting attacks on non-control-data. In: CRiSIS","DOI":"10.1109\/CRISIS.2009.5411977"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2011.06.003"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_2_50_2","unstructured":"Filli\u00e2tre Jean-Christophe (2000) Hash consing in an ML framework. Research Report 1368 LRI Universit\u00e9 Paris Sud"},{"key":"e_1_2_1_2_51_2","unstructured":"Filli\u00e2tre J-C (2003) Why: a multi-language multi-prover verification tool. Research Report 1366 LRI Universit\u00e9 Paris Sud"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Floyd RW (1967) Assigning meanings to programs. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics vol 19","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C March\u00e9 C (2007) The why\/krakatoa\/caduceus platform for deductive program verification. In: CAV volume 4590 of LNCS. Springer pp 173\u2013177","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J-C Paskevich A (2013) Why3\u2014where programs meet provers. In: The 22nd European symposium on programming (ESOP 2013) volume 7792 of LNCS. Springer","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2008.109"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Giorgetti A Groslambert J Julliand J Kouchnarenko O (2008) Verification of class liveness properties with Java Modeling Language. IET Softw 2(6)","DOI":"10.1049\/iet-sen:20080008"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Gulavani Bhargav S Henzinger Thomas A Kannan Y Nori Aditya V Rajamani Sriram K (2006) SYNERGY: a new algorithm for property checking. In: The 14th ACM SIGSOFT international symposium on foundations of software engineering (FSE 2006) ACM pp 117\u2013127","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_2_1_2_59_2","unstructured":"Gmp: Gnu multiple precision arithmetic library. http:\/\/gmplib.org\/"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Gastin P Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: The 13th international conference on computer aided verification (CAV 2001) volume 2102 of LNCS. Springer pp 53\u201365","DOI":"10.1007\/3-540-44585-4_6"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Granger P (1991) Static analysis of linear congruence equalities among variables of a program. In: TAPSOF volume 493 of LNCS. Springer pp 169\u2013192","DOI":"10.1007\/3-540-53982-4_10"},{"key":"e_1_2_1_2_62_2","unstructured":"Groslambert J Stouls N (2009) V\u00e9rification de propri\u00e9t\u00e9s LTL sur des programmes C par g\u00e9n\u00e9ration d\u2019annotations. In: Approches Formelles dans l\u2019Assistance au D\u00e9veloppement de Logiciels (AFADL 2009) in French"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"crossref","unstructured":"Heintze N Jaffar J Voicu R (2000) A framework for combining analysis and verification. In: The 27th symposium on principles of programming languages (POPL 2000)","DOI":"10.1145\/325694.325700"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"Herms P March\u00e9 C Monate B (2012) A certified multi-prover verification condition generator. In: The 4th international conference on verified software: theories tools experiments (VSTTE 2012) volume 7152 of LNCS. Springer pp 2\u201317","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10)","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"crossref","unstructured":"Horwitz S Reps T Binkley D (1988) Interprocedural slicing using dependence graphs. In: The ACM SIGPLAN conference on programming language design and implementation (PLDI 1988) volume 23\u20137 pp 35\u201346","DOI":"10.1145\/960116.53994"},{"key":"e_1_2_1_2_67_2","unstructured":"Herrmann P Signoles J (2013) Annotation generation: Frama-C\u2019s RTE plug-in April. http:\/\/frama-c.com\/download\/frama-c-rte-manual.pdf"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"IEEE Std 754-2008 (2008) IEEE standard for floating-point arithmetic. Technical report. http:\/\/dx.doi.org\/10.1109\/IEEESTD.2008.4610935","DOI":"10.1109\/IEEESTD.2008.4610935"},{"key":"e_1_2_1_2_69_2","unstructured":"ISO\/IEC JTC1\/SC22\/WG14 (2007) 9899:TC3: programming languages\u2014C. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1256.pdf"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","unstructured":"Jobredeaux R Wang Timothy E Feron Eric M (2011) Autocoding Control Software with Proofs I: annotation translation. In: Proceedings of the IEEE\/AIAA digital avionics systems conference (DASC)","DOI":"10.1109\/DASC.2011.6096122"},{"key":"e_1_2_1_2_71_2","unstructured":"Johannes K Rod C Cyrille C Jerome G Yannick M Emyr R (2014) Explicit assumptions\u2014a prenup for marrying static and dynamic program verification. In: Proceedings of TAP 2014 To appear"},{"key":"e_1_2_1_2_72_2","unstructured":"Kosmatov N. Online version of PathCrawler. http:\/\/pathcrawler-online.com\/"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Kosmatov N (2010) Artificial intelligence applications for improved software engineering development: new prospects chapter XI: Constraint-Based Techniques for Software Testing. IGI Global","DOI":"10.4018\/978-1-60566-758-4.ch011"},{"key":"e_1_2_1_2_74_2","doi-asserted-by":"crossref","unstructured":"Kosmatov N Petiot G Signoles J (2013) An optimized memory monitoring for runtime assertion checking of C programs. In: The 4th international conference on runtime verification (RV 2013) volume 8174 of LNCS. Springer pp 167\u2013182","DOI":"10.1007\/978-3-642-40787-1_10"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"crossref","unstructured":"Kosmatov N Signoles J (2013) A lesson on runtime assertion checking with Frama-C. In: The 4th international conference on runtime verification (RV 2013) volume 8174 of LNCS. Springer pp 386\u2013399","DOI":"10.1007\/978-3-642-40787-1_29"},{"key":"e_1_2_1_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_1_2_77_2","unstructured":"Leroy X Doligez D Frisch A Garrigue J R\u00e9my Didier Vouillon J\u00e9r\u00f3me (2013) The OCaml system release 4.01. INRIA 2013. http:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml-4.01\/"},{"key":"e_1_2_1_2_78_2","unstructured":"Leino KRM (2008) This is Boogie 2. Micros Res"},{"key":"e_1_2_1_2_79_2","doi-asserted-by":"crossref","unstructured":"Marre B Arnould A (2000) Test sequences generation from Lustre descriptions: GATeL. In: The 15th IEEE international conference on automated software engineering (ASE 2000). IEEE Computer Society pp 229\u2013237","DOI":"10.1109\/ASE.2000.873667"},{"key":"e_1_2_1_2_80_2","unstructured":"MathWorks. Polyspace. http:\/\/www.mathworks.com\/products\/polyspace"},{"key":"e_1_2_1_2_81_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_2_82_2","doi-asserted-by":"crossref","unstructured":"Min\u00e9 Antoine (2012) Static analysis of run-time errors in embedded real-time parallel c programs. Log Methods Comput Sci 8(1): \u2013","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"e_1_2_1_2_83_2","unstructured":"March\u00e9 C Moy Y (2012) The Jessie plug-in for deduction verification: In: Frama-C version 2.30. INRIA 2012. http:\/\/krakatoa.lri.fr\/jessie.pd."},{"key":"e_1_2_1_2_84_2","doi-asserted-by":"crossref","unstructured":"Mauborgne L Rival X (2005) Trace partitioning in abstract interpretation based static analyzers. In: Sagiv M (ed) European symposium on programming (ESOP\u201905) volume 3444 of lecture notes in computer science. Springer pp 5\u201320","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_2_85_2","doi-asserted-by":"crossref","unstructured":"Necula GC Mcpeak S Rahul SP Weimer W (2002) CIL: intermediate language and tools for analysis and transformation of C programs. In: The international conference on compiler construction (CC 2002) volume 2304 of LNCS. Springer pp 213\u2013228","DOI":"10.1007\/3-540-45937-5_16"},{"key":"e_1_2_1_2_86_2","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890000"},{"key":"e_1_2_1_2_87_2","unstructured":"Pariente D Ledinot E. Formal verification of industrial C code using Frama-C: a case study. In: FoVeOOS"},{"key":"e_1_2_1_2_88_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: The 18th annual symposium on foundations of computer science (FOCS 1977). IEEE Computer Society pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_89_2","doi-asserted-by":"crossref","unstructured":"Randimbivololona F Souyris J Baudin P Pacalet A Raguideau J Schoen D (1999) Applying formal proof techniques to avionics software: a pragmatic approach. In: The wold congress on formal methods in the development of computing systems (FM 1999) volume 1709 of LNCS. Springer pp 1798\u20131815","DOI":"10.1007\/3-540-48118-4_45"},{"key":"e_1_2_1_2_90_2","doi-asserted-by":"crossref","unstructured":"Rushby J (2005) An evidential tool bus. In: Formal methods and software engineering ICFEM volume 3785 of LNCS","DOI":"10.1007\/11576280_3"},{"key":"e_1_2_1_2_91_2","doi-asserted-by":"crossref","unstructured":"Smaragdakis Y Csallner C (2007) Combining static and dynamic reasoning for bug detection. In: The first international conference on tests and proofs (TAP 2007) volume 4454 of LNCS. Springer pp 1\u201316","DOI":"10.1007\/978-3-540-73770-4_1"},{"key":"e_1_2_1_2_92_2","unstructured":"Signoles J Correnson L Prevosto V (2013) Frama-C plug-in development guide April. http:\/\/frama-c.com\/download\/plug-in-developer.pdf"},{"key":"e_1_2_1_2_93_2","unstructured":"Signoles J (2009) Foncteurs imp\u00e9ratifs et compos\u00e9s: la notion de projet dans Frama-C. In: JFLA volume 7.2 of Studia Informatica Universalis (in French)"},{"key":"e_1_2_1_2_94_2","unstructured":"Signoles J (2013) E-ACSL: executable ANSI\/ISO C specification language. Version 1.7 http:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf"},{"key":"e_1_2_1_2_95_2","unstructured":"Signoles J (2014) Comment un chameau peut-il \u00e9crire un journal? In JFLA (in French)"},{"key":"e_1_2_1_2_96_2","unstructured":"Stouls N Prevosto V (2011) Aora\u00ef plug-in tutorial version Nitrogen-20111001 October 2011. http:\/\/frama-c.com\/download\/frama-c-aorai-manual.pdf"},{"key":"e_1_2_1_2_97_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000469"},{"key":"e_1_2_1_2_98_2","doi-asserted-by":"crossref","unstructured":"Tschannen J Furia CA Nordio M Meyer B (2011) Usable verification of object-oriented programs by combining static and dynamic techniques. In: The 9th international conference on software engineering and formal methods (SEFM 2011)","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"e_1_2_1_2_99_2","unstructured":"Wikipedia. Dining philosophers problem. http:\/\/en.wikipedia.org\/wiki\/Dining_philosophers_problem"},{"key":"e_1_2_1_2_100_2","doi-asserted-by":"crossref","unstructured":"Williams N Marre B Mouy P Roger M (2005) PathCrawler: automatic generation of path tests by combining static and dynamic analysis. In: The 5th European dependable computing conference on dependable computing (EDCC 2005) volume 3463 of LNCS Springer pp 281\u2013292","DOI":"10.1007\/11408901_21"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0326-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0326-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0326-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:05:51Z","timestamp":1641485151000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0326-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5]]},"references-count":100,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["10.1007\/s00165-014-0326-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0326-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5]]}}}