I am a former PhD student of the Computer Science Research Center (CRI) of MINES ParisTech (also known as École des mines de Paris). I have defended my thesis on February 6, 2015, and no longer work at CRI.
My thesis is about static analysis of control-command systems, with a particular focus on floating-point and integer invariants. This work has been done under the supervision of my PhD advisor François Irigoin and my PhD associate advisor Olivier Hermant.
Static Analysis of Control-Command Systems: Floating-Point and Integer Invariants, Vivien Maisonneuve, Paris, France, February 2015
Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov (French), Olivier Hermant, Vivien Maisonneuve, in Journées Approches Formelles dans l'Assistance au Développement Logiciel (AFADL 2015), Bordeaux, France, September 2015
Computing Invariants with Transformers: Experimental Scalability and Accuracy, Vivien Maisonneuve, Olivier Hermant, François Irigoin, in The Fifth International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2014), Munich, Germany, September 2014
ALICe: A Framework to Improve Affine Loop Invariant Computation, Vivien Maisonneuve, Olivier Hermant, François Irigoin, in The Fifth International Workshop on Invariant Generation (WING 2014), Vienna, Austria, July 2014
Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach, Vivien Maisonneuve, in The Third International Workshop on Numerical and Symbolic Abstract Domain (NSAD 2011), Venice, Italy, September 2011
Translation of Lyapunov Stability Proofs to Machine Arithmetic, Vivien Maisonneuve, in The Eighth Meeting of the French Community of Compilation, Nice, France, July 2014
ALICe: A Benchmark to Improve Affine Loop Invariant Computation, Vivien Maisonneuve, in The Seventh Meeting of the French Community of Compilation, Dammarie-les-Lys, France, December 2013
From Physics to Interrupt Handlers: the Real to Float Step, Vivien Maisonneuve, in TOCCATA Research Team Seminar, Saclay, France, November 2012
From Physics to Interrupt Handlers: the Real to Float Step, Vivien Maisonneuve, in DEDUCTEAM Research Team Seminar, Paris, France, June 2012
LinPy: A Polyhedral Library for Python Based on isl, Danielle Bolan, Vivien Maisonneuve, August 2014
Preservation of Lyapunov-Theretic Proofs: From Real to Floating-Point Arithmetic, Vivien Maisonneuve, Olivier Hermant, François Irigoin, February 2014
Préservation de preuve lors de la compilation sur microcontrôleur (French), Vivien Maisonneuve, in GDR GPL National Days, Paris, France, May 2014
Best Poster Award
Last updated: July 16, 2015 – HTML validation, CSS validation