The Convergence Span of Greedy Load Balancing. - Ernie Cohen (Inf. Process. Lett., 1994)

Reduction in TLA. - Ernie Cohen; Leslie Lamport (CONCUR, 1998)

TAPS: A First-Order Verifier for Cryptographic Protocols. - Ernie Cohen (CSFW, 2000)

Separation and Reduction. - Ernie Cohen (MPC, 2000)

A note on the complexity of propositional Hoare logic. - Ernie Cohen; Dexter Kozen (ACM Trans. Comput. Log., 2000)

TAPS: The Last Few Slides. - Ernie Cohen (FASec, 2002)

First-order Verification of Cryptographic Protocols. - Ernie Cohen (J. Comput. Secur., 2003)

Weak Kleene Algebra and Computation Trees. - Ernie Cohen (RelMiCS, 2006)

Using Probabilistic Kleene Algebra for Protocol Verification. - Annabelle McIver; Ernie Cohen; Carroll Morgan (RelMiCS, 2006)

Validating the Microsoft Hypervisor. - Ernie Cohen (FM, 2006)

Optimistic synchronization-based state-space reduction. - Scott D. Stoller; Ernie Cohen (Formal Methods Syst. Des., 2006)

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)

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; et al. (Ershov Memorial Conference, 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 (TPHOLs, 2009)

A Better Reduction Theorem for Store Buffers - Ernie Cohen; Norbert Schirmer (CoRR, 2009)

Pessimistic Testing - Ernie Cohen (CoRR, 2009)

Weak Kleene Algebra is Sound and (Possibly) Complete for Simulation - Ernie Cohen (CoRR, 2009)

A Precise Yet Efficient Memory Model For C. - Ernie Cohen; Michal Moskal; Stephan Tobies; Wolfram Schulte (SSV, 2009)

Local Verification of Global Invariants in Concurrent Programs. - Ernie Cohen; Michal Moskal; Wolfram Schulte; Stephan Tobies (CAV, 2010)

Verifying shadow page table algorithms. - Eyad Alkassar; Ernie Cohen; Mark A. Hillebrand; Mikhail Kovalev; Wolfgang J. Paul (FMCAD, 2010)

Modular specification and verification of interprocess communication. - Eyad Alkassar; Ernie Cohen; Mark A. Hillebrand; Hristo Pentchev (FMCAD, 2010)

From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. - Ernie Cohen; Bert Schirmer (ITP, 2010)

The 1st Verified Software Competition: Experience Report. - Vladimir Klebanov; Peter Müller 001; Natarajan Shankar; Gary T. Leavens; Valentin Wüstholz; Eyad Alkassar; Rob Arthan; Derek Bronish; Rod Chapman; Ernie Cohen; Mark A. Hillebrand; Bart Jacobs 002; et al. (FM, 2011)

Verification of TLB Virtualization Implemented in C. - Eyad Alkassar; Ernie Cohen; Mikhail Kovalev; Wolfgang J. Paul (VSTTE, 2012)

Theory of Multi Core Hypervisor Verification. - Ernie Cohen; Wolfgang J. Paul; Sabine Schmaltz (SOFSEM, 2013)

Data Abstraction in VCC. - Ernie Cohen (Engineering Dependable Software Systems, 2013)

Store Buffer Reduction with MMUs. - Geng Chen; Ernie Cohen; Mikhail Kovalev (VSTTE, 2014)

Modular Verification of Hybrid System Code with VCC. - Ernie Cohen (CoRR, 2014)

Hypothesis Elimination in Kleene Semirings. - Ernie Cohen (CoRR, 2014)

Coherent Causal Memory. - Ernie Cohen (CoRR, 2014)

Verification Tools for Transactional Programs. - Adrián Cristal; Burcu Kulahcioglu Ozkan; Ernie Cohen; Gokcen Kestor; Ismail Kuru 001; Osman S. Unsal; Serdar Tasiran; Suha Orhun Mutluergil; Tayfun Elmas (Transactional Memory, 2015)

Object-Oriented Security Proofs. - Ernie Cohen (FM, 2018)

A Reduction Theorem for Store Buffers. - Ernie Cohen; Norbert Schirmer (Arch. Formal Proofs, 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 002; Bernardo Portela; Pierre-Yves Strub; Serdar Tasiran (IACR Cryptol. ePrint Arch., 2019)