Constantin is a Professor of Computer Science at Ecole Polytechnique, and member of LIX, a research laboratory of Ecole Polytechnique and CNRS. Before that, he was an Associate Professor at University of Paris and member of IRIF, a post-doc at IRIF, and he was awarded a joint phd at University 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, automated testing
I am always looking for highly motivated students or postdocs who would like to work in my research area. Send me an email if any of the topics interest you.

Upcoming events:

Publications

For the full list see DBLP

  • Scenario-based Proofs for Concurrent Objects. (pdf), with Eric Koskinen: OOPSLA 2024 (conditionally accepted)
  • Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels. (pdf), with Ahmed Bouajjani and Enrique Román-Calvo: PLDI 2023
  • Faithful Simulation of Randomized BFT Protocols on Block DAGs. (pdf), with Hagit Attiya and Shafik Nassar: CONCUR 2023
  • Quorum Tree Abstractions of Consensus Protocols. (pdf), with Berk Çirisci and Suha Orhun Mutluergil: ESOP 2023
  • A Pragmatic Approach to Stateful Partial Order Reduction. (pdf), with Berk Çirisci, Azadeh Farzan, and Suha Orhun Mutluergil: VMCAI 2023
  • Blunting an Adversary Against Randomized Concurrent Programs with Linearizable Implementations. (pdf), with Hagit Attiya and Jennifer L. Welch: PODC 2022
  • Automated Synthesis of Asynchronizations. (pdf), with Sidi Mohamed Beillahi, Ahmed Bouajjani, and Shuvendu K. Lahiri: SAS 2022
  • MonkeyDB: effectively testing correctness under weak isolation levels. (pdf), with Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, and Akash Lal: OOPSLA 2021
  • Impossibility of Strongly-Linearizable Message-Passing Objects via Simulation by Single-Writer Registers. (pdf), with Hagit Attiya and Jennifer L. Welch: DISC 2021
  • Checking Robustness Between Weak Transactional Consistency Models. (pdf), with Sidi Mohamed Beillahi and Ahmed Bouajjani: ESOP 2021
  • Proving Highly-Concurrent Traversals Correct. (pdf), with Yotam Feldman, Artem Khyzha, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, and Sharon Shoham: OOPSLA 2020
  • Testing Consensus Implementations using Communication Closure. (pdf), with Cezara Drăgoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic: OOPSLA 2020
  • Behavioral Simulation for Smart Contracts. (pdf), with Sidi Mohamed Beillahi, Gabriela Ciocarlie, and Michael Emmi: PLDI 2020
  • Inductive Sequentialization of Asynchronous Programs. (pdf), with Thomas Henzinger, Bernhard Kragl, Suha Mutluergil, and Shaz Qadeer: PLDI 2020
  • Verifying Visibility-Based Weak Consistency. (pdf), with Siddharth Krishna, Michael Emmi, and Dejan Jovanovic: ESOP 2020
  • Root Causing Linearizability Violations. (pdf), with Berk Çirisci, Azadeh Farzan, and Suha Orhun Mutluergil: CAV 2020
  • Boosting Sequential Consistency Checking Using Saturation. (pdf), with Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, and Mohammed Erradi: ATVA 2020
  • Formalizing and Checking Multilevel Consistency. (pdf), with Ahmed Bouajjani, Madhavan Mukund, and Gautham Shenoy R, S.P. Suresh: VMCAI 2020
  • On the complexity of checking transactional consistency. (pdf), with Ranadeep Biswas: OOPSLA 2019
  • Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs that Use Concurrent Objects. (pdf), with Hagit Attiya: DISC 2019
  • Gradual Consistency Checking. (pdf), with Rachid Zennou, Ahmed Bouajjani, and Mohammed Erradi: CAV 2019
  • Checking Robustness Against Snapshot Isolation. (pdf), with Sidi Mohamed Beillahi and Ahmed Bouajjani: CAV 2019
  • On the Complexity of Checking Consistency for Replicated Data Types. (pdf), with Ranadeep Biswas and Michael Emmi: CAV 2019
  • Violat: Generating Tests of Observational Refinement for Concurrent Objects. (pdf), with Michael Emmi: CAV 2019
  • Replication-Aware Linearizability. (pdf), with Chao Wang, Suha Orhun Mutluergil, and Gustavo Petri: PLDI 2019
  • Weak-Consistency Specification via Visibility Relaxation. (pdf), with Michael Emmi: POPL 2019
  • Robustness Against Transactional Causal Consistency. (pdf, journal version), with Sidi Mohamed Beillahi and Ahmed Bouajjani: CONCUR 2019
  • Order out of Chaos: Proving Linearizability Using Local Views. (pdf, with Yotam M. Y. Feldman, Adam Morrison, Noam Rinetzky and Sharon Shoham: DISC 2018
  • Reasoning About TSO Programs Using Reduction and Abstraction. (pdf, long version), with Ahmed Bouajjani, Suha Orhun Mutluergil, and Serdar Tasiran: CAV 2018
  • On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. (pdf, long version), with Ahmed Bouajjani, Kailiang Ji, and Shaz Qadeer: CAV 2018
  • Monitoring Weak Consistency. (pdf), with Michael Emmi: CAV 2018
  • Exposing Non-Atomic Methods of Concurrent Objects. (pdf), with Michael Emmi
  • Datalog-Based Scalable Semantic Diffing of Concurrent Programs. (pdf), with Chungha Sung, Shuvendu K. Lahiri, Chao Wang: ASE 2018
  • Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections. (pdf), with Michael Emmi POPL 2018
  • 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, long version), 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, long version), 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, journal version), 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

