About
Constantin is an Assistant Professor at the Université Paris Diderot (Paris 7), member of the Modélisation et vérification group of LIAFA, a laboratory of Université Paris Diderot and CNRS. Before that, he was a post-doc in the same group and he was awarded a phd at Université Paris 12 and Universitatea "Al. I. Cuza", Iasi, Romania under the advising of Dr. Catalin Dima and Dr. Ferucio Laurentiu Tiplea.
Constantin's research is focused on developing formal verification and analysis techniques to help the construction of reliable software systems. More precisely, his main research interests are:
- algorithmic verification techniques
- static analysis for heap manipulating programs
- logics for program verification and decision procedures
Publications
Recent
- Local Shape Analysis for Overlaid Data Structures (pdf), with Cezara Dragoi and Mihaela Sighireanu, SAS 2013
- Verifying Concurrent Programs Against Sequential Specifications (pdf, technical report pdf), with Ahmed Bouajjani, Michael Emmi, and Jad Hamza, ESOP 2013
- Compositional Invariant Checking for Overlaid and Nested Linked Lists (pdf), with Vlad Saveluc and Mihaela Sighireanu, ESOP 2013
- Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data (pdf), with Ahmed Bouajjani, Cezara Dragoi, and Mihaela Sighireanu, ATVA 2012
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data (pdf) , with Ahmed Bouajjani, Cezara Dragoi, and Mihaela Sighireanu, VMCAI 2012
- On Inter-Procedural Analysis of Programs with Lists and Data (pdf), with Ahmed Bouajjani, Cezara Dragoi, and Mihaela Sighireanu, PLDI 2011
Tools
Celia: a Frama-C plug-in for inter-procedural static analysis of C programs with linked lists and unbouded data.
Cinv: a tool for the data and shape analysis of programs with linked lists.