Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data. A simulation from public publication records: the people listed were not invited and did not agree to review.
? Tutorial for this page
Demo Data from EDBT 2026 / reviewers in the wild / expert

Ariel Cohen 0002

dblp:c/ArielCohen2 · DBLP profile ↗
← Back
8ranked-venue papers
7as first author
0since 2021 · last 2010
0009-0003-7981-2262ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 7 · 6 first-authorTheory of computation · 7 · 7 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.

Theoretical computer science
4 papers
Logic in computer science · 100%
Software engineering, system software, and programming languages
5 papers
Program verification · 85% Concurrent programming · 15%

Topics — the 6 heaviest of 8, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program verification
concurrent program verification		 0.442010
SPLIT: A Compositional LTL Verifier · CAV 2010
A Dash of Fairness for Compositional Reasoning · CAV 2010
Local Proofs for Linear-Time Properties of Concurrent Programs · CAV 2008
Logic in computer science
temporal logic		 0.222010
SPLIT: A Compositional LTL Verifier · CAV 2010
Local Proofs for Linear-Time Properties of Concurrent Programs · CAV 2008
Logic in computer science › temporal logic
linear temporal logic		 0.112010
SPLIT: A Compositional LTL Verifier · CAV 2010
Concurrent programming
memory models		 0.112008
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses · CAV 2008
Logic in computer science › temporal logic
linear-time properties		 0.112008
Local Proofs for Linear-Time Properties of Concurrent Programs · CAV 2008
Logic in computer science › temporal logic
safety properties		 0.112007
Local Proofs for Global Safety Properties · CAV 2007

Methods — techniques the papers use, named apart from their topics

compositional verification · 0.5local reasoning · 0.3compositional reasoning · 0.2theorem proving · 0.1mechanical verification · 0.1
YearPublicationVenuePosition
2010 A Dash of Fairness for Compositional Reasoning
Ariel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa'ar
 CAV1
2010 SPLIT: A Compositional LTL Verifier
Ariel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa'ar
 CAV1
2009 Local proofs for global safety properties
Ariel Cohen 0002, Kedar S. Namjoshi
 Formal Methods Syst. Des.1
2008 Local Proofs for Linear-Time Properties of Concurrent Programs
Ariel Cohen 0002, Kedar S. Namjoshi
 CAV1
2008 Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
Ariel Cohen 0002, Amir Pnueli, Lenore D. Zuck
 CAV1
2007 Local Proofs for Global Safety Properties
Ariel Cohen 0002, Kedar S. Namjoshi
 CAV1
2007 Verifying Correctness of Transactional Memories
abstract
We show how to verify the correctness of transactional memory implementations with a model checker. We show how to specify transactional memory in terms of the admissible interchange of transaction operations, and give proof rules for showing that an implementation satisfies this specification. This notion of an admissible interchange is a key to our ability to use a model checker, and lets us capture the various notions of transaction conflict as characterized by Scott. We demonstrate our work using the TLC model checker to verify several well-known implementations described abstractly in the TLA+ specification language.
Ariel Cohen 0002, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck
 FMCAD1
2006 Ranking Abstraction of Recursive Programs
Ittai Balaban, Ariel Cohen 0002, Amir Pnueli
 VMCAI2