Demo Data from EDBT 2026 / reviewers in the wild / expert
Yonit Kesten
dblp:11/934
· DBLP profile ↗
18ranked-venue papers
17as first author
0since 2021 · last 2006
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 17 · 16 first-authorSoftware engineering, systems software and programming languages · 4 · 4 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
7 papers |
Automated reasoning and model checking · 36% Logic in computer science · 36% Automata and formal languages · 12% |
Topics — the 14 heaviest of 15, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Logic in computer science
concurrency theory |
0.1 | 1 | 2005 | Bridging the gap between fair simulation and trace inclusion · Inf. Comput. 2005 |
Automated reasoning and model checking › program verification › verification of concurrent systems
fair simulation |
0.0 | 1 | 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion · CAV 2003 |
Distributed computing theory
simulation relations |
0.0 | 1 | 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion · CAV 2003 |
Automated reasoning and model checking › automata-based verification
trace containment |
0.0 | 1 | 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion · CAV 2003 |
Logic in computer science › temporal logic
linear temporal logic |
0.0 | 2 | 1998 | Algorithmic Verification of Linear Temporal Logic Specifications · ICALP 1998 A Decision Algorithm for Full Propositional Temporal Logic · CAV 1993 |
Automata and formal languages
infinite-state systems |
0.0 | 1 | 1999 | Decidable Integration Graphs · Inf. Comput. 1999 |
Automated reasoning and model checking
temporal logic verification |
0.0 | 1 | 1998 | Algorithmic Verification of Linear Temporal Logic Specifications · ICALP 1998 |
Logic in computer science › program logic
assertion language |
0.0 | 1 | 1997 | Symbolic Model Checking with Rich ssertional Languages · CAV 1997 |
Automated reasoning and model checking › model checking
symbolic model checking |
0.0 | 1 | 1997 | Symbolic Model Checking with Rich ssertional Languages · CAV 1997 |
Logic in computer science
proof theory |
0.0 | 1 | 1995 | A Complete Proof Systems for QPTL · LICS 1995 |
Logic in computer science
temporal logic |
0.0 | 1 | 1995 | A Complete Proof Systems for QPTL · LICS 1995 |
Computational complexity › decidability › decision problems for automata
language inclusion |
0.0 | 1 | 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion · CAV 2003 |
Automated reasoning and model checking › decision procedures
temporal logic decision procedures |
0.0 | 1 | 1993 | A Decision Algorithm for Full Propositional Temporal Logic · CAV 1993 |
Automata and formal languages › omega-automata
büchi automata |
0.0 | 1 | 1995 | A Complete Proof Systems for QPTL · LICS 1995 |
Methods — techniques the papers use, named apart from their topics
trace inclusion · 0.1fair simulation · 0.1simulation relation analysis · 0.0presburger arithmetic · 0.0decidability · 0.0symbolic model checking · 0.0equivalence transformations · 0.0automata reduction · 0.0decision procedure · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2006 | Model Checking with Strong Fairness
Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar |
Formal Methods Syst. Des. | 1 |
| 2005 | Bridging the gap between fair simulation and trace inclusion
Yonit Kesten, Nir Piterman, Amir Pnueli |
Inf. Comput. | 1 |
| 2005 | A compositional approach to CTL* verification
Yonit Kesten, Amir Pnueli |
Theor. Comput. Sci. | 1 |
| 2003 | Bridging the Gap between Fair Simulation and Trace Inclusion
Yonit Kesten, Nir Piterman, Amir Pnueli |
CAV | 1 |
| 2002 | Network Invariants in Action
Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck |
CONCUR | 1 |
| 2002 | A Deductive Proof System for CTL
Amir Pnueli, Yonit Kesten |
CONCUR | 2 |
| 2002 | Complete Proof System for QPTLabstractThe paper presents an axiomatic system for quantified propositional temporal logic (QPTL), which is propositional temporal logic equipped with quantification over propositions (Boolean variables). The advantages of this extended temporal logic is that its expressive power is strictly higher than that of the unquantified version (PTL) and is equal to that of S1S, as well as that of ω‐automata. Another important application of QPTL is its use for formulating and verifying refinement relations between reactive systems. In fact, the completeness proof is based on the reduction of a QPTL formula into a Büchi automaton, and performing equivalence transformations on this automaton, formally justifying these transformations as a bi‐directional refinement. Yonit Kesten, Amir Pnueli |
J. Log. Comput. | 1 |
| 2001 | Verification by Augmented Abstraction: The Automata-Theoretic View
Yonit Kesten, Amir Pnueli, Moshe Y. Vardi |
J. Comput. Syst. Sci. | 1 |
| 2001 | Symbolic model checking with rich assertional languages
Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
Theor. Comput. Sci. | 1 |
| 2000 | Verification of Clocked and Hybrid Systems
Yonit Kesten, Zohar Manna, Amir Pnueli |
Acta Informatica | 1 |
| 2000 | Verification by Augmented Finitary Abstraction
Yonit Kesten, Amir Pnueli |
Inf. Comput. | 1 |
| 2000 | Control and Data Abstraction: The Cornerstones of Practical Formal Verification
Yonit Kesten, Amir Pnueli |
Int. J. Softw. Tools Technol. Transf. | 1 |
| 1999 | Decidable Integration Graphs
Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine |
Inf. Comput. | 1 |
| 1998 | Algorithmic Verification of Linear Temporal Logic Specifications
Yonit Kesten, Amir Pnueli, Li-on Raviv |
ICALP | 1 |
| 1998 | Modularization and Abstraction: The Keys to Practical Formal Verification
Yonit Kesten, Amir Pnueli |
MFCS | 1 |
| 1997 | Symbolic Model Checking with Rich ssertional Languages
Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
CAV | 1 |
| 1995 | A Complete Proof Systems for QPTLabstractThe paper presents an axiomatic system for quantified propositional temporal logic (QPTL), which is propositional temporal logic equipped with quantification over propositions (boolean variables). The advantages of this extended temporal logic is that its expressive power is strictly higher than that of the unquantified version (PTL) and is equal to that of SIS, as well as that of /spl omega/-automata. Another important application of QPTL is its use for formulating and verifying refinement relations between reactive systems. In fact, the completeness proof is based on the reduction of a QPTL formula into a Buchi automaton, and performing equivalence transformations on this automata, formally justifying these transformations. Yonit Kesten, Amir Pnueli |
LICS | 1 |
| 1993 | A Decision Algorithm for Full Propositional Temporal Logic
Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli |
CAV | 1 |