Damien Massé: Papers

2016 - 2015 - 2014 - 2012 - 2006 - 2005 - 2004 - 2003 - 2002 - 2001

• NSAD'2012: Proving termination by policy iteration
  Abstract :
  In this paper, we explore the adaptation of policy iteration techniques to compute greatest fixpoint approximations, in order to find sufficient conditions for program termination. Restricting ourselves to affine programs and the abstract domain of template constraint matrices, we show that the abstract greatest fixpoint can be computed exactly using linear programming, and that strategies are related to the template constraint matrix used. We also present a first result on the relationships between this approach and methods which use ranking functions.
  
  BibTeX references:

  @inproceedingsi{Masse12-01,
     author = {Mass{\'e}, D{.}},
     title = {Proving termination by policy iteration},
     booktitle = { Proceedings of the Fourth international workshop on Numerical and Symbolic Abstract Domains },
     address = { Deauville, France },
     journal   = {ENTCS},
     volume    = {287},
     pages     = {77-88},
     year = 2012,
     month = Sep,
  }
  

• Séminaire du LISYC: Analyse abstraite de missions sous PILOT
  
  BibTeX references:

  @inproceedings{Masse05-01,
     author = {Mass\'e, D{.}},
     title = {Analyse abstraite de missions sous PILOT},
     booktitle = {LISYC -- Journ\'ees de l'Aber-Wrac'h},
     address = {Aber-Wrac'h, France},
     year = 2005,
     month = june,
  }
  

  PDF.
• OCEANS'05: Embedded Intelligent Supervision and Piloting for Oceanographic AUV
  
  BibTeX references:

  @inproceedingsi{ea3883-2005-3,
     title = "Embedded Intelligent Supervision and Piloting for Oceanographic AUV",
     author = "L. Nana Tchamnda, F. Singhoff, J. Legrand, J. Vareille, P. Le Parc, F. Monin, D. Mass\'e;, L. Marc\'e;, J. Opderbecke, M. Perrier and V. Rigaud",
     journal = "IEEE Oceanic Engineering Society, OCEANS'05",
     month = Jun,
     year = "2005"
  }
  

• AMAST'2004 : Abstract Domains for Property Checking Driven Analysis of Temporal Properties
  Abstract :
  Abstract interpretation-based static analysis infers properties from the source code of a program. When the goal is to check a temporal specification on the program, we need the analysis to be as precise as possible to avoid false negatives. In previous work [VMCAI'2003], we suggested a method called ``property checking driven analysis'' to automatically use the specification to check during the analysis in order to refine it. However, this approach requires to abstract domains of lower closure operators, something which was not developed. In this paper, we describe some abstractions on lower closure operators developed for a small analyzer of temporal properties. We examine the need for weak relational abstractions, and show that using our new approach can give more precise results than using a traditional abstract interpretation-based analysis with expensive abstract domains.
  
  BibTeX references:

  @inproceedings{Masse04-1,
     author = {Mass{\'e}, D{.}},
     title  = {Abstract Domains for Property Checking Driven Analysis of Temporal Properties},
     page = {349--363},
     booktitle = {Proceedings of the Tenth International Conference on Algebraic Methodology And Software Technology (AMAST'2004)},
     address = {Stirling, UK},
     series = {Lecture Notes in Computer Sciences},
     year = 2004,
     month = {July 12--16},
     volume = {3116},
     publisher = {Springer-Verlag, Berlin, Germany},
  }
  

  PDF.

• PhD Thesis : Vérification par Interprétation Abstraite Guidée par une Propriété Temporelle
  Temporal Property-driven Verification by Abstract Interpretation
  BibTeX references:

  @phdthesis{Masse-Thesis,
     author = {Mass{\'e}, D{.}},
     title  = {Temporal Property-driven Verification by Abstract Interpretation},
     school = {{\'E}cole Polytechnique},
     type = {PhD Thesis},
     year = 2002,
  }
  

  PDF.
• VMCAI'2003 : Property Checking Driven Abstract Interpretation-Based Static Analysis
  Abstract :
  Concrete semantics used for abstract interpretation analyses are generally expressed as fixpoints. Checking a property on this kind of semantics can be done by intersecting the fixpoint with a specification related to the property. In this paper, we show how to produce a new, ``reverse'' analysis from this specification. The result of this analysis, expressed as a lower closure operator, is then used to guide the initial analysis. With this approach, we can refine the result given by the direct abstract analysis. We show that this method enables to deduce forward analyses from backward analyses (and \emph{vice-versa}), and to combine them iteratively in a way similar to the forward-backward combination of analyses.
  
  BibTeX references:

  @inproceedings{Masse03-1,
     author = {Mass{\'e}, D{.}},
     title  = {Property Checking Driven Abstract Interpretation-Based Static Analysis},
     pages  = {56--69},
     booktitle = {Proceedings of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'03)},
     address = {New York, USA},
     series = {Lecture Notes in Computer Sciences},
     volume = 2575,
     editor = {L{.} Zuck and P{.} Attie and A{.} Cortesi and S{.} Mukhopadhyay},
     year = 2003,
     month = {January 9--11},
     publisher = {Springer-Verlag, Berlin, Germany},
  }
  

  Compressed Postscript, PDF.

• SAS'2002 : Semantics for Abstract Interpretation-Based Static Analyses of Temporal Properties
  Abstract :
  Analyzing programs with abstract interpretation often requires to use a combination of forward and backward analyses. However, the forward analyses are mostly reachability analyses, which are often not precise enough when we want to check other temporal properties. In this paper we propose to combine transition systems with temporal properties (with backward modalities) to get ``extended'' transition systems. We define forward and backward semantics for these systems, and give indications for their combination. These semantics, which use set of trees, can be abstracted to make more precise forward and backward analyses of programs. The combinations of these analyses are expected to give better results than the current abstract analyses.
  
  BibTeX references:

  @inproceedings{Masse02-1,
     author = {Mass{\'e}, D{.}},
     title  = {Semantics for Abstract Interpretation-Based Static Analyses of Temporal Properties},
     pages  = {428--443},
     booktitle = {Proceedings of the Ninth Static Analysis Symposium SAS'02},
     address = {Madrid, Spain},
     series = {Lecture Notes in Computer Sciences},
     editor = {M{.} Hermenegildo and G{.} Puebla},
     year = 2002,
     volume = 2477,
     month = {17 -- 20 September},
     publisher = {Springer-Verlag, Berlin, Germany},
  }
  

  Compressed Postscript, PDF.

• PADO'2001 : Combining backward and forward analyses of temporal properties.
  Abstract :
  In this paper we extend the well-known combination of forward and backward static analyses in abstract interpretation for the verification of complex temporal properties for transition systems. First, we show that this combination, whose results are often better than those obtained by using both analyses separately, can be used to check simple temporal properties with just one fixpoint. Then we extend this result to more complex temporal properties, including a superset of \textsc{Ctl} in the case of non-game properties, and a superset of \textsc{Atl} in the case of game properties.
  
  BibTeX references:

  @inproceedings{Masse01-1,
     author = {Mass{\'e}, D{.}},
     title  = {Combining backward and forward analyses of temporal properties},
     pages  = {155--172},
     booktitle = {Proceedings of the Second Symposium PADO'2001, Programs as
                  Data Objects},
     address = {Århus, Denmark},
     series = {Lecture Notes in Computer Sciences},
     editor = {O{.} Danvy and A{.} Filinski},
     year = 2001,
     volume = 2053,
     month = {21 -- 23 May},
     publisher = {Springer-Verlag, Berlin, Germany},
  }
  

  Compressed Postscript, PDF.