CSTVA06 :
Workshop on Constraints in Software Testing, Verification and Analysis

Co-located with CP'06 September 25-29, 2006 - Cité des Congrès - Nantes, France


September 25, 2006
Afternoon  (1:45 p.m.  5:30 p.m.)
bannière


Overview

Dates

Proceedings

Accepted papers

Programme

Organisation Committee
 Overview

In recent years, there has been an increasing interest in the application of constraint solving techniques to the testing and analysis of software systems. A significant body of constraint-based techniques have been proposed and investigated in program analysis (static and dynamic), structural testing, model-based testing, property-oriented testing, etc.

The central idea behind these techniques is designing constraint solvers to deal with boolean, integer and floating-point data types, enumerated types, control structures, method calls and so on. In static analysis, dedicated linear constraints (polyhedra, octagons) and existing solvers (simplex) have been exploited whereas finite domains and set solvers (floating-point constraint solvers, CLP(FD), CLPS, …) have been successfully used in automatic test case generation.

The constraint systems that result from these analyses usually share some common features such as being heterogeneous and highly dynamic. This also led to the design of domain-specific heuristics able to exploit the structure of programs or specification models.

The aim of this workshop is to bring together researchers working in constraint-based program analysis and testing, as well as researchers working on constraint programming or program analysis and testing, to investigate future developments in this research field.

The workshop will focus on the following topics without excluding others related works:
  • Constraint-based analysis of program
  • Constraint-based test cases generation
  • Constraint solvers over specific domains
  • Heuristics guided by the structure of programs and models
  • Combination of dedicated constraint solvers



Dates

  • Camera-ready copy: due to August 30, 2006 for inclusion in the CP+Workshops electronic proceedings

  • Workshop : September 25, 2006 - Afternoon  (1:45 p.m.  5:30 p.m.)

 

The Proceedings are available on line

 

Accepted papers

Extending a CP Solver with Congruences as Domains for Program Verification
Michel Leconte and Bruno Berstel

Generating random values using Binary Decision Diagrams and Convex Polyhedra
Erwan Jahier and Pascal Raymond

Requirements for Constraint Solvers in Verification of Data-Intensive Embedded System Software
Qiang Fu, Maurice Bruynooghe, Gerda Janssens, and Francky Catthoor

Confinement Analysis with Graph Reachabilty Constraints
Fred Spiessens, Luis Quesada, Peter Van Roy

A Symbolic Intruder Model for Hash-Collision Attacks
Yannick Chevalier and Mounira Kourjieh

Strategy for flaws detection based on a service-driven model for group protocols
Najah Chridi and Laurent Vigneron

 

Programme

13h45 - 13h50  Introduction

13h50 - 14h30  On Modular-Reduction Vulnerabilities - Andy King

Abstract:
Securing systems that interact with potentially malicious parties can be a tremendous challenge. Systems written in C are especially difficult to secure, given C's tendency to sacrifice safety for efficiency. Given that buffer overflows are a particularly widespread type of vulnerability, much research has focused on these types of flaw. Recently, a number of subtle buffer overflow vulnerabilities have come to light due to the modular nature of integer arithmetic. This talk will show how analysis techniques, motivated by techniques in constrained-based test-data generation, have potential for diagnosing these integer overflow vulnerabilities. We will also detail some research problems related to these techniques.

14h30 - 15h30 Session: Constraints for software testing and analysis

  Extending a CP Solver with Congruences as Domains for Program Verification
    Michel Leconte and Bruno Berstel

  bullet Generating random values using Binary Decision Diagrams and Convex Polyhedra
     Erwan Jahier and Pascal Raymond

  bullet Requirements for Constraint Solvers in Verification of Data-Intensive Embedded System Software
     Qiang Fu, Maurice Bruynooghe, Gerda Janssens, and Francky Catthoor

15h30 - 16h00 Break

16h00 - 17h00 Session: Constraints for software security

  bullet Confinement Analysis with Graph Reachabilty Constraints
     Fred Spiessens, Luis Quesada, Peter Van Roy

 bullet A Symbolic Intruder Model for Hash-Collision Attacks
     Yannick Chevalier and Mounira Kourjieh

  bullet Strategy for flaws detection based on a service-driven model for group protocols
      Najah Chridi and Laurent Vigneron

17h00 - 17h15  The V3F project - Michel Rueher

17h15 - 17h30  Discussion and conclusion

 

Organisation Committee

WORKSHOP CO-ORGANIZERS

Benjamin Blanc CEA - Paris

Arnaud Gotlieb INRIA - Rennes (Arnaud.Gotlieb@irisa.fr)

Claude Michel University of Nice


PROGRAMME COMMITTEE

  • Fabrice Bouquet, INRIA Nancy
  • Andy King, University of Kent
  • Bruno Legeard, Leirios Technologies
  • Bruno Marre, CEA Paris
  • Christophe Meudec, Institute of Technology Carlow
  • Fred Mesnard, University of La Réunion
  • Andreas Podelski, Max-Planck-Institut für Informatik
  • Jean-Charles Régin, ILOG S.A.
  • Michel Rueher, University of Nice
  • Pascal Van Hentenryck, Brown University