Industrial day on

Automatic Tools for Program Verification

January 20, 2005   :   Paris, France

Maison des Polytechniciens
(The conference venue is a private place, only registered participants will have access to the conference.)

The objectives of the workshop are to provide a forum for participants with high confidence complex systems needs and participants with emerging technologies or research that might contribute to addressing such problems.

The programme will consist of a tutorial on abstract interpretation, presentations of verification tools, assessments of the use of a few of such tools by industrial users, and a panel on future research challenges.

8:30 - 9:00 Coffee
9:00 - 10:30 Tutorial (Session Chair: Roberto Giacobazzi)
  • Abstract Interpretation

    Patrick Cousot (École Normale Supérieure, Paris)

    Abstract: Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science such that the semantics, the proof, the static analysis, the verification, the safety and the security of software or hardware computer systems. In particular, abstract interpretation-based static analysis, which automatically infers dynamic properties of computer systems, has been very successful these last years to automatically verify complex properties of real-time, safety critical, embedded systems.

10:30 - 11:00 Coffee
11:00 - 12:30 (Session Chair: Warren A. Hunt)
  • SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft

    Sriram K. Rajamani (Microsoft Research, Redmond, USA)

    Abstract: There are several obstacles to commercially viable formal methods. First, we need to solve a real and pressing problem, whose solution is of independent interest. Next, every formal method for reasoning about systems needs some kind of specification, and thus any formal methods effort needs to answer the question "Where does the spec come from?".
    In this talk we will outline our experiences from the SLAM project at Microsoft Research. The goal of the SLAM project is to analyze system software written in C, and check it against temporal safety properties. The SLAM toolkit uses model checking, program analysis and theorem proving techniques to do automatic analysis, and requires no user-supplied abstractions or annotations such as pre-conditions, post-conditions or loop invariants. We have successfully applied the SLAM toolkit to over 100 Windows device drivers, to both validate their behavior and find defects in their usage of kernel-level APIs. The SLAM toolkit currently is in transition from a research prototype to a product-grade tool that will be supported and used by the Windows development organization.

  • C Global Surveyor: Designing a Static Analyzer for NASA Flight Software

    Arnaud Venet, Guillaume Brat (Kestrel Technology / NASA Ames Research Center, USA)

    Abstract: In this talk we will report our experience in designing, implementing and infusing C Global Surveyor, a static analysis tool specially tailored for analyzing large space flight control systems developed at NASA in the Mars Exploration Program. Our analyzer focuses on memory errors that occur in pointer-intensive applications. It provides a level of certification that is comparable or better than state-of-the-art commercial tools while achieving a much better scalability. Being able to analyze hundreds of thousands lines of code in few hours while providing a good level of precision makes C Global Surveyor ready to be infused into NASA missions. This process has already begun and we will report first experiments conducted with NASA developers.

  • Is your program always fast enough?

    Christian Ferdinand (AbsInt GmbH, Saarbruecken, Germany)

    Abstract: Many tasks in safety-critical embedded systems have hard real-time characteristics. Failure to meet deadlines may result in the loss of life or in large damages. Utmost carefulness and state-of-the-art machinery have to be applied to make sure that all requirements are met. To do so lies in the responsibility of the system designer(s). Fortunately, the state of the art in deriving run-time guarantees for real-time systems has progressed so much that tools based on sound methods are commercially available and have proved their usability in industrial practice. Recent advances in the area of abstract interpretation have led to the development of static program analysis tools that efficiently determine upper bounds for the Worst-Case Execution Time (WCET) of code snippets given as routines in executables. The predicted WCETs can be used to determine an appropriate scheduling scheme for the tasks and to perform an overall schedulability analysis in order to guarantee that all timing constraints will be met (also called timing validation).

