NSAD Program

Friday, January 21, 2005

9:00 - 10:00 Invited Speaker (Session Chair: Francesco Logozzo)
  • K. Rustan M. Leino (Microsoft Research)
    Writing specifications for object-oriented programs

    Abstract: The verification of programs requires knowing what properties the program is supposed to satisfy as well as the availability of inductive properties that the program satisfies. For example, to prove that a program meets a programmer-declared precondition of a call that appears after a loop, one may need an inductive loop invariant for the loop. Whether these properties are supplied by the programmer or are automatically inferred, how to express the properties for object-oriented programs is not obvious. In this talk, I describe a systematic way (a methodology) of thinking about specifications for object-oriented programs. The methodology is incorporated in the Spec# programming system, which includes an object-oriented language plus dynamic and static checks. The talk will also feature a brief demo of the Spec# programming system.

10:00 - 10:20 Coffee
10:20 - 12:25 (Session Chair: Arnaud Venet)
  • Cost-precision Tradeoff in Termination Analysis of Higher-Order Functional programs

    Damien Sereni (Oxford University)
    Neil D. Jones (University of Copenhagen)
    Oege de Moor (Oxford University)

  • Inferring Polynomial Invariants with Polyinvar

    Helmut Seidl (Technische Universität München)
    Michael Petter (Technische Universität München)

  • Compositional abstraction and analysis of digital linear filters using the Z-transform

    David Monniaux (École Normale Supérieure, Paris)

  • Towards an Abstraction of the Physical Environment of Embedded Systems

    Matthieu Martel (CEA, Saclay)

  • Parametric Abstract Domains

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

12:30 - 14:00 Lunch
14:00 - 15:00 Invited Speaker (Session Chair: David A. Schmidt)
  • Antoine Miné (École Normale Supérieure, Paris)
    Relational Numerical Abstract Domains for Real-Life Program Analysis

    Abstract: An important choice in the design of a static analyser by Abstract Interpretation is that of one or several suitable numerical abstract domains. They may be used to abstract not only the value of existing numerical program variables, but also numerical instrumented quantities introduced by non-standard semantics for non purely numerical phenomena e.g., in parametric predicate abstraction. There is not one all-purpose domain, and so, the choice must be driven by the specificities of the program class we wish to analyse, taking into account both semantical and algorithmic criteria.
    In this article, we wish to share our experience with the design of numerical domains for the analysis of real-life embedded critical avionic softwares. The main difficulties were: the correct abstraction of floating-point and machine-integer arithmetics, the need for relational invariants able to precisely abstract assignments, guards, and loop invariants, and, finally, the scalability to programs hundreds of thousands lines long with tens of thousands live variables at each program point. To achieve our goal, that is, prove the absence of run-time errors, we designed many techniques that work together. We will present some of them that are of general interest: the octagon domain, specific abstract transfer functions and widenings, expression linearization, symbolic constant propagation, and variable packing.

15:00 - 15:20 Coffee
15:20 - 18:00 (Session Chair: Laurent Mauborgne)
  • Relational Analysis of Floating Point Arithmetic

    Axel Simon (University of Kent Canterbury)

  • Numerical Abstract Domains for Digital Filters

    Jérôme Feret (École Normale Supérieure, Paris)

  • Widening operators for weakly relational numeric abstractions

    Roberto Bagnara (University of Parma)
    Patricia Hill (University of Leeds)
    Elena Mazzi (University of Parma)
    Enea Zaffanella (University of Parma)

  • Weakly relational Domains for FP Computation

    Éric Goubault (CEA Saclay)
    Sylvie Putot (CEA Saclay)

  • Inference of Numerical Relations from Digital Circuits

    Enric Rodriguez-Carbonell (Universitat Politècnica de Catalunya)
    Jordi Cortadella (Universitat Politècnica de Catalunya)

  • More Efficient Determinization of Finite Tree Automata and its Application in Static Analysis

    John P. Gallagher (Roskilde University)
    Kim S. Henriksen (Roskilde University)

  • A Relational Abstraction for Functions

    Bertrand Jeannet (INRIA Rennes),
    Dennis Gopan (University of Wisconsin)
    Thomas Reps (University of Wisconsin)

  • Benchmarking Polyhedral Algorithms: Satisfiability and Dual Conversion

    Duong Nguyen Que (École des Mines de Paris)
    Francois Irigoin (École des Mines de Paris)

Panoram de Paris 360

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


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

Affiliated events

Industrial Day NSAD'05 AIOOL'05


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