Demo Data from VLDB 2026 / reviewers in the wild / expert
Ernie Cohen
dblp:84/4905
· DBLP profile ↗
18ranked-venue papers
12as first author
0since 2021 · last 2019
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 13 · 9 first-authorSoftware engineering, systems software and programming languages · 8 · 4 first-authorSecurity and privacy · 3 · 2 first-authorDatabases, data management, data science and information retrieval · 1 · 1 first-authorApplied, interdisciplinary, general and emerging computing · 1 · 1 first-author
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Network and information security
3 papers |
Cryptographic protocols and secure computation · 52% Cryptographic primitives and cryptanalysis · 48% | |
| Software engineering, system software, and programming languages
3 papers |
Program verification · 90% Operating systems · 10% | |
| Theoretical computer science
2 papers |
Automated reasoning and model checking · 100% |
Topics — the 8 heaviest of 8, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Cryptographic protocols and secure computation
key management |
0.4 | 1 | 2019 | A Machine-Checked Proof of Security for AWS Key Management Service · CCS 2019 |
Cryptographic primitives and cryptanalysis
provable security |
0.4 | 1 | 2019 | A Machine-Checked Proof of Security for AWS Key Management Service · CCS 2019 |
Program verification
concurrent program verification |
0.1 | 1 | 2010 | Local Verification of Global Invariants in Concurrent Programs · CAV 2010 |
Automated reasoning and model checking › program verification
program invariants |
0.1 | 1 | 2010 | Local Verification of Global Invariants in Concurrent Programs · CAV 2010 |
Program verification › system verification › systems code verification
hypervisor verification |
0.1 | 1 | 2006 | Validating the Microsoft Hypervisor · FM 2006 |
Cryptographic protocols and secure computation
security protocol analysis |
0.0 | 1 | 2000 | TAPS: A First-Order Verifier for Cryptographic Protocols · CAV 2000 |
Automated reasoning and model checking
theorem proving |
0.0 | 1 | 2000 | TAPS: A First-Order Verifier for Cryptographic Protocols · CAV 2000 |
Operating systems › virtualization
hypervisor |
0.0 | 1 | 2006 | Validating the Microsoft Hypervisor · FM 2006 |
Methods — techniques the papers use, named apart from their topics
machine-checked proof · 0.4rely-guarantee reasoning · 0.2compositional verification · 0.2theorem proving · 0.1first-order logic · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 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 0002, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran |
CCS | 5 |
| 2018 | Object-Oriented Security Proofs
Ernie Cohen |
FM | 1 |
| 2013 | Theory of Multi Core Hypervisor Verification
Ernie Cohen, Wolfgang J. Paul, Sabine Schmaltz |
SOFSEM | 1 |
| 2011 | The 1st Verified Software Competition: Experience Report
Vladimir Klebanov, Peter Müller 0001, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Roderick Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs 0002, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß 0001 |
FM | 10 |
| 2010 | Local Verification of Global Invariants in Concurrent Programs
Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies |
CAV | 1 |
| 2010 | Verifying shadow page table algorithms
Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul |
FMCAD | 2 |
| 2010 | Modular specification and verification of interprocess communication
Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev |
FMCAD | 2 |
| 2010 | From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
Ernie Cohen, Norbert Schirmer |
ITP | 1 |
| 2006 | Validating the Microsoft Hypervisor
Ernie Cohen |
FM | 1 |
| 2006 | Optimistic synchronization-based state-space reduction
Scott D. Stoller, Ernie Cohen |
Formal Methods Syst. Des. | 2 |
| 2003 | Optimistic Synchronization-Based State-Space Reduction
Scott D. Stoller, Ernie Cohen |
TACAS | 2 |
| 2003 | First-order Verification of Cryptographic ProtocolsabstractWe describe a verification method for cryptographic protocols, based on first-order invariants. For typical protocols, a suitable invariant can be generated mechanically from the program text, allowing safety properties to be proved by ordinary first-order reasoning. The method has been implemented in an automatic verifier, TAPS, that proves safety properties comparable to those in published Isabelle verifications, but does so much faster with little or no guidance from the user. TAPS has verified properties of about 100 protocols, including all but three protocols from the Clark and Jacob survey; on average, these verifications require less than a second of CPU time and less than 4 bytes of hints from the user. Ernie Cohen |
J. Comput. Secur. | 1 |
| 2000 | TAPS: A First-Order Verifier for Cryptographic Protocols
Ernie Cohen |
CAV | 1 |
| 2000 | TAPS: A First-Order Verifier for Cryptographic ProtocolsabstractWe describe a proof method for cryptographic protocols, based on a strong secrecy invariant that catalogues conditions under which messages can be published. For typical protocols, a suitable first-order invariant can be generated automatically from the program text, independent of the properties being verified, allowing safety properties to be proved by ordinary first-order reasoning. We have implemented the method in an automatic verifier, TAPS, that proves safety properties roughly equivalent to those in published Isabelle verifications, but does so much faster (usually within a few seconds) and with little or no guidance from the user. We have used TAPS to analyze about 60 protocols, including all but three protocols from the Clark and Jacob survey; on average, these verifications each require less than 4 seconds of CPU time and less than 4 bytes of hints from the user. Ernie Cohen |
CSFW | 1 |
| 2000 | Separation and Reduction
Ernie Cohen |
MPC | 1 |
| 2000 | A note on the complexity of propositional Hoare logicabstractWe provide a simpler alternative proof of the PSPACE -hardness of propositional Hoare logic (PHL). Ernie Cohen, Dexter Kozen |
ACM Trans. Comput. Log. | 1 |
| 1998 | Reduction in TLA
Ernie Cohen, Leslie Lamport |
CONCUR | 1 |
| 1994 | The Convergence Span of Greedy Load Balancing
Ernie Cohen |
Inf. Process. Lett. | 1 |