12:30 - 14:00 Lunch
14:00 - 15:30 (Session Chair: Patrick Cousot)
  • Validating Industrial-Scale Models Using ACL2

    Warren A. Hunt, Jr. (University of Texas, Austin, USA)

    Abstract: We present our tool suite and describe how industry is using it to validate their computer system designs. We use the combined simulation and automated verification environment available within the ACL2 system to specify and verify models of commercial-sized computing systems. We summarize the use of ACL2 to model and verify processors from AMD, Motorola, and Rockwell Collins. We describe our modeling approach, how we validate these models, and how we prove the correctness of these models with respect to their specifications.

  • ASTRÉE: Verification of Large Critical Software

    Laurent Mauborgne (École Normale Supérieure, Paris) joint work with Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, David Monniaux and Xavier Rival

    Abstract: ASTRÉE is an abstract interpretation-based static analyzer that is efficient and precise enough to prove the absence of errors in a family of large real-time embedded safety-critical applications. This is achieved through the computation of a precise and safe over-approximation of the reachable states of a program. ASTRÉE can cope with a large number of interrelated global variables, and takes into account all possible rounding errors in floating point computations. The analysis is fully automatic, and it has been succesfully applied on industrial software, yelding no false alarm.

  • Proving Automatically the Absence of Run Time Errors in Avionics

    Jean Souyris (Airbus France)

    Abstract: Even the most safety-critical avionics programs tend to be more complex (more functions put into software), leading to dramatically increase the cost of test campaigns. Moreover, when it is mandatory, e.g. for safety reasons, to demonstrate that a program will never have unwanted behaviours, the intrinsic limits of testing make this demonstration more and more difficult. That is why Airbus relies on Abstract Interpretation-based static analysers for proving that unwanted behaviours will never occur. A first step has been achieved in the field of "performance analysis" with AbsInt GmbH's tools for maximum stack usage and Worst Case Execution Time computations; these tools being used by Airbus in the developement of avionics programs. Next step is the proof of properties more related to program's computations like the absence of Run Time Errors. For that, an Abstract Interpretation-based static analyser called ASTRÉE is being developed at the École Normale Supérieure de Paris (rue d'Ulm). This tool is able to analyse real-size safety-critical synchronous programs with ZERO FALSE ALARMS.
    The aim of the talk is to express airbus' point of view about the future industrial usage of ASTRÉE on avionics programs.

15:30 - 16:00 Coffee
16:00 - 17:00 (Session Chair: Sriram Rajamani)
  • FLUCTUAT: a static analyzer by abstract interpretation of the accuracy of floating-point computations

    Eric Goubault (CEA-LIST, Saclay) joint work with Matthieu Martel and Sylvie Putot

    Abstract: FLUCTUAT is an abstract interpreter that characterizes the discrepancy due to the usage of IEEE 754 floating-point numbers instead of the mathematical real numbers in ANSI C (and some assembly codes) programs. It helps determine the lines of code most responsible for an inaccuracy, by keeping track of (overapproximations of) magnitudes of errors that can occur in all executions of the program. We will present some of the principles on which this static analyzer is based, and show some examples. FLUCTUAT is currently used on fragments of real industrial codes.

  • TVLA: A System for Generating Abstract Interpreters

    Roman Manevich (Tel-Aviv University) joint work with Tal Lev-Ami and Mooly Sagiv

    Abstract: Modern programming languages such as C++,C# and Java support dynamic allocation of objects and pointer manipulations. These features make programs notoriously error-prone and hard to prove correct and optimize. The goal of the TVLA (Three-Valued-Logic Analyzer) is to provide a platform to experiment and assess different algorithms for proving properties of heap-manipulating programs. TVLA is based on a mathematical framework that allows to automatically produce sound approximations of all executions of a program. TVLA was implemented in Java and successfully used to prove interesting properties of (concurrent) Java programs manipulating dynamically allocated linked data structures. I will describe some of the TVLA applications, ongoing work, and the stumbling blocks for scaling TVLA to handle larger programs.

17:00 - 18:00 Panel : Future research challenges
  • J. Souyris (Airbus France)
  • S. Rajamani (Microsoft Research, Redmond, USA)
  • P. Cousot (École Normale Supérieure, Paris)
  • A. Cortesi (Università Ca' Foscari di Venezia, I)
  • R. Giacobazzi (Università di Verona, I)


Panoram de Paris 360

Contact: Radhia[point]Cousot[arobase]polytechnique [point]fr
Last modified: Sunday May 23, 2010
Valid XHTML 1.1! Valid CSS!
ACM

VMCAI'05

Conference venue Invited speakers Invited tutorial Program Call for papers Committees Registration Sponsors Publication LNCS 3385

Affiliated events

Industrial Day NSAD'05 AIOOL'05

Paris

Accommodations Subway (map, itinary,...) Weather Maps

Links

VMCAI'04VMCAI'03
EAPLS