Ernie Cohen

According to our database, Ernie Cohen authored at least 34 papers between 1994 and 2019.

Collaborative distances:

• Dijkstra number of two.
• Erdős number of three.

2019

A Machine-Checked Proof of Security for AWS Key Management Service.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran

IACR Cryptol. ePrint Arch., 2019

A Reduction Theorem for Store Buffers.

Ernie Cohen, Norbert Schirmer

Arch. Formal Proofs, 2019

2018

Object-Oriented Security Proofs.

Ernie Cohen

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2015

Verification Tools for Transactional Programs.

Adrián Cristal, Burcu Kulahcioglu Ozkan, Ernie Cohen, Gokcen Kestor, Ismail Kuru, Osman S. Unsal, Serdar Tasiran, Suha Orhun Mutluergil, Tayfun Elmas

Proceedings of the Transactional Memory. Foundations, Algorithms, Tools, and Applications, 2015

2014

Coherent Causal Memory.

Ernie Cohen

CoRR, 2014

Hypothesis Elimination in Kleene Semirings.

Ernie Cohen

CoRR, 2014

Modular Verification of Hybrid System Code with VCC.

Ernie Cohen

CoRR, 2014

Store Buffer Reduction with MMUs.

Geng Chen, Ernie Cohen, Mikhail Kovalev

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

2013

Data Abstraction in VCC.

Ernie Cohen

Proceedings of the Engineering Dependable Software Systems, 2013

Theory of Multi Core Hypervisor Verification.

Ernie Cohen, Wolfgang J. Paul, Sabine Schmaltz

Proceedings of the SOFSEM 2013: Theory and Practice of Computer Science, 2013

2012

Verification of TLB Virtualization Implemented in C.

Eyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

2011

The 1st Verified Software Competition: Experience Report.

Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß

Proceedings of the FM 2011: Formal Methods, 2011

2010

From Total Store Order to Sequential Consistency: A Practical Reduction Theorem.

Ernie Cohen, Bert Schirmer

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Modular specification and verification of interprocess communication.

Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Verifying shadow page table algorithms.

Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Local Verification of Global Invariants in Concurrent Programs.

Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

A Precise Yet Efficient Memory Model For C.

Ernie Cohen, Michal Moskal, Stephan Tobies, Wolfram Schulte

Proceedings of the 4th International Workshop on Systems Software Verification, 2009

Weak Kleene Algebra is Sound and (Possibly) Complete for Simulation

Ernie Cohen

CoRR, 2009

Pessimistic Testing

Ernie Cohen

CoRR, 2009

A Better Reduction Theorem for Store Buffers

Ernie Cohen, Norbert Schirmer

CoRR, 2009

VCC: A Practical System for Verifying Concurrent C.

Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Invariants, Modularity, and Rights.

Ernie Cohen, Eyad Alkassar, Vladimir Boyarinov, Markus Dahlweid, Ulan Degenbaev, Mark A. Hillebrand, Bruno Langenstein, Dirk Leinenbach, Michal Moskal, Steven Obua, Wolfgang J. Paul, Hristo Pentchev, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, Sergey Tverdyshev

Proceedings of the Perspectives of Systems Informatics, 2009

2008

Using probabilistic Kleene algebra pKA for protocol verification.

A. K. McIver, Carlos Gonzalía, Ernie Cohen, Carroll C. Morgan

J. Log. Algebraic Methods Program., 2008

2006

Optimistic synchronization-based state-space reduction.

Scott D. Stoller, Ernie Cohen

Formal Methods Syst. Des., 2006

Validating the Microsoft Hypervisor.

Ernie Cohen

Proceedings of the FM 2006: Formal Methods, 2006

Using Probabilistic Kleene Algebra for Protocol Verification.

Annabelle McIver, Ernie Cohen, Carroll Morgan

Proceedings of the Relations and Kleene Algebra in Computer Science, 2006

Weak Kleene Algebra and Computation Trees.

Ernie Cohen

Proceedings of the Relations and Kleene Algebra in Computer Science, 2006

2003

First-order Verification of Cryptographic Protocols.

Ernie Cohen

J. Comput. Secur., 2003

2002

TAPS: The Last Few Slides.

Ernie Cohen

Proceedings of the Formal Aspects of Security, First International Conference, 2002

2000

A note on the complexity of propositional Hoare logic.

Ernie Cohen, Dexter Kozen

ACM Trans. Comput. Log., 2000

Separation and Reduction.

Ernie Cohen

Proceedings of the Mathematics of Program Construction, 5th International Conference, 2000

TAPS: A First-Order Verifier for Cryptographic Protocols.

Ernie Cohen

Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000

1998

Reduction in TLA.

Ernie Cohen, Leslie Lamport

Proceedings of the CONCUR '98: Concurrency Theory, 1998

1994

The Convergence Span of Greedy Load Balancing.

Ernie Cohen

Inf. Process. Lett., 1994