Constantin Enea's webpage
Constantin Enea

Constantin is an Associate Professor at the Université Paris Diderot (Paris 7), member of IRIF, a research laboratory of Université Paris Diderot and CNRS. Before that, he was a post-doc in the same laboratory and he was awarded a joint phd at Université Paris 12 and Universitatea "Al. I. Cuza", Iasi, Romania under the advising of Catalin Dima and 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 and logical foundations for constructing reliable software
  • Programming abstractions for concurrent and distributed software
  • Algorithmic verification, static analysis
E-mail: cenea AT irif DOT fr

     My research is founded in part by an ERC Starting Grant
         "Formal Specification and Verification of Distributed Data Structures" (2016-2021)

I am looking for enthusiastic PhD students and postdocs to join my group. Please send me an email if you are interested in research on program verification and static analysis.



  • Checking Linearizability of Concurrent Priority Queues. (pdf), with Ahmed Bouajjani and Chao Wang CONCUR 2017
  • Abstract Semantic Diffing of Evolving Concurrent Programs. (pdf), with Ahmed Bouajjani and Shuvendu Lahiri SAS 2017
  • Proving Linearizability Using Forward Simulations. (pdf), with Ahmed Bouajjani, Michael Emmi, and Suha Orhun Mutluergil CAV 2017
  • Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency (pdf), with Ahmed Bouajjani, Michael Emmi, Burcu Kulahcioglu Ozkan, and Serdar Tasiran, ESOP 2017
  • On Verifying Causal Consistency (pdf), with Ahmed Bouajjani, Rachid Guerraoui, and Jad Hamza, POPL 2017
  • On Atomicity in Presence of Non-atomic Writes (pdf), with Azadeh Farzan, TACAS 2016
  • Symbolic Abstract Data Type Inference (pdf), with Michael Emmi, POPL 2016
  • On Automated Lemma Generation for Separation Logic with Inductive Definitions (pdf), with Mihaela Sighireanu and Zhilin Wu, ATVA 2015
  • On Reducing Linearizability to State Reachability (pdf), with Ahmed Bouajjani, Michael Emmi, and Jad Hamza, ICALP 2015
  • Monitoring Refinement via Symbolic Reasoning (pdf), with Michael Emmi, and Jad Hamza, PLDI 2015
  • Tractable Refinement Checking for Concurrent Objects (pdf), with Ahmed Bouajjani, Michael Emmi, and Jad Hamza, POPL 2015
  • Compositional Entailment Checking for a Fragment of Separation Logic (pdf), with Ondrej Lenga, Mihaela Sighireanu, and Tomas Vojnar, APLAS 2014
    • The tool SPEN participated to SL-COMP'14, a competition of solvers for Separation Logic
  • On the Path-Width of Integer Linear Programming (pdf), with Peter Habermehl, Omar Inverso, and Gennaro Parlato, GANDALF 2014
  • Verifying Eventual Consistency of Optimistic Replication Systems (pdf), with Ahmed Bouajjani and Jad Hamza, POPL 2014
  • 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

Complete List

Program committees:

VMCAI 2015    CAV 2016    ATVA 2017    CONCUR 2017    POPL 2018


Violinefficient symbolic reasoning algorithms for checking linearizability of concurrent data structures.

SPENa solver for Separation Logic with inductive predicates.

Celiaa 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.