Orna Lichtenstein

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 VLDB 2026 / reviewers in the wild / expert

dblp:60/6082 · DBLP profile ↗

← Back

2ranked-venue papers

1as first author

0since 2021 · last 1990

—ORCID · none

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

Software engineering, systems software and programming languages · 1 · 1 first-authorTheory of computation · 1

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 2 papers		Automated reasoning and model checking · 73% Logic in computer science · 27%
Software engineering, system software, and programming languages 1 paper		Program verification · 100%

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

Topic	Papers	Last	Evidence papers
Automated reasoning and model checking decision procedures	1	1990	Explicit Clock Temporal Logic · LICS 1990
Automated reasoning and model checking model checking	1	1990	Explicit Clock Temporal Logic · LICS 1990
Automated reasoning and model checking › model checking real-time model checking	1	1990	Explicit Clock Temporal Logic · LICS 1990
Logic in computer science › temporal logic real-time temporal logic	1	1990	Explicit Clock Temporal Logic · LICS 1990
Logic in computer science temporal logic	1	1990	Explicit Clock Temporal Logic · LICS 1990
Automated reasoning and model checking › automated reasoning validity problem	1	1990	Explicit Clock Temporal Logic · LICS 1990
Automated reasoning and model checking › program verification › verification of concurrent systems finite-state concurrent systems	1	1985	Checking That Finite State Concurrent Programs Satisfy Their Linear Specification · POPL 1985
Automated reasoning and model checking › model checking › temporal logic model checking LTL model checking	1	1985	Checking That Finite State Concurrent Programs Satisfy Their Linear Specification · POPL 1985

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

expressive power comparison · 0.0fair computation semantics · 0.0linear-time temporal logic · 0.0linear time temporal logic · 0.0

Year	Publication	Venue	Position
1990	Explicit Clock Temporal Logic abstract The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finite state programs (model checking). The expressive power of XCTL is compared with that of some other logics proposed for the expression of real time properties. It is shown that it is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic).> Eyal Harel, Orna Lichtenstein, Amir Pnueli	LICS	2
1985	Checking That Finite State Concurrent Programs Satisfy Their Linear Specification abstract We present an algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program. The running time of the algorithm is exponential in the size of the formula but linear in the size of the checked program. The algorithm yields also a formal proof in case the formula is valid over the program. The algorithm has four versions that check satisfiability by unrestricted, impartial, just and fair computations of the given program. Orna Lichtenstein, Amir Pnueli	POPL	1