Working with Mihaela Sighireanu

Project Proposals

I'm searching students motivated by formal methods, verification, logic and programming to work on the following projects:

• Decision procedures for Separation Logic with Pointer Arithmetics (see SPEN solver)
• Separation Logic for Symbolic Execution (see Colis project)
• Static Analysis of C Programs (see CELIA)
• Model-based Design and Testing of Dynamic Memory Allocators (see my paper at ISMM'17)
• Verification of Container Libraries (see project Vecolib and my paper at TACAS'18)

Current students

• 2017-: Quentin Bouillaguet, PhD Universite de Paris and CEA, is working on combine static analyses and automatic solvers for deductive verification.

Past Students

• 2015-2018: Bin Fang, PhD University Paris Diderot and ECNU Shanghai, on Formal Verification of Dynamic Memory Allocators; co-directed with Geguang Pu (ECNU Shanghai); now at Huawei Shanghai.
• 2009-2012: Cezara Dragoi, PhD University of Paris Diderot, on Automated verification of heap-manipulating programs with infinite data; co-directed with Ahmed Bouajjani; now at INRIA.

• 2017-2018: Raphael Cauderlier (PhD CNAM, France), Verification of Bounded Containers in the Vecolib ANR Project
• 2005: Petr Matousek (PhD University of Brno, Czech Republic), A library of parameterized intervals
• 2003: Marc Boyer (post-doc on ADVANCE EU project), Verification of the PGM protocol with TReX

• Nicolas Jeannerod, MPRI 2016, on Definition of Colis language, co-directed with Ralf Treinen
• Vlad Saveluc, MPRI 2012, on Abstract Domains for Overlaid Data Structures, co-directed with Constatin Enea
• Selma Saidi, Master 2 University of H. Boumedien, Algeria, 2007, on Verification of parameterized systems with infinite data
• Bruno Vivien, CNAM engineer 1998, on Compilation of LOTOS-NT Data Types, co-directed with Hubert Garavel

1. 2018: Pierre Nigron (Master 1): Integration of the multi-set theory in VeriFast (co-directed with Raphael Cauderlier)
2. 2018: Mamadou Balde (EIDD 2nd year engineering): Model-based icode generation for dynamic memory allocators
3. 2015: Etienne Toussaint (Licence 3): Decision procedure for a multi-set constraints (co-directed with Arnaud Sangnier)
4. 2015: Samantha Dinh (EIDD 2nd year engineering): Coding Ada2012 Collections in C
5. 2015: Jean-Christophe Fabrici (EIDD 2nd year engineering): Symbolic execution for tree data structures
6. 2014: Alexandre Nal (EIDD 2nd year engineering): Improved generation of tree automata from inductive definitions
7. 2014: Lionel Reis (EIDD 2nd year engineering): Abstract domain for words of integers
8. 2013: Sebastien Caunois (EIDD 2nd year engineering): Efficient representation of functional graphs
9. 2012: Ghita Layachi (EIDD 2nd year engineering): Improving abstract domains for lists
10. 2011: Maria Abramiuc (Licence 3, University of Iasi, Romania) Weakest precondition calculus in separation logic (co-directed with Constantin Enea)
11. 2011: Vlad Saveluc (Master 1, Univesity of Iasi, Romania) Shape analysis for C programs manipulating doubly-linked list (co-directed with Constantin Enea)
12. 2008: Ouri Maler (Master 1): Synthesis of timed controllers using timed game automata (co-directed with Eugene Asarin)
13. 2008: Alexis Rimbaud (Master 1): Time Games and Planning (co-directed with Eugene Asarin)
14. 2007: Gael Pantin (Master 1): Analysis of Synchronous Process Rewriting Systems (co-directed with Tayssir Touili)
15. 2006: Vimal Kumar Gupta (B.Sc. Internship, India) Verification of Coloured Markup Rewriting Systems
16. 2006: Vishal Kumar Lahoti (Internship B.Sc., India) Parameterized DBM and PPL
17. 2003: Walid Missaoui (Licence 3 University of Tunis, Tunisia) Parameterized DBM and Automatic Solvers
18. 2003: Lisa Allali (Master 1): Analysis of Process Rewrite Systems with Tree Automata (co-directed with Tayssir Touili)
19. 2002: Stephanie Delaune (Master 1): Numerical symbolic representations using automata
20. 2001: Gloria Anaite Paiz (Master 1): A library for BDD and DDD
21. 2001: Guillaume Journaux, Gwenole Tallec (Master 1): Partial exploration of automata with GraphViz (co-directed with Paul Gastin)