Online Publications

Recent Challenges and Ideas in Temporal Synthesis
SOFTSEM 12 paper
Abstract PDF Bibtex entry

Synthesis with Clairvoyance
HVC 11 paper with Dorsa Sadigh and Sanjit A. Seshia
Abstract PDF Bibtex entry

Max and Sum Semantics for Alternating Weighted Automata
ATVA 11 paper with Shaull Almagor
Abstract PDF Bibtex entry

Formal Analysis of Online Algorithms
ATVA 11 paper with Benajmin Aminof and Robby Lampert
Abstract PDF Bibtex entry

What's Decidable About Weighted Automata?
ATVA 11 paper with Shaull Almagor and Udi Boker
Abstract PDF Bibtex entry

An Abstraction-Refinement Framework for Trigger Querying
SAS 11 paper with Guy Avni
Abstract PDF Bibtex entry

Unifying Buchi Complementation Constructions
CSL 11 paper with Seth Fogarty, Moshe Y. Vardi, and Th. Wilke
Abstract PDF Bibtex entry

Rigorous Approximated Determinization of Weighted Automata
LICS 11 paper with Benjamin Aminof and Robby Lampert
Abstract PDF Bibtex entry

Temporal Specifications with Accumulative Values
LICS 11 paper with Udi Boker, Krishnendu Chatterjee, and Thomas A. Henzinger
Abstract PDF Bibtex entry

Minimizing Deterministic Lattice Automata
FOSSACS 11 paper with Shulamit Halamish
Abstract PDF Bibtex entry

Co-Buching Them All
FOSSACS 11 paper with Udi Boker
Abstract PDF Bibtex entry

Temporal Synthesis for Bounded Systems and Environments
STACS 11 paper with Yoad Lustig, Moshe Y. Vardi, and Mihalis Yannakakis
Abstract PDF Bibtex entry

Partyizing Rabin and Streett
FST & TCS 10 paper with Udi Boker and Avital Steinitz
Abstract PDF Bibtex entry

The Blow-Up in Translating LTL to Deterministic Automata
MOCHART 10 paper with Adin Rosenberg
Abstract PDF Bibtex entry

Promptness in \omega-Automata
ATVA 10 paper with Shaull Almagor and Yoram Hirshfeld
Abstract PDF Bibtex entry

Alternation Removal in Buchi Automata
ICALP 10 paper with Udi Boker and Adin Rosenberg
Abstract PDF Bibtex entry

Coping with Selfish On-going Behaviors
LPAR 10 paper with Tami Tamir
Abstract PDF Bibtex entry

Synthesis of Trigger Properties
LPAR 10 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Variable Automata over Infinite Alphabets
LATA 10 paper with Orna Grumberg and Sarai Sheinvald
Abstract PDF Bibtex entry

Rational Synthesis
TACAS 10 paper with Dana Fisman and Yoad Lustig
Abstract PDF Bibtex entry

Improved Model Checking of Hierarchical Systems
VMCAI 10 paper with Benjamin Aminof and Aniello Murano
Abstract PDF Bibtex entry

Reasoning about Finite-State Switched Systems
HVC 09 paper with Dana Fisman
Abstract PDF Bibtex entry

Co-ing Buchi Made Tight and Useful
LICS 09 paper with Udi Boker
Abstract PDF Bibtex entry

Lower Bounds on Witnesses for Nonemptiness of Universal co-Buchi Automata
FOSSACS 09 paper with Nir Piterman
Abstract PDF Bibtex entry

Reasoning about Online Algorithms with Weighted Automata
SODA 09 paper with Benjamin Aminof and Robby Lampert
Abstract PDF Bibtex entry

A Framework for Inherent Vacuity
HVC 08 paper with Dana Fisman, Sarai Sheinvald, and Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Relative Succinctness of Nondeterministic Buchi and co-Buchi Word Automata
LPAR 08 paper with Benjamin Aminof and Omer Lev
Abstract PDF Bibtex entry

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
FMCAD 08 paper with Wenchao Li and Sanjit S. Seshia
Abstract PDF Bibtex entry

Vacuity in Testing
TAP 08 paper with Thomas Ball
Abstract PDF Bibtex entry

On Verifying Fault Tolerance of Distributed Protocols
TACAS 08 paper with Dana Fisman and Yoad Lustig
Abstract PDF Bibtex entry

What Triggers a Behavior?
FMCAD 07 paper with Yoad Lustig
Abstract PDF Bibtex entry

Latticed Simulation Relations and Games
ATVA 07 paper with Yoad Lustig
Abstract PDF Bibtex entry