Group

Phd students:

Namratha Reddy (started 2023)
Enrique Roman Calvo (started 2021)
Srinidhi Nagendra (started 2020)

Graduated Phd students/Postdocs:

Berk Cirisci (graduated 2022)
Ranadeep Biswas (graduated 2021)
Sidi Mohamed Beillahi (graduated 2021, co-directed with Ahmed Bouajjani)
German Andres Delbianco (postdoc 2017-2019)
Chao Wang (postdoc 2016-2018)
Suha Orhun Mutluergil (graduated 2018, co-directed with Serdar Tasiran)
Jad Hamza (graduated 2016, co-directed with Ahmed Bouajjani)

Graduated MSC students:

Maria Abramiuc (2012, co-directed with Mihaela Sighireanu)
Vlad Saveluc (2013, co-directed with Mihaela Sighireanu)

Awards

Junior member of Institut Universitaire de France, 2019
European Research Council (ERC) Starting Grant, 2015

Professional activities

Program Co-Chair     CAV 2023
Program Committee     POPL 2023
Program Committee     VMCAI 2023
Co-Organizer Dagstuhl Seminar     Formal Methods and Distributed Computing: Stronger Together
Program Committee     OOPSLA 2022
Program Committee     PLDI 2022
Program Committee     CONCUR 2022
Program Committee     NETYS 2022
Program Committee     CAV 2021
Program Committee     SAS 2021
Program Committee     DISC 2020
Program Co-Chair    PERR 2020
Program Committee     CAV 2020
Program Committee     FORTE 2020
Program Committee     VMCAI 2020
Program Committee     SYNASC 2019 (Logic and Programming)
Program Committee     iFM 2019
Program Co-Chair     VMCAI 2019
Program Committee     ESOP 2019
Program Committee     NETYS 2019
Program Committee     CAV 2019
Program Co-Chair     EPIT 2018
Program Co-Chair     YR-CONCUR 2018
Program Committee     PAPOC 2018
Program Committee     NETYS 2018
Program Committee     POPL 2018
Program Committee     RADICAL 2017
Program Committee     CONCUR 2017
Program Committee     ATVA 2017
Program Committee    CAV 2016
Program Committee    VMCAI 2015