Ernie Cohen

38 papers A* 3A 1B 9Journal 13Unranked 9
YearRankTypeTitle / Venue / Authors
2019 A* conf
A Machine-Checked Proof of Security for AWS Key Management Service.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Reduction Theorem for Store Buffers.
Arch. Formal Proofs
Ernie Cohen, Norbert Schirmer
2018 B conf
Object-Oriented Security Proofs.
FM
Ernie Cohen
2015 — ch.
Verification Tools for Transactional Programs.
Transactional Memory
Adrián Cristal, Burcu Kulahcioglu Ozkan, Ernie Cohen, Gokcen Kestor, Ismail Kuru, Osman S. Unsal, Serdar Tasiran, Suha Orhun Mutluergil, Tayfun Elmas
2014 J jnl
Coherent Causal Memory.
CoRR
Ernie Cohen
2014 J jnl
Hypothesis Elimination in Kleene Semirings.
CoRR
Ernie Cohen
2014 J jnl
Modular Verification of Hybrid System Code with VCC.
CoRR
Ernie Cohen
2014 — conf
Store Buffer Reduction with MMUs.
VSTTE
Geng Chen, Ernie Cohen, Mikhail Kovalev
2014 — ed.
Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers
VSTTE
Ernie Cohen, Andrey Rybalchenko
2013 — ch.
Data Abstraction in VCC.
Engineering Dependable Software Systems
Ernie Cohen
2013 B conf
Theory of Multi Core Hypervisor Verification.
SOFSEM
Ernie Cohen, Wolfgang J. Paul, Sabine Schmaltz
2012 — conf
Verification of TLB Virtualization Implemented in C.
VSTTE
Eyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul
2011 B conf
The 1st Verified Software Competition: Experience Report.
FM
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ß
2010 B conf
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem.
ITP
Ernie Cohen, Bert Schirmer
2010 A* conf
Local Verification of Global Invariants in Concurrent Programs.
CAV
Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies
2010 B conf
Modular specification and verification of interprocess communication.
FMCAD
Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev
2010 B conf
Verifying shadow page table algorithms.
FMCAD
Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul
2009 J jnl
A Better Reduction Theorem for Store Buffers
CoRR
Ernie Cohen, Norbert Schirmer
2009 — conf
A Precise Yet Efficient Memory Model For C.
SSV
Ernie Cohen, Michal Moskal, Stephan Tobies, Wolfram Schulte
2009 — conf
Invariants, Modularity, and Rights.
Ershov Memorial Conference
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
2009 J jnl
Pessimistic Testing
CoRR
Ernie Cohen
2009 — conf
VCC: A Practical System for Verifying Concurrent C.
TPHOLs
Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies
2009 J jnl
Weak Kleene Algebra is Sound and (Possibly) Complete for Simulation
CoRR
Ernie Cohen
2008 J jnl
Using probabilistic Kleene algebra pKA for protocol verification.
J. Log. Algebraic Methods Program.
A. K. McIver, Carlos Gonzalía, Ernie Cohen, Carroll C. Morgan
2006 J jnl
Optimistic synchronization-based state-space reduction.
Formal Methods Syst. Des.
Scott D. Stoller, Ernie Cohen
2006 — conf
Using Probabilistic Kleene Algebra for Protocol Verification.
RelMiCS
Annabelle McIver, Ernie Cohen, Carroll Morgan
2006 B conf
Validating the Microsoft Hypervisor.
FM
Ernie Cohen
2006 — conf
Weak Kleene Algebra and Computation Trees.
RelMiCS
Ernie Cohen
2003 J jnl
First-order Verification of Cryptographic Protocols.
J. Comput. Secur.
Ernie Cohen
2003 A conf
Optimistic Synchronization-Based State-Space Reduction.
TACAS
Scott D. Stoller, Ernie Cohen
2002 — conf
TAPS: The Last Few Slides.
FASec
Ernie Cohen
2000 J jnl
A note on the complexity of propositional Hoare logic.
ACM Trans. Comput. Log.
Ernie Cohen, Dexter Kozen
2000 B conf
Separation and Reduction.
MPC
Ernie Cohen
2000 A* conf
TAPS: A First-Order Verifier for Cryptographic Protocols.
CAV
Ernie Cohen
2000 — conf
TAPS: A First-Order Verifier for Cryptographic Protocols.
CSFW
Ernie Cohen
1998 B conf
Reduction in TLA.
CONCUR
Ernie Cohen, Leslie Lamport
1994 J jnl
The Convergence Span of Greedy Load Balancing.
Inf. Process. Lett.
Ernie Cohen