Temporal Synthesis for Bounded Systems and Environments
(full version of STACS'11 paper with O. Kupferman and M. Yannakakis).
Optimized Temporal Monitors for SystemC
(full version of RV'10 paper with D. Tabakov).
Symbolic Systems, Explicit Properties:
on Hybrid Approaches for LTL Symbolic Model Checking
(full version of CAV'05 paper with R. Sebastiani and S. Tonetta).
Synthesis from Component Libraries
(full version of FOSSACS'09 paper with Y. Lustig).
State of Buechi Complementation
(full version of CIAA'10 paper with S. Fogarty, M.-H.~Tsai, and
Y.-K.~Tsay).
Monitoring Temporal SystemC Properties
(MEMOCODE'10 paper with D. Tabakov),
with
code.
Relentful Strategic Reasoning in Alternating-Time Temporal Logic
(LPAR'10 paper with F. Mogavero and A. Murano).
Synthesis of Trigger Properties
(LPAR'10 paper with O. Kupferman).
Sampling-based Motion Planning with Temporal Goals
(ICRA'10 paper with A. Bhatia and L. Kavraki).
Node Selection Query Languages for Trees
(long version of AAAI'10 paper with D. Calvanese, G. De Giacomo,
and M. Lenzerini).
Buechi Complementation and Size-Change Termination
(full version of TACAS'09 paper with S. Fogarty).
LTL Satisfiability Checking
(Full version of SPIN'07 paper with K. Rozier).
Efficient Buechi Universality Checking
(TACAS'10 paper with S. Fogarty).
Symbolic Techniques in Propositional Satisfiability Solving
(invited talk at SAT'09).
An Automata-Theoretic Approach to Regular XPath
(DBPL'09 paper with D. Calvanese, G. De Giacomo, and M. Lenzerini).
Trace Semantics Is Fully Abstract
(LICS'09 paper with S. Nain)
with full version.
Buechi Complementation and Size-Change Termination
(TACAS'09 paper with S. Fogarty).
Falsification of LTL Safety Properties in Hybrid Systems
(TACAS'09 paper with E. Plaku and L. Kavraki).
Synthesis from Component Libraries
(FOSSACS'09 paper with Y. Lustig).
From Philosophical to Industrial Logics
(invited ICLA'09 paper).
A Framework for Inherent Vacuity
(HVC'08 paper with D. Fisman, S. Sheinvald-Faragy, and O. Kupferman).
A Temporal Language for SystemC
(FMCAD'08 paper with D. Tabakov, G. Kamhi, and E. Singerman).
Intelligate: Scalable Dynamic Invariant Learning for Power Reduction
(PATMOS'08 paper with G. Kamhi, and R. Wiener).
The Complexity of Relational Queries: Personal Perspective
(SIGMOD'08 Codd Award presentation).
Impact of Workspace Decomposition on Discrete Search Leading
Contiuous Exploration (DSLX) Motion Planning
(ICRA'08 paper with E. Plaku and L. Kavraki).
The Complexity of Enriched Mu-Calculi
(Full version of ICALP'06 paper with with P. Bonati, C. Lutz, and A. Murano).
CACM: Past, Present, and Future
(Essay in CACM, January 2008).
Automata: From Logics to Algorithms
(WAL'07 paper with T. Wilke).
Hybrid Systems: From Verification to Falsification
(Full version of CAV'07 paper with E. Plaku and L. Kavraki).
From Liveness to Promptness
(Full version of CAV'07 paper with O. Kupferman and N. Piterman).
From Monadic Logic and Prior to PSL
(paper in Festschrift for Boaz Trakhtenbrot).
Branching vs. Linear Time: Semantical Perspective
(invited ATVA'07 paper with S. Nain),
Version 1.1,
Version 1.2,
slides,
,
a reply by Robin Milner and
a second reply by Robin Milner.
An Analysis of Slow Convergence in Interval Propagation
(CP'07 paper with L. Bordeaux and Y. Hamadi).
Pushdown Module Checking
(CONCUR'07 paper with B. Aminoff and A. Murano).
Discrete Search Leading Continuous Exploration for Kynodynamic
Motion Planning
(RSS'07 paper with E. Plaku and L. Kavraki).
LTL Satisfiability Checking
(SPIN'07 paper with K. Rozier).
From Liveness to Promptness
(CAV'07 paper with O. Kupferman and N. Piterman).
Hybrid Systems: From Verification to Falsification
(CAV'07 paper with E. Plaku and L. Kavraki).
Globalization and Offshoring of Software
(book chapter with W. Aspray and F. Mayadas).
Formal Techniques for SystemC Verification
(DAC'07 paper).
Groebner Bases Computation in Boolean Rings for Symbolic Model
Checking
(IASTED'07 paper with Q. Tran).
Multi-Objective Model Checking of Markov Decision Processes
(TACAS'07 paper with K. Etessami, M. Kwiatkowska, and
M. Yannakakis).
Property-Driven Partitioning for Abstraction Refinement
(TACAS'07 paper with R. Sebastiani and S. Tonetta).
Model Checking Buechi Specifications
(LATA'07 paper with D. Tabakov).
From Church and Prior to PSL
(25MC paper).
A Motion Planner for a Hybrid Robotic System with Kinodynamic
Constraints
(ICRA'07 paper with E. Plaku and L. Kavraki).
PowerQuest: Trace Driven Data Mining for Power Optimization
(DATE'07 paper with P. Babighian and G. Kamhi).
GSTE Is Partitioned Model Checking
(Full version of CAV'04 paper with R. Sebastiani, E. Singerman,
and S. Tonetta).
The Buechi complementation saga
(invited STACS'07 paper).
Automata-theoretic model checking revisited
(invited VMCAI'07 paper).
Deeper bound in BMC by combining constant propagation and
abstraction
(ASP-DAC'07 paper with R. Armoni, L. Fix, R. Fraer, T. Heyman,
Y. Vizel, and Y. Zbar).
Proving that programs eventually do something good
(POPL'07 paper with with B. Cook, A. Gotsman, A. Podelski,
and A. Riybalchenko).
A logical Approach to Constraint Satisfaction
(chapter in Finite-Model Theory and Its Applications,
with P. Kolaitis).
Aggregating Disparate Estimates of Chance
(paper in Games and Economic Behavior with D. Osherson).
Verification of Open Systems
(chapter in Interactive Computation, with O. Kupferman).
On Locally Checkable Properties
(LPAR'06 paper with with O. Kupferman and Y. Lustig).
From Verification to Synthesis
(slides of invited talk at FMCO'06).
The Complexity of Enriched Mu-Calculi
(ICALP'06 paper with with P. Bonati, C. Lutz, and A. Murano).
Automata-Theoretic Techniques for Temporal Reasoning
(chapter in the Handbook of Modal Logic).
Deterministic Dynamic Monitors for Linear-Time Assertions
(FATES/RV'06 paper with
R. Armoni, D. Korchemny, A. Tiemeyer and Y. Zbar).
Fixed-Parameter Hierarchies inside PSPACE
(LICS'06 paper with with G. Pan).
Memoryful Branching-Time Logic
(LICS'06 paper with with O. Kupferman).
Safraless Compositional Synthesis
(CAV'06 paper with with O. Kupferman and N.Piterman).
Panel: Educational Response to Offshore Outsourcing
(SIGCSE'06 panel with W. Aspray, F. Mayadas, and S. Zweben) with
Vardi's panel statement,
Aspray's panel statement,
Zweben's panel statement.
Panel: Automata Theory . Its Relevance to Computer Science
Students and Course Contents
(SIGCSE'06 panel with M. Armoni, S. Rodger, and R. Verma) and
panel statement.
BDD-Based Decision Procedures for the Modal Logic K
(full version of CADE'02 and CADE'03 with G. Pan and U. Sattler).
Safraless Decision Procedures
(full version of FOCS'05 paper with O. Kupferman).
The Planning Spectrum --- One, Two, Three, Infinity
(full version of LICS'03 paper with M. Pistore).
Treewidth in Verification: Local vs. Global
(LPAR'05 paper with A. Ferrara and G. Pan).
Evaluating Classical Automata-Theoretic Algorithms
(LPAR'05 paper with D. Tabakov).
Efficient LTL-Compilation for SAT-Based Model Checking
(ICCAD'05 paper with R. Armony, S. Egorov, R. Fraer,
and D. Korchemny).
Regular Vacuity
(CHARME'05 paper with D. Bustan, A. Flaisher, O. Grumberg,
and O. kKupferman).
A Continuous-Discontinuous Transition in The Satisfiability of
Random Horn Formulas
(Random'05 paper with C. Moore, G. istrate, and D. Demopoulos).
Buechi Complementation: A Forty-Year Saga
(invited extended abstract in ALC'05).
From Linear-time to Branching-time
(Full version of LICS'98 paper with O. Kupferman).
BDD-Based Decision Procedures for The Modal Logic K
(Full version of IJCAR'02+CADE'03 papers with G. Pan and U.
Sattler).
Symbolic Techniques in Satisfiability Solving
(Full version of SAT'04 paper with G. Pan).
Symbolic Systems, Explicit Properties:
on Hybrid Approaches for LTL Symbolic Model Checking
(CAV'05 paper with R. Sebastiani and S. Tonetta).
Formal Verification of Backward Compatibility of Microcode
(CAV'05 paper with T. Arons, E. Elster, L. Fix, S. Mador-Haim,
M. Mishaeli, J. Shalev, E. Singerman, A. Tiemeyer, and L. Zuck).
Buchi Complementation Made Tighter
(Full version of ATVA'04 paper with E. Friedgut and O. Kupferman).
Complementation Constructions for Nondeterministic Automata on Infinite
Words
(TACAS'05 paper with O. Kupferman).
Model Checking for Database Theoreticians
(Invited ICDT'05 paper) and
talk.
View-based Query Processing:
On the Relationship between Rewriting, Answering and Losslessness
(ICDT'05 paper with D. Calvanese, G. De Giacomo, and M. Lenzerini).
Decidable Containment of Recursive Queries
(Full version of ICDT'03 paper with D. Calvanese and D. De Giacomo).
Coverage Metrics for Formal Verification
(Full version of CHARME'03 paper with H. Chockler and O. Kupferman).
Buchi Complementation Made Tighter
(ATVA'04 paper with E. Friedgut and O. Kupferman).
Aggregating Disparate Estimates of Chance
(Games and Econimic Behavior paper with D. Osherson).
Pattern Search in Hierarchical High-Level Designs
(ICECS'04 paper with G. Kamhi, Z. Terem, and A. Irron).
Relating Word and Tree Automata
(full version of LICS'96 paper with O. Kupferman and S. Safra).
From Complementation to Certification
(Full version of TACAS'04 paper with O. Kupferman).
Symbolic Decision Procedures for QBF
(CP'04 paper with G. Pan).
Constraint Propagation as A Proof System
(CP'04 paper with A. Atserias and P. Kolaitis).
SAT-based Induction for Temporal Safety Properties
(BMC'04 paper with R. Armoni, L. Fix, R. Fraer, S. Huddleston,
and N. Piterman).
Global Model Checking of Infinite-State Systems
(CAV'04 paper with N. Piterman).
GSTE Is Partitioned Model Checking
(CAV'04 paper with R. Sebastiani, E. Singerman, and S. Tonetta).
Verifying omega-Regular Properties of Markov Chains
(CAV'04 paper with D. Bustan and S. Rubin).
Search vs. Symbolic Techniques in Satisfiability Solving
(SAT'04 paper with G. Pan).
Complete Axiomatizations for Reasoning About Knowledge and Time
(SICOMP paper with J.Y. Halpern and R. van der Meyden).
The phase transition in the random 1-3-HornSAT problem
(Special Volume on Computational Complexity and Statistical Physics
paper with D. Demopoulos).
From Complementation to Certification
(TACAS'04 paper with O. Kupferman).
A Measured Collapse of The Modal Mu-Calculus Alternation Hierarchy
(STACS'04 paper with D. Bustan and O. Kupferman).
Projection Pushing Revisited
(EDBT04'04 paper with B. McMahan, G. Pan, and P. Porter).
Reasoning on Regular Path Queries
(SIGMOD Record paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Coverage Metrics for Formal Verification
(CHARME'03 paper with H. Chockler and O. Kupferman).
On Complementing Nondeterministic Buechi Automata
(CHARME'03 paper with S. Gurumurthy, O. Kupferman, and F. Somenzi).
Fair Equivalence Relations
(Full version of FST&TCS'00 paper with O. Kupferman and N. Piterman).
Automated verification = graphs, logic, and automata.
(invited IJCAI'03 paper).
Enhanced Vacuity Detection in Linear Temporal Logic
(CAV'03 paper with R. Armoni, L. Fix, A. Flaisher, O. Grumberg,
N. Piterman, A. Tiemeyer).
Optimizing a BDD-based Modal Solver
(CADE'03 paper with G. Pan).
Pi_2 Intersect Sigma_2 = AFMC
(ICALP'03 paper with O. Kupferman).
Micro-Macro Stack Systems:
A New Frontier of Elementary Decidability for Sequential Systems
(LICS'03 paper with N. Piterman).
The Planning Spectrum: One, Two, Three, Infinity
(LICS'03 paper with M. Pistore).
Homomorphism Closed vs Existential Positive
(LICS'03 paper with T. Feder).
View-Based Query Containment
(PODS'03 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Multiple-Counterexample Guided Iterative Abstraction Refinement:
An Industrial Evaluation
(TACAS'03 paper with M. Glusman, G. Kamhi, S. Mador-Haim,
and R. Fraer).
Aborts vs Resets in Linear Temporal Logic
(TACAS'03 paper with R. Armony, D. Bustan, and O. Kupferman).
Decidable Containment of Recursive Queries
(ICDT'03 paper with D. Calvanese and D. De Giacomo).
Pushdown Specifications
(LPAR'02 paper with O. Kupferman and N. Piterman).
Constraint Satisfaction, Bounded Treewidth, and Finite-Variable Logics
(CP'02 paper with P. Kolaitis and V. Dalmau).
First-Order Logic with Two Variables and Unary Temporal Logic
(full version of LICS'97 paper with K. Etessami and T. Wilke).
BDD-Based Decision Procedures for K
(CADE'02 paper with G. Pan and U. Sattler).
The Complexity of the Graded Mu-Calculus
(CADE'02 paper with O. Kupferman and U. Sattler).
Model Checking Linear Properties of Prefix-Recognizable Systems
(CAV'02 paper with O. Kupferman and N. Piterman).
Lossless Regular Views
(PODS'02 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Coverage Metrics for Temporal Logic Model Checking
(Full version of TACAS'01 paper with Chockler and Kupferman).
Reasoning about Actions and Planning in LTL Action Theories
(KR'02 paper with D. Calvanese and G. De Giacomo).
Eliminating Incoherence from Subjective Estimates of Chance
(KR'02 paper with R. Batsell, L. Brenner, D. Osherson, and
S. Tsavachidis).
The ForSpec Temporal Logic:
A New Temporal Property-Specification Language
(TACAS'02 paper with many co-authors) and
ForSpec Reference Manual.
On Bounded Specifications
(LPAR'01 paper with Kupferman).
From Bidirectionality to Alternation
(Full version of MFCS'01 paper with Piterman).
View-based Query Answering and Query Containment over
Semistructured Data
(DBPL'01 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Random 3-SAT and BDDs: The Plot Thickens Further
(CP'01 paper with A. San Miguel Aguirre).
Towards an Efficient Library for SAT: a Manifesto
(LICS'01 SAT Workshop paper with Giunchiglia,
Narizzano, and Tacchella).
From Bidirectionality to Alternation
(MFCS'01 paper with Piterman).
Extended Temporal Logic Revisited
(CONCUR'01 paper with Kupferman and Piterman).
Random 3-SAT: The Plot Thickens
(Full version of CP'00 paper with C. Coarfa, D.D. Demopoulos,
A. San Miguel Aguirre and D. Subramanian).
A Practical Approach to Coverage in Model Checking
(CAV'01 paper with Chokler, Kupferman, and Kurshan).
Benefits of Bounded Model Checking at an Industrial Setting
(CAV'01 paper with Copty, Fix, Fraer, Guinchiglia, Kamhi,
and Tacchella).
The Hybrid Mu-Calculus
(IJCAR'01 paper with Sattler).
Synthesizing Distributed Systems
(LICS'01 paper with Kupferman).
On the Unusual Effectiveness of Logic in Computer Science
(BSL submission with Halpern, Harper, Immerman, Kolaitis, and
Vianu).
Branching vs. Linear Time: Final Showdown
Version 1.0,
Version 1.1,
Version 1.2, and
Version 1.3
(invited ETAPS'01 paper) and
talk.
On the Complexity of Parity Word Automata
(FOSSACS'01 paper with King and Kupferman).
Coverage Metrics for Temporal Logic Model Checking
(TACAS'01 paper with Chockler and Kupferman).
Is There a Best Symbolic Cycle-Detection Algorithm?
(TACAS'01 paper with Fisler, Fraer, Kamhi, and Yang).
Strong Cyclic Planning Revisited
(ECP'99 paper with Daniele and Traverso).
Weak Alternating Automata Are Not That Weak
(Full version of ISTCS'97 paper with O. Kupferman).
Vacuity Detection in Temporal Model Checking
(Full version of CHARME'99 paper with O. Kupferman).
Fair Equivalence Relations
(FST&TCS'00 paper with O. Kupferman and N. Piterman).
On the Complexity of Verifying Concurrent Transition Systems
(Full version of CONCUR'97 paper with D. Harel and O. Kupferman).
Open Systems in Reactive Environments: Control and Synthesis
(CONCUR'00 paper with O. Kupferman, P. Madhusudan, and
P.S. Thiagarajan).
0-1 Laws for Fragments of Existential Second-Order Logic: A Survey
(Invited MFCS'00 paper with P.G. Kolaitis).
Prioritized Traversal: Efficient Reachability Analysis for
Verification and Falsification
(CAV'00 paper with R. Fraer, G. Kamhi, B. Ziv,
and L. Fix).
Random 3-SAT: The Plot Thickens
(CP'00 paper with C. Coarfa, D.D. Demopoulos, A. San Miguel
Aguirre and D. Subramanian).
View-based Query Processing and Constraint Satisfaction
(LICS'00 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Mu-calculus Synthesis
(MFCS'00 paper with O. Kupferman).
What is View-Based Query Rewriting?
(KRDB'00 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
An Automata-Theoretic Approach to Reasoning about
Infinite-State Systems
(CAV'00 paper with O. Kupferman).
A Game-Theoretic Approach to Constraint Satisfaction
(AAAI'00 paper with P. Kolaitis).
An Automata-Theoretic Approach to Modular Model Checking
(TOPLAS'00 paper with O. Kupferman).
Constraint Satisfaction and Database Theory: a Tutorial
(PODS'00 tutorial).
Talk.
The Hierarchical Approach to Modeling Knowledge and Common Knowledge
(Full version of TARK92'00 paper with R. Fagin, J. Geanakopolos,
and J.Y. Halpern).
View-Based Query Processing for Regular Path Queries with Inverse
(PODS'00 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Verification by Augmented Abstraction: The Automata-Theoretic View
(Full version of CSL'99 paper with Y. Kesten and A. Pnueli).
Containment of Conjunctive Regular Path Queries with Inverse
(KR'00 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Answering Regular Path Queries Using Views
(ICDE'00 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
The Complexity of Problems on Graphs Represented as OBDDs
(with J. Feigenbaum, S. Kannan, and Mahesh Viswanathan,
published in
the Chicago J. of Theoretical Computer Science).
Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting
(SMC'99 paper with L. Fix, R. Fraer, and G. Kamhi).
Church's Problem Revisited
(BSL paper with O. Kupferman).
Rewriting of regular expressions and regular path queries
(Full version of PODS'99 paper with D. Calvanese, G. DeGiacomo, and
M. Lenzerini).
Model Checking of Safety Properties
(Full version of CAV'99 paper with O. Kupferman).
Automata-Theoretic Approach to Planning for Temporally Extended
Goals
(ECP'99 paper with G. De Giacomo).
Bisimulation and Model Checking
(CHARME'99 paper with K. Fisler).
Counting with Automata
(technical report with O. Kupferman and A. Ta-Shma).
Conjunctive-query containment and constraint satisfaction
(Full version of PODS'98 paper with P. Kolaitis).
Vacuity Detection in Temporal Model Checking
(CHARME'99 paper with O. Kupferman).
Black Box Checking
(PSTV'99 paper with D. Peled and M. Yannakakis).
Robust Satisfaction
(CONCUR'99 paper with O. Kupferman).
Model Checking of Safety Properties
(CAV'99 paper with O. Kupferman).
Improved Automata Generation for Linear Temporal Logic
(CAV'99 paper with M. Daniele and F. Giunchiglia).
LTL2AUT:
software to generate Büchi automata from LTL formulas.
Rewriting of regular expressions and regular path queries
(PODS'99 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).
Probabilistic linear-time model checking:
an overview of the automata-theoretic approach
(invited ARTS'99 paper).
The Weakness of Self-Complementation
(STACS'99 paper with O. Kupferman).
Bisimulation Minimization in an Automata-Theoretic Verification
Framework
(FMCAD'98 paper with K. Fisler).
Alternating Refinement Relations
(CONCUR'98 paper with R. Alur, T. Henzinger, and O. Kupferman).
Synthesis from Knowledge-Based Specifications
(CONCUR'98 paper with R. van der Meyden).
Sometimes and Not Never Re-revisited:
On Branching Versus Linear Time
(CONCUR'98 invited paper).
An Automata-Theoretic Approach to Branching-Time Model Checking
(full version of CAV'94 paper with coauthors O. Kupferman and
P. Wolper).
Conjunctive-query containment and constraint satisfaction
(PODS'98 paper with P. Kolaitis).
Reasoning about The Past with Two-Way Automata
(ICALP'98 paper).
Linear vs. Branching Time:
A Complexity-Theoretic Perspective
(invited LICS'98 paper).
Freedom, Weakness, and Determinism:
From Linear-time to Branching-time
(LICS'98 paper with O. Kupferman).
Computational Model Theory: an Overview
(WOLLIC'97 paper)
Complexity of Problems on Graphs Represented as OBDDs
(STACS'98 paper with J. Feigenbaum, S. Kannan, and
M. Viswanathan).
Modular Model Checking
(COMPOS'97 paper with O. Kupferman).
Verification of Fair Transition Systems
(with O. Kupferman, published in
the Chicago J. of Theoretical Computer Science).
Weak Alternating Automata and Tree Automata Emptiness
(STOC'98 paper with O. Kupferman).
Logic in The Computer Science Curriculum
(SIGCSE'98 panel with B. Kim,P. Kolaitis, and D. Leivant).
Relating Linear and Branching Model Checking
(PROCOMET'98 paper with O. Kupferman).
Module Checking
(full version of CAV'96 paper with O. Kupferman and P. Wolper).
The Computational Structure of Monotone Monadic SNP and Constraint
Satisfaction: A Study through Datalog and Group Theory
(full version of STOC'93 paper with T. Feder).
Verification of Open Systems
(FST&TCS'97 invited paper).
Synthesis with Incomplete Information
(ICTL'97 paper with O. Kupferman).
Alternating Automata: Unifying Truth and Validity Checking for Temporal
Logics
(invited paper in CADE'97).
On the Complexity of Verifying Concurrent Transition Systems
(CONCUR'97 paper with D. Harel and O. Kupferman).
Weak Alternating Automata Are Not That Weak
(ISTCS'97 paper with O. Kupferman).
Module Checking Revisited
(CAV'97 paper with O. Kupferman).
Model Checking and Transitive-Closure Logic
(CAV'97 paper with N. Immerman).
A New Heuristic for Bad Cycle Detection Using BDDs
(CAV'97 paper with R. Hardin, R. Kurshan, and S.K. Shukla).
First-Order Logic with Two Variables and Unary Temporal Logic
(LICS'97 paper with K. Etessami and T. Wilke).
Knowledge-Based Programs
(full version PODC'95 paper with coauthors R. Fagin, J.Y. Halpern,
and Y. Moses).
On the Decision Problem for Two-Variable First-Order Logic
(to appear in Bulletin of the ASL, with E. Graedel and P. Kolaitis).
Why is Modal Logic So Robustly Decidable?
(paper for DIMACS workshop).
Fixpoint Logics, Relational Machines, and Computational Complexity
(Full version of Structures'92 paper with Abiteboul and Vianu).
A Space-Efficient On-the-Fly Algorithm for Real-Time Model
Checking
(CONCUR'96 paper with O. Kupferman and T. Henzinger).
Module Checking
(CAV'96 paper with O. Kupferman).
Verification of Fair Transition Systems
(CAV'96 paper with O. Kupferman).
Relating Word and Tree Automata
(LICS'96 paper with O. Kupferman and S. Safra).
On the Expressive Power of Variable-Confined Logics
(LICS'96 paper with P. Kolaitis).
Common knowledge revisited
(TARK'96 paper with R. Fagin, J.Y. Halpern, and Y. Moses).
Implementing knowledge-based programs
(TARK'96 paper).
Rank Predicates vs. Progress Measures in Concurrent-Program
Verification
(published in
the Chicago J. of Theoretical Computer Science).
On the Equivalence of Recursive and Nonrecursive Datalog Programs
(PODS'92 paper with coauthor S. Chaudhuri, to appear in a
special issue of JCSS).
On the complexity of branching modular model checking
(CONCUR'95 paper with coauthor O. Kupferman).
Knowledge-Based Programs
(PODC'95 paper with coauthors R. Fagin, J.Y. Halpern, and Y. Moses).
Simple On-the-fly Automatic Verification of Linear Temporal Logic
(PSTV'95 paper with coauthors R. Gerth, D. Peled, and
P. Wolper).
An Automata-Theoretic Approach to Fair Realizability and Synthesis
(CAV'95 paper).
Reasoning about Knowledge
(book with co-authors R. Fagin, J.Y. Halpern, and
Y. Moses, published by
MIT Press).
Alternating automata and program verification
(LNCS Vol. 1000).
On the Complexity of Modular Model Checking
(LICS'95 paper).
On the Complexity of Bounded-Variable Queries
(PODS'95 paper).
An automata-theoretic approach to linear temporal logic
(Banff'94).
An operational semantics for knowledge bases
(AAAI'94 paper with coauthors R. Fagin, J.Y. Halpern
and Y. Moses).
An Automata-Theoretic Approach to Branching-Time Model Checking
(CAV'94 paper with coauthors O. Bernholtz and P. Wolper).
On the complexity of equivalence between recursive and nonrecursive
Datalog programs
(PODS'92 paper with S. Chaudhuri).
Nontraditional applications of automata theory
(invited TACS'94 paper).
Algorithmic knowledge
(TARK'94 paper with J.Y. Halpern and Y. Moses).
Parametric Real-Time Reasoning
(STOC'93 paper with T. Henzinger and R. Alur).
Reasoning about infinite computations
(Full version of FOCS'83 paper with P. Wolper).
Model Checking vs. Theorem Proving: A Manifesto
(Full version of KR'91 paper with J.Y. Halpern).
What is an inference rule?
(Full version of JCIT'90 paper with R. Fagin and J.Y. Halpern).
Infinitary Logics and 0-1 Laws
(Full version of LICS'90 paper with P. Kolaitis).
Memory-Efficient Algorithms for the Verification
of Temporal Properties
(CAV'90 paper with C. Courcoubetis, P. Wolper,
and M. Yannakakis).
On the Expressive Power of Datalog: Tools and a Case Study
(PODS'90 paper with P.G. Kolaitis).
On The Complexity of Epistemic Reasnoning
(LICS'89 paper).
On omega-Automata and Temporal Logic
(STOC'89 paper with S. Safra).
A Note on the Reduction of Two-Way Automata to One-Way Automata
(IPL'88 paper).
A Temporal Fixpoint Calculus
(POPL'88 paper).
The Universal--Relation Data Model for Logical Independence
(IEEE Software 1988 paper).
Verification of Concurrent Programs: The Automata-Theoretic
Framework
(Full version of LICS'87 paper).
Fundamentals of dependency theory
(TTCS'87 paper).
An Automata-Theoretic Approach to Automatic Program Verification
(LICS'86 paper with P. Wolper).
Knowledge and implicit knowledge in a distributed environment
(TARK'86 paper with R. Fagin).
The Complexity of Reasoning about Knowledge and Time -- Synchronous
Systems
(IBM Research Report, STOC'86 paper with J. Halpern).
The complexity of reasoning about knowledge and time, I -- lower
bounds
(STOC'86 paper with J. Halpern).
Reasoning about fair concurrent programs
(STOC'86 paper with C. Courcoubetis and P. Wolper).
Notions of dependency satisfaction
(JACM'86 paper with M. Graham and A. Mendelzon).
The theory of data dependencies -- a survey
(MIP'86 paper with R. Fagin).
Updating logical databases
(ACR'86 paper with R. Fagin, G. Kuper, and J.D. Ullman).
Automatic verification of probabilistic concurrent finite-state
programs
(FOCS'85 paper).
The Complementation Problem for Büchi Automata with Applications
to Temporal Logic
(full version of ICALP'85 paper with P. Sistla and P. Wolper).
The implication problem for funcational and inclusion
dependencies is undecidable
(SICOMP'85 paper with A. Chandra).
Improved upper and lower bounds for modal logics of programs
(STOC'85 paper with L. Stockmeyer), with
lower bound in full.
Automata-theoretic techniques for modal logics of programs
(Full version of STOC'84 paper with P. Wolper).
A proof procuedre for data dependencies
(JACM'84 paper with C. Beeri), and an earlier
draft (with a section relating chase to resolution).
Formal systems for tuple and equality generating dependencies
(SICOMP'84 paper with C. Beeri).
A note on lossless database decompositions
(IPL'84 paper).
On the semantics of updates in databases
(PODS'83 paper with R. Fagin and J.D. Ullman).
Yet another process logic
(LOP'83 paper with P. Wolper).
The implication and finite implication problems for typed
template dependencies
(full version of PODS'82 paper).
The complexity of relational query languages
(STOC'82 paper).
Global decision problems for relational databases
(FOCS'81 paper).
The implication problem for data dependencies
(ICALP'81 paper with C. Beeri)
and
long version.
Global decision problems for relational databases
(FOCS'81 paper).
On the complexity of testing implications of data
dependencies
(1980 Technical report with C. Beeri)