Tightening the Exchange Rate Between Automata
CSL 07 paper
Abstract PDF Bibtex entry

Leaping Loops in the Presence of Abstraction
CAV 07 paper with Thomas Ball and Mooly Sagiv
Abstract PDF Bibtex entry

From Liveness to Promptness
CAV 07 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Lattice Automata
VMCAI 07 paper with Yoad Lustig
Abstract PDF Bibtex entry

Better Under-approximation of Programs by Hiding Variables
VMCAI 07 paper with Thomas Ball
Abstract PDF Bibtex entry

On Locally Checkable Properties
LPAR 06 paper with Yoad Lustig and Moshe Vardi
Abstract PDF Bibtex entry

On the Construction of Fine Automata for Safety Properties
ATVA 06 paper with Robby Lampert
Abstract PDF Bibtex entry

On The Succinctness of Nondeterminizm
ATVA 06 paper with Benjamin Aminof
Abstract PDF Bibtex entry

Sanity Checks in Formal Verification
CONCUR 06 paper
Abstract PDF Bibtex entry

Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
CONCUR 06 paper with Sarai Sheinvald-Faragy
Abstract PDF Bibtex entry

Safraless Compositional Synthesis
CAV 06 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Avoiding Determinization
LICS 06 paper
Abstract PDF Bibtex entry

An Abstraction-Refinement Framework for Multi-Agent Systems
LICS 06 paper with Thomas Ball
Abstract PDF Bibtex entry

Memoryful Branching-Time Logics
LICS 06 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Safraless Decision Procedures
FOCS 05 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Abstraction for Falsification
CAV 05 paper with Thomas Ball and Greta Yorsh
Abstract PDF Bibtex entry

Regular Vacuity
CHARME 05 paper with Doron Bustan, Alon Flaisher, Orna Grumberg, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Verifying Quantitative Properties Using Bound Functions
CHARME 05 paper with Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, and Rupak Majumdar
Abstract PDF Bibtex entry

Complementation Constructions for Nondeterministic Automata on Infinite Words
TACAS 05 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Reasoning about Systems with Transition Fairness
LPAR 04 paper with Benjamin Aminof and Thomas Ball
Abstract PDF Bibtex entry

Typeness for \omega-Regular Automata
ATVA 04 paper with Gila Morgenstern and Aniello Murano
Abstract PDF Bibtex entry

Buchi Complementation Made Tighter
ATVA 04 paper with Ehud Friedgut and Moshe Y. Vardi
Abstract PDF Bibtex entry

A Measured Collapse of The Modal \mu-Calculus Alternation Hierarchy
STACS 04 paper with Doron Bustan and Moshe Y. Vardi
Abstract PDF Bibtex entry

From Complementation to Certification
TACAS 04 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Coverage Metrics for Formal Verification
CHARME 03 paper with Hana Chockler and Moshe Y. Vardi
Abstract PDF Bibtex entry

On Complementing Nondeterministic Buchi Automata
CHARME 03 paper with Sankar Gurumurthy, Fabio Somenzi, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Formal Analysis of Scientific-Computation Methods
ADHS 03 paper with Gadi Auerbach
Abstract PDF Bibtex entry

\Pi_2 \cap \Sigma_2 = AFMC
ICALP 03 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Universal and Existential Fragments of the \mu-Calculus
TACAS 03 paper with Thomas A. Henzinger and Rupak Majumdar
Abstract PDF Bibtex entry

Resets vs. Aborts in Linear Temporal Logic
TACAS 03 paper with Roi Armoni, Doron Bustan, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Pushdown Specifications
LPAR 02 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

\omega-regular Languages are Testable with a Constant Number of Queries
RANDOM 02 paper with Hana Chockler
Abstract PDF Bibtex entry

Trading Probability for Fairness
CSL 02 paper with Marcin Jurdzinski and Thomas Henzinger
Abstract PDF Bibtex entry

An Improved Algorithm for the Membership Problem for Extended Regular Expressions
MFCS 02 paper with Sharon Zuhovitzky
Abstract PDF Bibtex entry

Coverage of implementations by simulating specifications
TCS 02 paper with Hana Chockler
Abstract PDF Bibtex entry

The Complexity of the Graded \mu-Calculus
CADE 02 paper with Ulrike Sattler and Moshe Y. Vardi
Abstract PDF Bibtex entry

Model Checking Linear Properties of Prefix-Recognizable Systems
CAV 02 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Synthesis of Uninitialized Systems
ICALP 02 paper with Thomas A. Henzinger, Sriram C. Krishnan, and Freddy Y.C. Mang
Abstract PDF Bibtex entry

