Constantin Enea

Orcid: 0000-0003-2727-8865

According to our database1, Constantin Enea authored at least 84 papers between 2002 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution Analysis.
CoRR, 2024

Strong Linearizability using Primitives with Consensus Number 2.
CoRR, 2024

2023
Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels.
Proc. ACM Program. Lang., 2023

Faithful Simulation of Randomized BFT Protocols on Block DAGs.
IACR Cryptol. ePrint Arch., 2023

A Domain Specific Language for Testing Consensus Implementations.
CoRR, 2023

The Commutativity Quotients of Concurrent Objects.
CoRR, 2023

A Pragmatic Approach to Stateful Partial Order Reduction.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2023

Comparing Causal Convergence Consistency Models.
Proceedings of the Networked Systems - 11th International Conference, 2023

Quorum Tree Abstractions of Consensus Protocols.
Proceedings of the Programming Languages and Systems, 2023

2022
Formal Methods and Distributed Computing: Stronger Together (Dagstuhl Seminar 22492).
Dagstuhl Reports, December, 2022

Checking causal consistency of distributed databases.
Computing, 2022

Automated Synthesis of Asynchronizations.
Proceedings of the Static Analysis - 29th International Symposium, 2022

Blunting an Adversary Against Randomized Concurrent Programs with Linearizable Implementations.
Proceedings of the PODC '22: ACM Symposium on Principles of Distributed Computing, Salerno, Italy, July 25, 2022

2021
MonkeyDB: effectively testing correctness under weak isolation levels.
Proc. ACM Program. Lang., 2021

Robustness Against Transactional Causal Consistency.
Log. Methods Comput. Sci., 2021

Linearizable Implementations Suffice for Termination of Randomized Concurrent Programs.
CoRR, 2021

MonkeyDB: Effectively Testing Correctness against Weak Isolation Levels.
CoRR, 2021

Impossibility of Strongly-Linearizable Message-Passing Objects via Simulation by Single-Writer Registers.
Proceedings of the 35th International Symposium on Distributed Computing, 2021

Checking Robustness Between Weak Transactional Consistency Models.
Proceedings of the Programming Languages and Systems, 2021

2020
Inductive Sequentialization of Asynchronous Programs (Evaluated Artifact).
Dataset, April, 2020

Proving highly-concurrent traversals correct.
Proc. ACM Program. Lang., 2020

Testing consensus implementations using communication closure.
Proc. ACM Program. Lang., 2020

Formalizing and Checking Multilevel Consistency.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Inductive sequentialization of asynchronous programs.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Behavioral simulation for smart contracts.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Verifying Visibility-Based Weak Consistency.
Proceedings of the Programming Languages and Systems, 2020

Root Causing Linearizability Violations.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Boosting Sequential Consistency Checking Using Saturation.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Weak-consistency specification via visibility relaxation.
Proc. ACM Program. Lang., 2019

On the complexity of checking transactional consistency.
Proc. ACM Program. Lang., 2019

Abstract semantic diffing of evolving concurrent programs.
Formal Methods Syst. Des., 2019

Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs that Use Concurrent Objects.
CoRR, 2019

Putting Strong Linearizability in Context: Preserving Hyperproperties in Programsthat Use Concurrent Objects.
Proceedings of the 33rd International Symposium on Distributed Computing, 2019


Replication-aware linearizability.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Gradual Consistency Checking.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Violat: Generating Tests of Observational Refinement for Concurrent Objects.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

On the Complexity of Checking Consistency for Replicated Data Types.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Checking Robustness Against Snapshot Isolation.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Sound, complete, and tractable linearizability monitoring for concurrent collections.
Proc. ACM Program. Lang., 2018

On reducing linearizability to state reachability.
Inf. Comput., 2018

Order out of Chaos: Proving Linearizability Using Local Views.
Proceedings of the 32nd International Symposium on Distributed Computing, 2018

On Verifying TSO Robustness for Event-Driven Asynchronous Programs.
Proceedings of the Networked Systems - 6th International Conference, 2018

Datalog-based scalable semantic diffing of concurrent programs.
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

Monitoring Weak Consistency.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Reasoning About TSO Programs Using Reduction and Abstraction.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
Compositional entailment checking for a fragment of separation logic.
Formal Methods Syst. Des., 2017

Exposing Non-Atomic Methods of Concurrent Objects.
CoRR, 2017

On verifying causal consistency.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

SPEN: A Solver for Separation Logic.
Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency.
Proceedings of the Programming Languages and Systems, 2017

Checking Linearizability of Concurrent Priority Queues.
Proceedings of the 28th International Conference on Concurrency Theory, 2017

Proving Linearizability Using Forward Simulations.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
On Atomicity in Presence of Non-atomic Writes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Symbolic abstract data type inference.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

2015
Tractable Refinement Checking for Concurrent Objects.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Monitoring refinement via symbolic reasoning.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk).
Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

On Automated Lemma Generation for Separation Logic with Inductive Definitions.
Proceedings of the Automated Technology for Verification and Analysis, 2015

2014
On the Path-Width of Integer Linear Programming.
Proceedings of the Proceedings Fifth International Symposium on Games, 2014

Verifying eventual consistency of optimistic replication systems.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013
Model checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics.
Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013), 2013

Local Shape Analysis for Overlaid Data Structures.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Compositional Invariant Checking for Overlaid and Nested Linked Lists.
Proceedings of the Programming Languages and Systems, 2013

Verifying Concurrent Programs against Sequential Specifications.
Proceedings of the Programming Languages and Systems, 2013

2012
Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
CoRR, 2012

Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking.
J. Appl. Non Class. Logics, 2011

On inter-procedural analysis of programs with lists and data.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

2010
Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
Proceedings of the Proceedings First Symposium on Games, 2010

Invariant Synthesis for Programs Manipulating Lists with Unbounded Data.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
Log. Methods Comput. Sci., 2009

A Logic-Based Framework for Reasoning about Composite Data Structures.
Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

2008
Abstraction techniques for verification of concurrent systems. (Techniques d'abstraction dans la verification des systèmes concurrents).
PhD thesis, 2008

Secrecy for bounded security protocols with freshness check is NEXPTIME-complete.
J. Comput. Secur., 2008

Counterexample Guided Abstraction Refinement is Better under Equational Abstraction.
Proceedings of the 15th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS 2008), 31 March, 2008

2007
Strategy-Based and Knowledge-Based Models of Information Flow: Equivalence and Decidability.
Proceedings of the Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2007

Abstractions of Multi-agent Systems.
Proceedings of the Multi-Agent Systems and Applications V, 2007

2006
Abstractions of data types.
Acta Informatica, 2006

2005
Decidability and Complexity Results for Security Protocols.
Proceedings of the Verification of Infinite-State Systems with Applications to Security, 2005

Unifying Decidability Results on Protection Systems Using Simulations.
Proceedings of the Formal Aspects in Security and Trust, Third International Workshop, 2005

2002
SE-Systems, Timing Mechanisms, and Time-Varying Codes.
Int. J. Comput. Math., 2002


  Loading...