Programme détaillé

• 08:30 - Welcome coffee and registration
• 09:00 - Opening comments

   F. Kirchner, List, CEA Tech
  

• 09:05 - Keynote: How Frama-C can help a verification & assessment body

  F. Sadmi, Bureau Veritas

  As software verification activities get more and more complex and expensive, developers and users need methodologies and tools to perform them in an optimal manner. On the other hand, third-parties have to find ways to trust the verification evidence that are provided, especially regarding standards and normative requirements. In particular, Bureau Veritas has to understand the Frama-C tool in order to assess its outputs or perform directly the analysis.

• 09:30 - Automatic Generation of Counter-Measure Calling Contexts: the CURSOR Method

  D. Pariente, DASSAULT AVIATION

  Designed during the FP7/STANCE project, the CURSOR method aims at detecting categories of common weaknesses in the source code, and generating the corresponding counter-measure calling contexts. This intends to strengthen applications potentially exposed to attacks based on identified families of flaws in the code. The method relies on a runtime-assertion checking approach, and is tooled by means of the Frama-C platform. CURSOR was successfully experimented on some Apache server libraries.

• 09:30 - I. INDUSTRIAL USES | Session 1
• 10:00 - Safe resource use tracking with a combination of control flow and data flow analysis

  P. Bishop & S. George, Adelard LLP

  Many dynamically allocated resources like memory, semaphores and interrupt enable/disable require a similar kind of analysis to demonstrate correct usage. To prevent long term resource starvation, any resource claim must be released on all subsequent branches of control flow. For cases where claims and releases are repeatedly made using the same resource identifier, an integrated data flow analysis is needed to complete the analysis. We have developed a prototype plug-in that performs this analysis in the context of malloc/free pairs, but is written in a generalised way that is easy to adapt to other resource claim/release patterns.

• 10:30 - Break
• 11:00 - II. INDUSTRIAL USES | Session 2
• 11:01 - TrustInSoft Analyzer: practical program analysis for guaranteed safety and security

  B. Monate, TrustInSoft

  TBA

• 11:30 - SPEEDY: Specification editing, checking & discovery for C programs with ACSL specifications

  D. R. Cok, GrammaTech, Inc.

  The SPEEDY tool intends to simplify the task of applying formal methods in the context of typical software development environments. The incarnation of SPEEDY described here targets C programs with ACSL specifications. The tool combines four elements: (a) enhancing the Eclipse development environment for C programs with first-class support for ACSL, (b) adding functionality and text to aid users in understanding how to write specifications, (c) integrating tools that check specifications, such as Frama-C, showing the success or failure of verification attempts in the Eclipse GUI, (d) integrating tools and algorithms for inferring specifications from the source code. The development of SPEEDY was supported by NASA (Contract #NNX14CL05C) and executed by GrammaTech, Inc.

• 12:00 - Lunch
• 14:00 - III. FRAMA-C AS A RESEARCH PLATFORM
• 14:01 - Formal verification of controller implementation

  P-L. Garoche, Onera

  Embedded control systems are amongst the most critical systems. Their behavior is specific: they have an infinite behavior in which, at each loop iteration, a sensor input is read, computations are performed, and an output is produced on actuators. A first part of the talk will focus on proving the bounded behavior of those systems, guarantying the absence of overflow despite their infinite behavior. Those systems are typically designed using high level models such as Matlab Simulink, ANSYS Scade or Lustre. Then they are compiled into embedded C code. These models are well suited to perform functional properties verification, eg. using k-induction-based model-checkers. But the expression and the analysis of those properties is more difficult at code level. We propose a methodology to compile these model-level specification and associated model-checking proofs into C level artifacts. Once produced we rely on Frama-C/WP to revalidate them, at code level. These results benefited from numerous collaborations including X. Thirioux (IRIT), P. Roux, T. Kahsai (NASA/CMU), E. Feron (Georgia Tech), G. Davy (Onera), H. Herencia-Zapana (ex-NIA, now GE), R. Jobredeaux (ex-GT), T. Wang (ex-GT, now UTRC).

• 14:30 - Research Challenges in Software Verification of Safety-Critical Aerospace Systems

  C. A. Muñoz, NASA

  This talk reports on formal methods research conducted under NASA’s Airspace Operations and Safety Program (AOSP). As part of this research, Frama-C has been used in the formal verification of numerical intensive software and in the formal verification of automatically generated run-time monitors. Based on this experience, the talk discusses research challenges in software verification of safety-critical systems of interest to NASA.

• 15:00 - Frama-C and Why3: going way back — and forward, too

  A. Paskevich - LRI, Université Paris-Saclay / Inria

  Why3 is a tool for deductive verification of imperative programs. Why3 and its predecessor, Why, have a long history of collaboration, both technical and human, with Frama-C. In this talk, we revisit the roots of this collaboration, assess its current state, and venture into possible future developments. In particular, we make a case for an interface between ACSL and high-level specification facilities available in Why3, which include type polymorphism, variant types and pattern matching, fine-grained specification libraries, and a way to ensure consistency of an axiomatization by realizing it in a sceptical proof assistant like Coq or Isabelle.

• 15:30 - Break
• 16:00 - IV. NEW DEVELOPMENTS BY THE Frama-C Team
• 16:01 - Proving C code with GATeL, or how to use Frama-C, WP and Value as libraries

  L. Correnson, List, CEA Tech

  Functional properties of reactive, synchrone software are naturally specified and encoded into Lustre Observers. In practice however, such an embedded software would not be completely generated from synchronous models, but would contain a large amount of manually written C code. One can thus be required to verify its Lustre properties directly from the C code.We show how to use the combined power of Value Analysis and WP interfaces to develop a Frama-C plug-in extracting a Lustre model of this synchronous behaviour from C source code, and to verify some of its properties with GaTEL. This constitutes a step forward in the proof of complex safety systems, and the very first experiment combining these three major technologies from our laboratory.

• 16:30 - Evolved Value Analysis

  B. Yakobowski, List CEA Tech

• 17:00 - Frama-Clang, a C++ front-end for Frama-C

  V. Prevosto, List, CEA Tech

  This talk will present the new Frama-Clang plug-in, which aims at providing a C++ front-end to Frama-C. As its name suggests, Frama-Clang relies on the Clang compiler for the parsing and type-checking of C++ code. We will see how the necessary information can be extracted from Clang's AST to build a valid Frama-C AST and how it is possible to extend Clang to parse and type-check ACSL(++) annotations together with the code itself.

• 17:30 - Cocktail