On Clopen Specifications
LPAR 01 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Extended Temporal Logic Revisited
CONCUR 01 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

A Practical Approach to Coverage in Model Checking
CAV 01 paper with Hana Chockler, Robert P. Kurshan, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Synthesizing Distributed Systems
LICS 01 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Complexity of Parity Word Automata
FOSSACS 01 paper with Valerie King and Moshe Y. Vardi
Abstract PDF Bibtex entry

Coverage Metrics for Temporal Logic Model Checking
TACAS 01 paper with Hana Chockler and Moshe Y. Vardi
Abstract PDF Bibtex entry

Fair Equivalence Relations
FST & TCS 00 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Branching-Depth Hierarchies
EXPRESS 00 paper with Shoham Shamir and Eli Shamir
Abstract PDF Bibtex entry

\mu-Calculus Synthesis
MFCS 00 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Open Systems in Reactive Environments: Control and Synthesis
CONCUR 00 paper with P. Madhusudan, P.S. Thiagarajan, and Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Behavioral Inheritance of State-Based Objects.
TOOLS 00 paper with David Harel
Abstract PDF Bibtex entry

An Automata-Theoretic Approach to Reasoning about Infinite-State Systems.
CAV 00 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Vacuity Detection in Temporal Model Checking.
CHARME 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Robust Satisfaction.
CONCUR 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Model Checking of Safety Properties.
CAV 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

The Weakness of Self-Complementation.
STACS 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Concurrent Reachability Games.
FOCS 98 paper with Luca de Alfaro and Thomas A. Henzinger
Abstract PDF Bibtex entry

Alternating Refinement Relations.
CONCUR 98 paper with Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi
Abstract PDF Bibtex entry

From Pre-historic to Post-modern Symbolic Model Checking.
CAV 98 paper with Thomas A. Henzinger and Shaz Qadeer
Abstract PDF Bibtex entry

Freedom, Weakness, and Determinism: From Linear-time to Branching-time.
LICS 98 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Weak Alternating Automata and Tree Automata Emptiness.
STOC 98 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Relating Linear and Branching Model Checking.
PROCOMET 98 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Modular Model Checking.
Compositionality 97 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Alternating-Time Temporal Logic.
FOCS 97 paper with Rajeev Alur and Thomas A. Henzinger
Abstract PDF Bibtex entry

Existence of Reduction Hierarchies.
CSL 97 paper with Robert P. Kurshan and Mihalis Yannakakis.
Abstract PDF Bibtex entry

Synthesis with Incomplete Informatio.
ICTL 97 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

On the Complexity of Verifying Concurrent Transition Systems.
CONCUR 97 paper with David Harel and Moshe Y. Vardi.
Abstract PDF Bibtex entry

Fair Simulation.
CONCUR 97 paper with Thomas A. Henzinger and Sriram Rajamani.
Abstract PDF Bibtex entry

Weak Alternating Automata are not That Weak.
ISTCS 97 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Module Checking Revisited.
CAV 97 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

From Quantity to Quality.
HART 97 paper with Thomas A. Henzinger.
Abstract PDF Bibtex entry

A Space-efficient On-the-fly Algorithm for Real-time Model Checking.
CONCUR 96 paper with Thomas A. Henzinger and Moshe Y. Vardi.
Abstract PDF Bibtex entry

Not Checking for Closure under Stuttering.
SPIN 96 paper with Gerard Holzmann.
Abstract PDF Bibtex entry

Verification of Fair Transition Systems.
CAV 96 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Module Checking.
CAV 96 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Relating Word and Tree Automata.
LICS 96 paper with Samuel Safra and Moshe Y. Vardi.
Abstract PDF Bibtex entry

Model Checking for Branching-Time Temporal Logics.
Ph.D. Thesis.
Abstract PDF Bibtex entry

On the Complexity of Branching Modular Model Checking.
CONCUR 95 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions.
CAV 95 paper.
Abstract PDF Bibtex entry

Once and For all.
LICS 95 paper with Amir Pnueli.
Abstract PDF Bibtex entry

Buy One, Get One Free!!!
ICTL 94 paper with Orna Grumberg.
Abstract PDF Bibtex entry

An Automata-Theoretic Approach to Branching-Time Model Checking.
CAV 94 paper with Moshe Y. Vardi and Pierre Wolper.
Abstract PDF Bibtex entry

Branching-Time Temporal Logic and Tree Automata.
CONCUR 93 paper with Orna Grumberg.
Abstract PDF Bibtex entry

Back to Home page