Moshe Y. Vardi - Publications and Presentations (Not Current)

The articles posted here consist of preliminary versions of articles that are about to be published or have been published in journals or conference proceedings. For final versions, please see cited journals or proceedings. If you'd like to be notified when new articles are posted here, click here.

SEBD'21 Panel on Past and Future of Computer Science Theory, with R. Fagin, G. Gottlob, C. Papadimitriou, G. Ausiello, M. Lenzerini, L. Palopoli, D. Sacca and F. Scarcello
The Long Game of Tenure (w. Todd Treangen)
Introduction to Logic (w. I. Barland, M. Felleisen, J. Greiner, and P. Kolaitis
Abstracted Power and Responsibility in Computer Science Ethics Education
From Linear Temporal Logics to Buechi Automata: The Early and Simple Principle (book chapter w. Y.K. Tsay)
Automata-Theoretic Verification (HB chapter w. J. Esparza and O. Kupferman)
On The Unreasonable Effectiveness of SAT Solvers (HB chapter w. V. Ganesh)
Deep Tech Ethics (SIGCSE'21 paper with R. Ferreira)
The Siren Song of Temporal Synthesis (invited talk at VMCAI'20 Winter School)
Logic, Automata, Games, and Algorithms (invited talk at VMCAI'20 Winter School)
Ranking of Institutions by Number of Papers published in the ACM Digital Library in 2013
Constrained Sampling and Counting (invited talk at CAV'16)
A Theory of Regular Queries (invited talk at PODS'16)
The Automated-Reasoning Revolution: from Theory to Practice and Back (Distinguished Lecture at NSF CISE, spring 2016)
Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls (IJCAI'16 paper with S. Chakraborty and K. Meel.
A Theory of Regular Queries (invited paper at PODS'16), with slides
Constrained Sampling and Counting: Universal Hashing Meets SAT Solving (paper at Beyond NP'16, with K.S Meel, S. Chakraborty,D.J. Fremont, S.A. Seshia, D. Fried, A. Ivrii, and S. Malik).
Theory in Practice for System Design and Verification (SIGLOG Survey article with R. Alur and T. Henzinger).
The SAT Revolution: Solving, Sampling, And Counting (slides of Special Talk at Highlights'15).
From Theory and Practice in Computing to Research Ethics (chapter in "The Human Face of Computing" by C.S. Calude).
SAT-Based Explicit LTL Reasoning (full version of HVC'15 paper with J. Li,, S. Zhu, and G. Pu).
Controller Synthesis for Mode-Target Games. (ADHS'15 paper with A. Balkan and P. Tabuada).
A Revisionist History of Algorithmic Game Theory (invited talk at SR'15).
On Computing Minimal Independent Support and Its Applications to Sampling and Counting (CP'15 paper with A. Ivrii, S. Malik, and K.S. Meel).
Synthesis for LTL and LDL on Finite Traces (IJCAI'15 paper with G. De Giacomo).
From Weighted to Unweighted Model Counting (IJCAI'15 paper with S. Chakraborty, D. Fried, and K.S. Meel).
Towards Manipulation Planning with Temporal Logic Specifications (ICRA'15 paper with K. He, M. Lahijanian, and L E. Kavraki).
On Parallel Scalable Uniform SAT Witness Generation (TACAS'15 paper with S. Chakraborty, D.J. Fremont, K.S. Meel, and S.A. Seshia).
Drug Target Optimization in Chronic Myeloid Leukemia Using Innovative Computational Platform (paper in Nature - Scientific Reports).
Artificial Intelligence and Technological Unemployment (AAAI'15 Tutorial Slides).
Regular Queries on Graph Databases (ICDT'15 paper with J. Reutter and M. Romero).
This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction (AAAI'15 paper with M. Lahijanian, S. Almagor, D. Fried, and L.E. Kavraki).
Synthesis with Rational Environments (EUMAS'14 paper with O. Kupferman and G. Perelli).
LTLf Satisfiability Checking (ECAI'14 paper with J. Li, L. Zhang, G. Pu, and J. He).
From Visual to Logical Formalisms for SoC Validation (MEMOCODE'14 paper with several Intel co-authors).
Assertion-Based Flow Monitoring of SystemC Models (MEMOCODE'14 paper with S. Dutta).
Distribution-Aware Sampling and Weighted Model Counting for SAT (AAAI'14 paper with S. Chakraborty, D. Fremont, K. Meel, and S. Seshia).
Balancing Scalability and Uniformity in SAT Witness Generator (DAC'14 paper with S. Chakraborty and K. Meel).
Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions (DAC'14 paper with Y. Abarbanel and E. Singerman).
The Complexity of Partial-observation Stochastic Parity Games With Finite-memory Strategies (full version of FOSSACS'14 paper with K. Chatterjee, L. Doyen, and S. Nain).
CHIMP: a Tool for Assertion-Based Dynamic Verification of SystemC Models (DIFTS'13 paper with with D. Tabakov and S. Dutta).
LTL Satisfiability Checking Revisited (TIME'13 paper with with J. Li, L. Zhang, G. Pu, and J. He).
Linear Temporal Logic and Linear Dynamic Logic on Finite Traces (IJCAI'13 paper with with G. De Giacomo).
A Scalable Apprximate Model Counter (CP'13 paper with S. Chakraborty and K. Meel).
Profile Trees for Buchi Word Automata, with Application to Determinization (GANDALF'13 paper with S. Fogarty, O. Kupferman, and T. Wilke).
A Scalable and Nearly Uniform Generator of SAT Witnesses (CAV'13 paper with S. Chakraborty and K. Meel).
Regular Real Analysis (LICS'13 paper with S. Chaudhuri and S. Sankaranarayanan).
Solving Partial-Information Stochastic Parity Games (LICS'13 paper with S. Nain).
Semantic Acyclicity on Graph Databases (PODS'13 paper with P. Barcelo and M. Romero).
Query Processing under GLAV Mappings for Relational and Graph Databases (PVLDB'13 paper with C. Calvanese, G. De Giacomo, and M. Lenzerini).
Relentful Strategic Reasoning in Alternating-Time Temporal Logic (full version of LPAR'10 paper with F. Mogavero and A. Murano).
Modeling, Analysis, and Verification - The Formal Methods Manifesto (Dagstuhl Manifesto with J. Kreiker, A. Tarlecki, and R.Wilhelm).
Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking (full version of HVC'12 paper with K. Rozier).
What makes ATL* decidable? A decidable fragment of Strategy Logic (CONCUR'12 paper with F. Mogavero, A. Murano, and G. Perelli).
BMA: Visual Tool for Modeling and Analyzing Biological Networks (CAV'12 paper with D. Benque, S. Bourton, C. Cockerton, B. Cook, J. Fisher, S. Ishtiaq, N. Piterman, and A. Taylor).
Once and For All (JCSS'12 paper with O. Kupferman and A. Pnueli).
Synthesizing Probabilistic Composers (full version of FOSSACS'12 submission with S. Nain).
Automatic Aspectization of SystemC (full version of MISS'12 submission with D. Tabakov).
Dynamic Reactive Modules (revised CONCUR'11 paper with J. Fisher, T.A. Henzinger, D. Nickovic, N. Piterman, and A.V. Singh).
Automata-Theoretic Verification (Handbook chapter with J. Esparza and O. Kupferman).
Synthesis from Probabilistic Components (Full version of CSL'11 paper with Y. Lustig and S. Nain).
Unifying Buechi Complementation Constructions (Full version of CSL'11 paper with S. Fogarty, O. Kupferman, and T. Wilke).
Synthesis from Recursive-Components Libraries (Full version of GANDALF'11 paper with Y. Lustig).
The Rise and Fall of Linear Temporal Logic (Invited talk at GANDALF'11).
A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking (FM'11 paper with K. Rozier).
The Only Way Is Up: On A Tower of Abstractions for Biology (FM'11 paper with J. Fisher and N. Piterman).
The Complexity of Integer Bound Propagation (full version of CP'07 paper with L. Bordeaux, G. Katsirelos, and N. Narodytska).
Simplifying Schema Mappings (ICDT'11 paper with D. Calvanese, G. De Giacomo, and M. Lenzerini).
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).
From Complementation to Certification (TACAS'04 talk 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).
Projection Pushing Revisited (EDBT04'04 talk 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, and sample industrial properties.
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).
Model Checking of Safety Properties (CAV'99 talk 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) and talk
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).
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), and full version
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).
Computational Model Theory: An Overview (Full version of WOLLIC'97 paper).
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).
Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory (Full version of LICS'92 paper with P. Kolaitis).
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).
Edmarkers can make a difference (IPL'89 paper).
A Note on the Reduction of Two-Way Automata to One-Way Automata (IPL'88 paper).
Decidable optimization problems for database logic programs (STOC'88 paper S. Cosmadakis, H. Gaifman, and P. Kanellakis).
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).
The Decision Problem for the Probabilities of Higher-Order Properties (STOC'87 paper with P. Kolaitis).
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).
On epistemic logic and logical omniscience (TARK'86 paper).
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.
An internal semantics for modal logic (STOC'85 paper with R. Fagin).
A simple proof that connectivity of finite graphs is not first-order definable. (EATCS Bulletin 26, 1985 paper with H. Gaifman).
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).
The implication problem for data dependencies (ICALP'81 paper with C. Beeri) and long version.
Global decision problems for relational databases (FOCS'81 paper).
The decision problem for database dependencies (IPL'81 paper).
On the complexity of testing implications of data dependencies (1980 Technical Report with C. Beeri)
Expeceed properties of set partitions (1980 Technical Report)