Moshe Y. Vardi

According to our database1, Moshe Y. Vardi
  • authored at least 570 papers between 1979 and 2017.
  • has a "Dijkstra number"2 of three.

Awards

ACM Fellow

ACM Fellow 2000, "For contributions to the development of logic as a unifying foundational framework and a tool for modeling computational systems.".

IEEE Fellow

IEEE Fellow 2009, "For contributions to the development of logic as a unifying framework for modeling computational systems".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2017
Regular Queries on Graph Databases.
Theory Comput. Syst., 2017

Preface to the Special Issue on SR 2014.
Inf. Comput., 2017

Alonzo Church Award 2017 - Call for Nominations.
Bulletin of the EATCS, 2017

Supervisory control and reactive synthesis: a comparative introduction.
Discrete Event Dynamic Systems, 2017

Symbolic LTLf Synthesis.
CoRR, 2017

Reasoning about Strategies: on the Satisfiability Problem.
Logical Methods in Computer Science, 2017

Combining the k-CNF and XOR Phase-Transitions.
CoRR, 2017

Divination by program committee.
Commun. ACM, 2017

Ten years at the helm of communications of the ACM.
Commun. ACM, 2017

Cyber insecurity and cyber libertarianism.
Commun. ACM, 2017

ACM's open-conference principle and political reality.
Commun. ACM, 2017

Technology for the most effective use of mankind.
Commun. ACM, 2017

2017 ACM PODS Alberto O. Mendelzon Test-of-Time Award.
Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2017

Strategy logic with imperfect information.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

The homomorphism problem for regular graph patterns.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Symbolic LTLf Synthesis.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Random Models for Evaluating Efficient Büchi Universality Checking.
Proceedings of the Logic and Its Applications - 7th Indian Conference, 2017

Counting-Based Reliability Estimation for Power-Transmission Grids.
Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017

2016
Iterative Temporal Planning in Uncertain Environments With Partial Satisfaction Guarantees.
IEEE Trans. Robotics, 2016

Semantic Acyclicity on Graph Databases.
SIAM J. Comput., 2016

Relentful strategic reasoning in alternating-time temporal logic.
J. Log. Comput., 2016

2014 CAV award announcement.
Formal Methods in System Design, 2016

Alonzo Church Award 2016 - Call for Nominations.
Bulletin of the EATCS, 2016

Viewpoints on "Logic activities in Europe", twenty years later.
Bulletin of the EATCS, 2016

Approximate Reachability.
CoRR, 2016

On computing minimal independent support and its applications to sampling and counting.
Constraints, 2016

Globalization, computing, and their political impact.
Commun. ACM, 2016

Academic rankings considered harmful!
Commun. ACM, 2016

The ritual of academic-unit review.
Commun. ACM, 2016

The moral imperative of artificial intelligence.
Commun. ACM, 2016

Are we headed toward another global tech bust?
Commun. ACM, 2016

The moral hazard of complexity-theoretic assumptions.
Commun. ACM, 2016

Synthesis with rational environments.
Ann. Math. Artif. Intell., 2016

Solving Parity Games Using an Automata-Based Algorithm.
Proceedings of the Implementation and Application of Automata, 2016

A Theory of Regular Queries.
Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2016

Regular Open APIs.
Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, 2016

LTLf and LDLf Synthesis under Partial Observability.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Combining the k-CNF and XOR Phase-Transitions.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

BDD-Based Boolean Functional Synthesis.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving.
Proceedings of the Beyond NP, 2016

Approximate Probabilistic Inference via Word-Level Counting.
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016

2015
Theory in practice for system design and verification.
SIGLOG News, 2015

Special issue on SR 2013.
Inf. Comput., 2015

Profile trees for Büchi word automata, with application to determinization.
Inf. Comput., 2015

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving.
CoRR, 2015

SAT-based Explicit LTL Reasoning.
CoRR, 2015

The Complexity of Synthesis from Probabilistic Components.
CoRR, 2015

Approximate Probabilistic Inference via Word-Level Counting.
CoRR, 2015

Node Selection Query Languages for Trees.
CoRR, 2015

Controller Synthesis for Mode-Target Games.
CoRR, 2015

What do we do when the jobs are gone, and why we must embrace active learning.
Commun. ACM, 2015

On lethal autonomous weapons.
Commun. ACM, 2015

What can be done about gender diversity in computing?: a lot!
Commun. ACM, 2015

Why doesn't ACM have a SIG for theoretical computer science?
Commun. ACM, 2015

Incentivizing quality and impact in computing research.
Commun. ACM, 2015

Is information technology destroying the middle class?
Commun. ACM, 2015

The rise and fall of industrial research labs.
Commun. ACM, 2015

On Parallel Scalable Uniform SAT Witness Generation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Synthesis for LTL and LDL on Finite Traces.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

From Weighted to Unweighted Model Counting.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

Towards manipulation planning with temporal logic specifications.
Proceedings of the IEEE International Conference on Robotics and Automation, 2015

Regular Queries on Graph Databases.
Proceedings of the 18th International Conference on Database Theory, 2015

The Complexity of Synthesis from Probabilistic Components.
Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

SAT-Based Explicit LTL Reasoning.
Proceedings of the Hardware and Software: Verification and Testing, 2015

Humans, machines, and the future of work.
Proceedings of the Ada Lovelace Symposium 2015, 2015

This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction.
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014
Reasoning About Strategies: On the Model-Checking Problem.
ACM Trans. Comput. Log., 2014

Design and Synthesis from Components (Dagstuhl Seminar 14232).
Dagstuhl Reports, 2014

State of Büchi Complementation.
Logical Methods in Computer Science, 2014

Synthesis from Probabilistic Components.
Logical Methods in Computer Science, 2014

Fast LTL Satisfiability Checking by SAT Solvers.
CoRR, 2014

LTLf satisfiability checking.
CoRR, 2014

The Complexity of Partial-observation Stochastic Parity Games With Finite-memory Strategies.
CoRR, 2014

Balancing Scalability and Uniformity in SAT Witness Generator.
CoRR, 2014

Distribution-Aware Sampling and Weighted Model Counting for SAT.
CoRR, 2014

The Complexity of Integer Bound Propagation.
CoRR, 2014

Would Turing have passed the Turing Test?
Commun. ACM, 2014

Openism, IPism, fundamentalism, and pragmatism.
Commun. ACM, 2014

Moore's law and the sand-heap paradox.
Commun. ACM, 2014

Boolean satisfiability: theory and engineering.
Commun. ACM, 2014

Scalable conferences.
Commun. ACM, 2014

Bridging the Gap between Supervisory Control and Reactive Synthesis: Case of Full Observation and Centralized Control.
Proceedings of the 12th International Workshop on Discrete Event Systems, 2014

Does query evaluation tractability help query containment?
Proceedings of the 33rd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2014

From visual to logical formalisms for SoC validation.
Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Assertion-based flow monitoring of SystemC models.
Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

A sampling-based strategy planner for nondeterministic hybrid systems.
Proceedings of the 2014 IEEE International Conference on Robotics and Automation, 2014

The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Synthesis with Rational Environments.
Proceedings of the Multi-Agent Systems - 12th European Conference, 2014

LTLf Satisfiability Checking.
Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

Balancing Scalability and Uniformity in SAT Witness Generator.
Proceedings of the 51st Annual Design Automation Conference 2014, 2014

Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions.
Proceedings of the 51st Annual Design Automation Conference 2014, 2014

From Löwenheim to PSL and SVA.
Proceedings of the Language, Culture, Computation. Computing - Theory and Technology, 2014

Distribution-Aware Sampling and Weighted Model Counting for SAT.
Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013
Falsification of LTL safety properties in hybrid systems.
STTT, 2013

Synthesis from component libraries.
STTT, 2013

On simplification of schema mappings.
J. Comput. Syst. Sci., 2013

Pushdown module checking with imperfect information.
Inf. Comput., 2013

A Scalable and Nearly Uniform Generator of SAT Witnesses
CoRR, 2013

Unifying Büchi Complementation Constructions
Logical Methods in Computer Science, 2013

Synthesis from Knowledge-Based Specifications.
CoRR, 2013

Polsat: A Portfolio LTL Satisfiability Solver.
CoRR, 2013

Profile Trees for Büchi Word Automata, with Application to Determinization.
Proceedings of the Proceedings Fourth International Symposium on Games, 2013

A Scalable Approximate Model Counter.
CoRR, 2013

What is a flagship publication?
Commun. ACM, 2013

The end of the American network.
Commun. ACM, 2013

Has the innovation cup run dry?
Commun. ACM, 2013

The great robotics debate.
Commun. ACM, 2013

Fricative computing.
Commun. ACM, 2013

To boycott or not to boycott.
Commun. ACM, 2013

Who begat computing?
Commun. ACM, 2013

LTL Satisfiability Checking Revisited.
Proceedings of the 2013 20th International Symposium on Temporal Representation and Reasoning, 2013

A logical revolution (keynote).
Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

A publication culture in software engineering (panel).
Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Semantic acyclicity on graph databases.
Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2013

Solving Partial-Information Stochastic Parity Games.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Regular Real Analysis.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Linear Temporal Logic and Linear Dynamic Logic on Finite Traces.
Proceedings of the IJCAI 2013, 2013

Iterative temporal motion planning for hybrid systems in partially unknown environments.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models.
Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, 2013

A Scalable Approximate Model Counter.
Proceedings of the Principles and Practice of Constraint Programming, 2013

A Scalable and Nearly Uniform Generator of SAT Witnesses.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012
Query Processing under GLAV Mappings for Relational and Graph Databases.
PVLDB, 2012

Once and for all.
J. Comput. Syst. Sci., 2012

2011 CAV award announcement.
Formal Methods in System Design, 2012

Optimized temporal monitors for SystemC.
Formal Methods in System Design, 2012

2010 CAV award announcement.
Formal Methods in System Design, 2012

Temporal property verification as a program analysis task - Extended Version.
Formal Methods in System Design, 2012

Publication Culture in Computing Research (Dagstuhl Perspectives Workshop 12452).
Dagstuhl Reports, 2012

A Decidable Fragment of Strategy Logic
CoRR, 2012

Büchi Complementation and Size-Change Termination
Logical Methods in Computer Science, 2012

Will MOOCs destroy academia?
Commun. ACM, 2012

Why ACM?
Commun. ACM, 2012

Predatory scholarly publishing.
Commun. ACM, 2012

Fair access.
Commun. ACM, 2012

What is an algorithm?
Commun. ACM, 2012

Artificial intelligence: past and future.
Commun. ACM, 2012

Compositional Temporal Synthesis.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking.
Proceedings of the Hardware and Software: Verification and Testing, 2012

Synthesizing Probabilistic Composers.
Proceedings of the Foundations of Software Science and Computational Structures, 2012

What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic.
Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

Bma: Visual Tool for Modeling and Analyzing Biological Networks.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking.
STTT, 2011

The Complexity of Integer Bound Propagation.
J. Artif. Intell. Res., 2011

Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482).
Dagstuhl Manifestos, 2011

Reasoning About Strategies: On the Model-Checking Problem
CoRR, 2011

The Planning Spectrum - One, Two, Three, Infinity
CoRR, 2011

Synthesis from Recursive-Components Libraries
Proceedings of Second International Symposium on Games, 2011

Computing for humans.
Commun. ACM, 2011

Is Moore's Party over?
Commun. ACM, 2011

Are you talking to me?
Commun. ACM, 2011

Solving the unsolvable.
Commun. ACM, 2011

Technology has social consequences.
Commun. ACM, 2011

Fumbling the future.
Commun. ACM, 2011

Where have all the workshops gone?
Commun. ACM, 2011

Temporal Synthesis for Bounded Systems and Environments.
Proceedings of the 28th International Symposium on Theoretical Aspects of Computer Science, 2011

Simplifying schema mappings.
Proceedings of the Database Theory, 2011

Constraints, Graphs, Algebra, Logic, and Complexity (Invited Talk).
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2011

A Multi-encoding Approach for LTL Symbolic Satisfiability Checking.
Proceedings of the FM 2011: Formal Methods, 2011

The Only Way Is Up.
Proceedings of the FM 2011: Formal Methods, 2011

Branching vs. Linear Time: Semantical Perspective.
Proceedings of the Computer Science Logic, 2011

Synthesis from Probabilistic Components.
Proceedings of the Computer Science Logic, 2011

Unifying Büchi Complementation Constructions.
Proceedings of the Computer Science Logic, 2011

Dynamic Reactive Modules.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Temporal Property Verification as a Program Analysis Task.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Motion Planning With Dynamics by a Synergistic Combination of Layers of Planning.
IEEE Trans. Robotics, 2010

LTL satisfiability checking.
STTT, 2010

2009 CAV award announcement.
Formal Methods in System Design, 2010

View Synthesis from Schema Mappings
CoRR, 2010

On P, NP, and computational complexity.
Commun. ACM, 2010

Science has only two legs.
Commun. ACM, 2010

Hypercriticality.
Commun. ACM, 2010

Globalization and Offshoring of Software revisited.
Commun. ACM, 2010

Revisiting the publication culture in computing research.
Commun. ACM, 2010

More debate, please!
Commun. ACM, 2010

State of Büchi Complementation.
Proceedings of the Implementation and Application of Automata, 2010

Efficient Büchi Universality Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Optimized temporal monitors for SystemC.
Proceedings of the Runtime Verification - First International Conference, 2010

Monitoring temporal SystemC properties.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Relentful Strategic Reasoning in Alternating-Time Temporal Logic.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Synthesis of Trigger Properties.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Sampling-based motion planning with temporal goals.
Proceedings of the IEEE International Conference on Robotics and Automation, 2010

Reasoning About Strategies.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010

Constraints, Graphs, Algebra, Logic, and Complexity.
Proceedings of the Principles and Practice of Constraint Programming - CP 2010, 2010

Motion planning with hybrid dynamics and temporal goals.
Proceedings of the 49th IEEE Conference on Decision and Control, 2010

An Automata-Theoretic Approach to Infinite-State Systems.
Proceedings of the Time for Verification, 2010

From Automated Verification to Automated Design.
Proceedings of the 20th International Conference on Automated Planning and Scheduling, 2010

Node Selection Query Languages for Trees.
Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, 2010

2009
Intelligate: An Algorithm for Learning Boolean Functions for Dynamic Power Reduction.
J. Low Power Electronics, 2009

Hybrid systems: from verification to falsification by combining motion planning and discrete search.
Formal Methods in System Design, 2009

From liveness to promptness.
Formal Methods in System Design, 2009

The 2008 CAV Award citation.
Formal Methods in System Design, 2009

Is the image crisis over?
Commun. ACM, 2009

The financial meltdown and computing.
Commun. ACM, 2009

Open, closed, or clopen access?
Commun. ACM, 2009

Conferences vs. journals in computing research.
Commun. ACM, 2009

"Yes, it can be done".
Commun. ACM, 2009

How are we doing?
Commun. ACM, 2009

Constraints, Graphs, Algebra, Logic, and Complexity.
Proceedings of the Theory and Applications of Models of Computation, 6th Annual Conference, 2009

Falsification of LTL Safety Properties in Hybrid Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Büchi Complementation and Size-Change Termination.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Symbolic Techniques in Propositional Satisfiability Solving.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Model Checking as A Reachability Problem.
Proceedings of the Reachability Problems, 3rd International Workshop, 2009

Trace Semantics is Fully Abstract.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

From Philosophical to Industrial Logics.
Proceedings of the Logic and Its Applications, Third Indian Conference, 2009

Synthesis from Component Libraries.
Proceedings of the Foundations of Software Science and Computational Structures, 2009

An Automata-Theoretic Approach to Regular XPath.
Proceedings of the Database Programming Languages, 2009

2008
Multi-Objective Model Checking of Markov Decision Processes.
Logical Methods in Computer Science, 2008

The Complexity of Enriched Mu-Calculi.
Logical Methods in Computer Science, 2008

Multi-Objective Model Checking of Markov Decision Processes
CoRR, 2008

The Complexity of Enriched Mu-Calculi
CoRR, 2008

Let us---together---make CACM exciting.
Commun. ACM, 2008

"Where do you come from? and where are you going?".
Commun. ACM, 2008

CACM: past, present, and future.
Commun. ACM, 2008

From Verification to Synthesis.
Proceedings of the Verified Software: Theories, 2008

From Church and Prior to PSL.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Intelligate: Scalable Dynamic Invariant Learning for Power Reduction.
Proceedings of the Integrated Circuit and System Design. Power and Timing Modeling, 2008

Impact of workspace decompositions on discrete search leading continuous exploration (DSLX) motion planning.
Proceedings of the 2008 IEEE International Conference on Robotics and Automation, 2008

Open Implication.
Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

Automata-Theoretic Model Checking Revisited.
Proceedings of the Hardware and Software: Verification and Testing, 2008

A Framework for Inherent Vacuity.
Proceedings of the Hardware and Software: Verification and Testing, 2008

A Temporal Language for SystemC.
Proceedings of the Formal Methods in Computer-Aided Design, 2008

A Logical Approach to Constraint Satisfaction.
Proceedings of the Complexity of Constraints, 2008

Automata: from logics to algorithms.
Proceedings of the Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., 2008

From Monadic Logic to PSL.
Proceedings of the Pillars of Computer Science, 2008

2007
Finite Model Theory and Its Applications
Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-68804-4, 2007

View-based query processing: On the relationship between rewriting, answering and losslessness.
Theor. Comput. Sci., 2007

A continuous-discontinuous second-order transition in the satisfiability of random Horn-SAT formulas.
Random Struct. Algorithms, 2007

The Planning Spectrum - One, Two, Three, Infinity.
J. Artif. Intell. Res., 2007

GSTE is partitioned model checking.
Formal Methods in System Design, 2007

Linear-Time Model Checking: Automata Theory in Practice.
Proceedings of the Implementation and Application of Automata, 2007

Automata-Theoretic Model Checking Revisited.
Proceedings of the Verification, 2007

Property-Driven Partitioning for Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Multi-objective Model Checking of Markov Decision Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

The Büchi Complementation Saga.
Proceedings of the STACS 2007, 2007

LTL Satisfiability Checking.
Proceedings of the Model Checking Software, 2007

Discrete Search Leading Continuous Exploration for Kinodynamic Motion Planning.
Proceedings of the Robotics: Science and Systems III, 2007

Proving that programs eventually do something good.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Model Checking Buechi Specifications.
Proceedings of the LATA 2007. Proceedings of the 1st International Conference on Language and Automata Theory and Applications., 2007

A Motion Planner for a Hybrid Robotic System with Kinodynamic Constraints.
Proceedings of the 2007 IEEE International Conference on Robotics and Automation, 2007

Interactive presentation: PowerQuest: trace driven data mining for power optimization.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

07441 Abstracts Collection -- Algorithmic-Logical Theory of Infinite Structures.
Proceedings of the Algorithmic-Logical Theory of Infinite Structures, 28.10. - 02.11.2007, 2007

07441 Summary -- Algorithmic-Logical Theory of Infinite Structures.
Proceedings of the Algorithmic-Logical Theory of Infinite Structures, 28.10. - 02.11.2007, 2007

Formal Techniques for SystemC Verification; Position Paper.
Proceedings of the 44th Design Automation Conference, 2007

An Analysis of Slow Convergence in Interval Propagation.
Proceedings of the Principles and Practice of Constraint Programming, 2007

Pushdown Module Checking with Imperfect Information.
Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

Hybrid Systems: From Verification to Falsification.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

From Liveness to Promptness.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Branching vs. Linear Time: Semantical Perspective.
Proceedings of the Automated Technology for Verification and Analysis, 2007

Deeper Bound in BMC by Combining Constant Propagation and Abstraction.
Proceedings of the 12th Conference on Asia South Pacific Design Automation, 2007

2006
Coverage metrics for formal verification.
STTT, 2006

BDD-based decision procedures for the modal logic K.
Journal of Applied Non-Classical Logics, 2006

Büchi Complementation Made Tighter.
Int. J. Found. Comput. Sci., 2006

Aggregating disparate estimates of chance.
Games and Economic Behavior, 2006

Coverage metrics for temporal logic model checking*.
Formal Methods in System Design, 2006

Relating word and tree automata.
Ann. Pure Appl. Logic, 2006

educational response to offshore outsourcing.
Proceedings of the 39th SIGCSE Technical Symposium on Computer Science Education, 2006

Automata theory: its relevance to computer science students and course contents.
Proceedings of the 39th SIGCSE Technical Symposium on Computer Science Education, 2006

On Locally Checkable Properties.
Proceedings of the Logic for Programming, 2006

Fixed-Parameter Hierarchies inside PSPACE.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Memoryful Branching-Time Logic.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

The Complexity of Enriched µ-Calculi.
Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Deterministic Dynamic Monitors for Linear-Time Assertions.
Proceedings of the Formal Approaches to Software Testing and Runtime Verification, 2006

Safraless Compositional Synthesis.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
From linear time to branching time.
ACM Trans. Comput. Log., 2005

From complementation to certification.
Theor. Comput. Sci., 2005

Decidable containment of recursive queries.
Theor. Comput. Sci., 2005

In memory of Seymour Ginsburg 1928 - 2004.
SIGMOD Record, 2005

Symbolic Techniques in Satisfiability Solving.
J. Autom. Reasoning, 2005

SAT-based Induction for Temporal Safety Properties.
Electr. Notes Theor. Comput. Sci., 2005

Complementation Constructions for Nondeterministic Automata on Infinite Words.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Experimental Evaluation of Classical Automata Constructions.
Proceedings of the Logic for Programming, 2005

Treewidth in Verification: Local vs. Global.
Proceedings of the Logic for Programming, 2005

Model Checking for Database Theoreticians.
Proceedings of the Database Theory, 2005

View-Based Query Processing: On the Relationship Between Rewriting, Answering and Losslessness.
Proceedings of the Database Theory, 2005

Efficient LTL compilation for SAT-based model checking.
Proceedings of the 2005 International Conference on Computer-Aided Design, 2005

Safraless Decision Procedures.
Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 2005

05241 Abstracts Collection - Synthesis and Planning.
Proceedings of the Synthesis and Planning, 12.-17. June 2005, 2005

05241 Executive Summary - Synthesis and Planning.
Proceedings of the Synthesis and Planning, 12.-17. June 2005, 2005

Regular Vacuity.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Formal Verification of Backward Compatibility of Microcode.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

A Continuous-Discontinuous Second-Order Transition in the Satisfiability of Random Horn-SAT Formulas.
Proceedings of the Approximation, 2005

2004
Complete Axiomatizations for Reasoning about Knowledge and Time.
SIAM J. Comput., 2004

From Complementation to Certification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

A Measured Collapse of the Modal µ-Calculus Alternation Hierarchy.
Proceedings of the STACS 2004, 2004

Search vs. Symbolic Techniques in Satisfiability Solving.
Proceedings of the Theory and Applications of Satisfiability Testing, 2004

Search vs. Symbolic Techniques in Satisfiability Solving.
Proceedings of the SAT 2004, 2004

Pattern search in hierarchical high-level designs.
Proceedings of the 2004 11th IEEE International Conference on Electronics, 2004

Projection Pushing Revisited.
Proceedings of the Advances in Database Technology, 2004

Symbolic Decision Procedures for QBF.
Proceedings of the Principles and Practice of Constraint Programming, 2004

Constraint Propagation as a Proof System.
Proceedings of the Principles and Practice of Constraint Programming, 2004

GSTE Is Partitioned Model Checking.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Global Model-Checking of Infinite-State Systems.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Verifying omega-Regular Properties of Markov Chains.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Büchi Complementation Made Tighter.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003
From bidirectionality to alternation.
Theor. Comput. Sci., 2003

Vacuity detection in temporal model checking.
STTT, 2003

Reasoning on regular path queries.
SIGMOD Record, 2003

Random 3-SAT: The Plot Thickens.
Constraints, 2003

Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Resets vs. Aborts in Linear Temporal Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Query Containment Using Views.
Proceedings of the Eleventh Italian Symposium on Advanced Database Systems, 2003

View-based query containment.
Proceedings of the Twenty-Second ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 2003

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

The Planning Spectrum - One, Two, Three, Infinity.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Homomorphism Closed vs. Existential Positive.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Automated Verification: Graphs, Logic, and Automata.
Proceedings of the IJCAI-03, 2003

Decidable Containment of Recursive Queries.
Proceedings of the Database Theory, 2003

Logic and Automata: A Match Made in Heaven.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Π2 ∩ Σ2 ≡ AFMC.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

On Complementing Nondeterministic Büchi Automata.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

Coverage Metrics for Formal Verification.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

Enhanced Vacuity Detection in Linear Temporal Logic.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Optimizing a BDD-Based Modal Solver.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

A Call to Regularity.
Proceedings of the PCK50, 2003

Fair Equivalence Relations.
Proceedings of the Verification: Theory and Practice, 2003

In Memoriam: Paris C. Kanellakis.
Proceedings of the PCK50, 2003

2002
Rewriting of Regular Expressions and Regular Path Queries.
J. Comput. Syst. Sci., 2002

Black Box Checking.
Journal of Automata, Languages and Combinatorics, 2002

On the Complexity of Verifying Concurrent Transition Systems.
Inf. Comput., 2002

First-Order Logic with Two Variables and Unary Temporal Logic.
Inf. Comput., 2002

Bisimulation Minimization and Symbolic Model Checking.
Formal Methods in System Design, 2002

Model Checking: A Complexity-Theoretic Perspective (invited talk).
Electr. Notes Theor. Comput. Sci., 2002

Complete Axiomatizations for Reasoning About Knowledge and Time
CoRR, 2002

A Rice University perspective on software engineering licensing.
Commun. ACM, 2002

The ForSpec Temporal Logic: A New Temporal Property-Specification Language.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Lossless Regular Views.
Proceedings of the Twenty-first ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 2002

Pushdown Specifications.
Proceedings of the Logic for Programming, 2002

Reasoning about Actions and Planning in LTL Action Theories.
Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), 2002

Eliminating Incoherence from Subjective Estimates of Chance.
Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), 2002

Alternation.
Proceedings of the Logics in Artificial Intelligence, European Conference, 2002

Constraint Satisfaction, Bounded Treewidth, and Finite-Variable Logics.
Proceedings of the Principles and Practice of Constraint Programming, 2002

Model Checking Linear Properties of Prefix-Recognizable Systems.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

BDD-Based Decision Procedures for K.
Proceedings of the Automated Deduction, 2002

The Complexity of the Graded µ-Calculus.
Proceedings of the Automated Deduction, 2002

2001
Weak alternating automata are not that weak.
ACM Trans. Comput. Log., 2001

Verification by Augmented Abstraction: The Automata-Theoretic View.
J. Comput. Syst. Sci., 2001

Module Checking.
Inf. Comput., 2001

Model Checking of Safety Properties.
Formal Methods in System Design, 2001

A New Heuristic for Bad Cycle Detection Using BDDs.
Formal Methods in System Design, 2001

Towards an Efficient Library for SAT: a Manifesto.
Electronic Notes in Discrete Mathematics, 2001

On the unusual effectiveness of logic in computer science.
Bulletin of Symbolic Logic, 2001

Branching vs. Linear Time: Final Showdown.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Is There a Best Symbolic Cycle-Detection Algorithm?
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Coverage Metrics for Temporal Logic Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

From Bidirectionality to Alternation.
Proceedings of the Mathematical Foundations of Computer Science 2001, 2001

On Bounded Specifications.
Proceedings of the Logic for Programming, 2001

Synthesizing Distributed Systems.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

On the Complexity of Parity Word Automata.
Proceedings of the Foundations of Software Science and Computation Structures, 2001

View-Based Query Answering and Query Containment over Semistructured Data.
Proceedings of the Database Programming Languages, 8th International Workshop, 2001

Random 3-SAT and BDDs: The Plot Thickens Further.
Proceedings of the Principles and Practice of Constraint Programming, 2001

Extended Temporal Logic Revisited.
Proceedings of the CONCUR 2001, 2001

Benefits of Bounded Model Checking at an Industrial Setting.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

A Practical Approach to Coverage in Model Checking.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

The Hybrid µ-Calculus.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000
An automata-theortetic approach to modular model checking.
ACM Trans. Program. Lang. Syst., 2000

Conjunctive-Query Containment and Constraint Satisfaction.
J. Comput. Syst. Sci., 2000

An automata-theoretic approach to branching-time model checking.
J. ACM, 2000

Constraint Satisfaction and Database Theory: a Tutorial.
Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2000

View-Based Query Processing for Regular Path Queries with Inverse.
Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2000

µ-Calculus Synthesis.
Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

0-1 Laws for Fragments of Existential Second-Order Logic: A Survey.
Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

View-Based Query Processing and Constraint Satisfaction.
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

What is View-Based Query Rewriting?
Proceedings of the 7th International Workshop on Knowledge Representation meets Databases (KRDB 2000), 2000

Containment of Conjunctive Regular Path Queries with Inverse.
Proceedings of the KR 2000, 2000

Answering Regular Path Queries Using Views.
Proceedings of the 16th International Conference on Data Engineering, San Diego, California, USA, February 28, 2000

Fair Equivalence Relations.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

Automated Verification = Graphs, Automata, and Logic.
Proceedings of the Computer Science Logic, 2000

Random 3-SAT: The Plot Thickens.
Proceedings of the Principles and Practice of Constraint Programming, 2000

Open Systems in Reactive Environments: Control and Synthesis.
Proceedings of the CONCUR 2000, 2000

What is Query Rewriting?
Proceedings of the Cooperative Information Agents IV, 2000

An Automata-Theoretic Approach to Reasoning about Infinite-State Systems.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

A Game-Theoretic Approach to Constraint Satisfaction.
Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30, 2000

1999
Reminiscences on Influential Papers.
SIGMOD Record, 1999

The hierarchical approach to modeling knowledge and common knowledge.
Int. J. Game Theory, 1999

Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting.
Electr. Notes Theor. Comput. Sci., 1999

The Complexity of Problems on Graphs Represented as OBDDs.
Chicago J. Theor. Comput. Sci., 1999

Church's problem revisited.
Bulletin of Symbolic Logic, 1999

Common Knowledge Revisited.
Ann. Pure Appl. Logic, 1999

Query Answering Using Views for Data Integration over the Web.
Proceedings of the ACM SIGMOD Workshop on The Web and Databases, 1999

The Weakness of Self-Complementation.
Proceedings of the STACS 99, 1999

Rewriting of Regular Path Queries.
Proceedings of the Atti del Settimo Convegno Nazionale Sistemi Evoluti per Basi di Dati, 1999

Rewriting of Regular Expressions and Regular Path Queries.
Proceedings of the Eighteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 31, 1999

Black Box Checking.
Proceedings of the Formal Methods for Protocol Engineering and Distributed Systems, 1999

Automata-Theoretic Approach to Planning for Temporally Extended Goals.
Proceedings of the Recent Advances in AI Planning, 5th European Conference on Planning, 1999

Strong Cyclic Planning Revisited.
Proceedings of the Recent Advances in AI Planning, 5th European Conference on Planning, 1999

Robust Satisfaction.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

Vacuity Detection in Temporal Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Bisimulation and Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Model Checking of Safety Properties.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Improved Automata Generation for Linear Temporal Logic.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach.
Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999

1998
The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory.
SIAM J. Comput., 1998

Computational Model Theory: An Overview.
Logic Journal of the IGPL, 1998

Common knowledge revisited
CoRR, 1998

Verification of Fair Transition Systems.
Chicago J. Theor. Comput. Sci., 1998

Weak Alternating Automata and Tree Automata Emptiness.
Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, 1998

Complexity of Problems on Graphs Represented as OBDDs (Extended Abstract).
Proceedings of the STACS 98, 1998

Panel: logic in the computer science curriculum.
Proceedings of the 29th SIGCSE Technical Symposium on Computer Science Education, 1998, Atlanta, Georgia, USA, February 26, 1998

Relating linear and branching model checking.
Proceedings of the Programming Concepts and Methods, 1998

Conjunctive-Query Containment and Constraint Satisfaction.
Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1998

Linear vs. Branching Time: A Complexity-Theoretic Perspective.
Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time.
Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Reasoning about The Past with Two-Way Automata.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Bisimulation Minimization in an Automata-Theoretic Verification Framework.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Sometimes and Not Never Re-revisited: On Branching Versus Linear Time.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

Synthesis from Knowledge-Based Specifications (Extended Abstract).
Proceedings of the CONCUR '98: Concurrency Theory, 1998

Alternating Refinement Relations.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

1997
Reasoning about Knowledge: A Response by the Authors.
Minds and Machines, 1997

Special Selection in Logic in Computer Science.
J. Symb. Log., 1997

On the Equivalence of Recursive and Nonrecursive Datalog Programs.
J. Comput. Syst. Sci., 1997

Fixpoint logics, relational machines, and computational complexity.
J. ACM, 1997

Knowledge-Based Programs.
Distributed Computing, 1997

On the decision problem for two-variable first-order logic.
Bulletin of Symbolic Logic, 1997

First-Order Logic with Two Variables and Unary Temporal Logic.
Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

Weak Alternating Automata Are Not That Weak.
Proceedings of the Fifth Israel Symposium on Theory of Computing and Systems, 1997

Verification of Open Systems.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1997

On the Complexity of Verifying Concurrent Transition Systems.
Proceedings of the CONCUR '97: Concurrency Theory, 1997

Modular Model Checking.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

Module Checking Revisited.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Model Checking and Transitive-Closure Logic.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics.
Proceedings of the Automated Deduction, 1997

1996
In Memoriam: Paris C. Kanellakis (1953-1995).
Inf. Comput., 1996

In Memoriam Paris C. Kanellakis.
ACM Comput. Surv., 1996

Rank Predicates vs. Progress Measures in Concurrent-Program Verification.
Chicago J. Theor. Comput. Sci., 1996

Implementing Knowledge-Based Programs.
Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, 1996

Common Knowledge Revisited.
Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, 1996

In Memoriam: Paris C. Kanellakis.
Proceedings of the Fifteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1996

Relating Word and Tree Automata.
Proceedings of the Proceedings, 1996

On the Expressive Power of Variable-Confined Logics.
Proceedings of the Proceedings, 1996

Database Research: Lead, Follow, or Get Out of the Way? - Panel Abstract.
Proceedings of the Twelfth International Conference on Data Engineering, February 26, 1996

Why is Modal Logic So Robustly Decidable?
Proceedings of the Descriptive Complexity and Finite Models, 1996

A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking.
Proceedings of the CONCUR '96, 1996

Verification of Fair Transisiton Systems.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Module Checking.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995
On Monadic NP vs. Monadic co-NP
Inf. Comput., July, 1995

Computing with Infinitary Logic.
Theor. Comput. Sci., 1995

Undecidable Boundedness Problems for Datalog Programs.
J. Log. Program., 1995

On the Expressive Power of Datalog: Tools and a Case Study.
J. Comput. Syst. Sci., 1995

A Nonstandard Approach to the Logical Omniscience Problem.
Artif. Intell., 1995

Simple on-the-fly automatic verification of linear temporal logic.
Proceedings of the Protocol Specification, 1995

On the Complexity of Bounded-Variable Queries.
Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1995

Knowledge-Based Programs.
Proceedings of the Fourteenth Annual ACM Symposium on Principles of Distributed Computing, 1995

On the Complexity of Modular Model Checking
Proceedings of the Proceedings, 1995

On the Complexity of Branching Modular Model Checking (Extended Abstract).
Proceedings of the CONCUR '95: Concurrency Theory, 1995

An Automata-Theoretic Approach to Fair Realizability and Synthesis.
Proceedings of the Computer Aided Verification, 1995

An Automata-Theoretic Approach to Linear Temporal Logic.
Proceedings of the Logics for Concurrency - Structure versus Automata (8th Banff Higher Order Workshop, August 27, 1995

Alternating Automata and Program Verification.
Proceedings of the Computer Science Today: Recent Trends and Developments, 1995

1994
Reasoning About Infinite Computations
Inf. Comput., November, 1994

Algorithmic Knowledge.
Proceedings of the 5th Conference on Theoretical Aspects of Reasoning about Knowledge, 1994

Nontraditional Applications of Automata Theory.
Proceedings of the Theoretical Aspects of Computer Software, 1994

On the Complexity of Equivalence between Recursive and Nonrecursive Datalog Programs.
Proceedings of the Thirteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1994

An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract).
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

An Operational Semantics for Knowledge Bases.
Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31, 1994

1993
The Logical Data Model.
ACM Trans. Database Syst., 1993

On the Complexity of Queries in the Logical Data Model.
Theor. Comput. Sci., 1993

Logical Query Optimization by Proff-Tree Transformation.
J. Comput. Syst. Sci., 1993

Undecidable Optimization Problems for Database Logic Programs.
J. ACM, 1993

Monotone monadic SNP and constraint satisfaction.
Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, 1993

Parametric real-time reasoning.
Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, 1993

Optimization of Real Conjunctive Queries.
Proceedings of the Twelfth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1993

The Complexity of Set Constraints.
Proceedings of the Computer Science Logic, 7th Workshop, 1993

On Monadic NP vs. Monadic co-NP (Extended Abstract).
Proceedings of the Eigth Annual Structure in Complexity Theory Conference, 1993

1992
Infinitary Logics and 0-1 Laws
Inf. Comput., June, 1992

What Is an Inference Rule?
J. Symb. Log., 1992

What Can Machines Know? On the Properties of Knowledge in Distributed Systems.
J. ACM, 1992

Memory-Efficient Algorithms for the Verification of Temporal Properties.
Formal Methods in System Design, 1992

The Expressive Power of the Kierarchical Approach to Modeling Knowledge and Common Knowledge.
Proceedings of the 4th Conference on Theoretical Aspects of Reasoning about Knowledge, 1992

On the Equivalence of Recursive and Nonrecursive Datalog Programs.
Proceedings of the Eleventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1992

Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory
Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

Computing with Infinitary Logic.
Proceedings of the Database Theory, 1992

Infinitary Logic for Computer Science.
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Fixpoint Logics, Relational Machines, and Computational Complexity.
Proceedings of the Seventh Annual Structure in Complexity Theory Conference, 1992

Automata Theory for Database Theoreticans.
Proceedings of the Theoretical Studies in Computer Science, 1992

1991
Database Logic Programming.
J. Log. Program., 1991

A Model-Theoretic Analysis of Knowledge.
J. ACM, 1991

Verification of Concurrent Programs: The Automata-Theoretic Framework.
Ann. Pure Appl. Logic, 1991

Tools for Datalog Boundedness.
Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1991

Logic Programs as Types for Logic Programs
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

Model Checking vs. Theorem Proving: A Manifesto.
Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR'91). Cambridge, 1991

1990
Polynomial-Time Implication Problems for Unary Inclusion Dependencies
J. ACM, January, 1990

Endmarkers can Make a Difference.
Inf. Process. Lett., 1990

0-1 Laws and Decision Problems for Fragments of Second-Order Logic
Inf. Comput., 1990

A Nonstandard Approach to the Logical Omniscience Problem.
Proceedings of the 3rd Conference on Theoretical Aspects of Reasoning about Knowledge, 1990

On the Expressive Power of Datalog: Tools and a Case Study.
Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1990

0-1 Laws for Infinitary Logics (Preliminary Report)
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

On the Power of Bounded Concurrency~III: Reasoning About Programs (Preliminary Report)
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

What is an inference rule?
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

Global Optimization Problems for Database Logic Programs.
Proceedings of the Logic Programming, 1990

Memory Efficient Algorithms for the Verification of Temporal Properties.
Proceedings of the Computer-Aided Verification, 1990

Memory Efficient Algorithms for the Verification of Temporal Properties.
Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990

1989
The Complexity of Reasoning about Knowledge and Time. I. Lower Bounds.
J. Comput. Syst. Sci., 1989

A Note on the Reduction of Two-Way Automata to One-Way Automata.
Inf. Process. Lett., 1989

On omega-Automata and Temporal Logic (Preliminary Report)
Proceedings of the 21st Annual ACM Symposium on Theory of Computing, 1989

Automata Theory for Database Theoreticans.
Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1989

Safety of Datalog Queries over Infinite Databases.
Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1989

Proof-Tree Transformation Theorems and Their Applications.
Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1989

On the Complexity of Epistemic Reasoning
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

1988
Response to a Letter to the Editor.
IEEE Software, 1988

The Universal-Relation Data Model for Logical Independence.
IEEE Software, 1988

Reasoning about Knowledge and Time in Asynchronous Systems
Proceedings of the 20th Annual ACM Symposium on Theory of Computing, 1988

Decidable Optimization Problems for Database Logic Programs (Preliminary Report)
Proceedings of the 20th Annual ACM Symposium on Theory of Computing, 1988

Database Logic Programming, Deductive Databases, and Expert Database Systems.
Proceedings of the 1988 ACM SIGMOD International Conference on Management of Data, 1988

A Temporal Fixpoint Calculus.
Proceedings of the Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988

Decidability and Undecidability Results for Boundedness of Linear Recursive Queries.
Proceedings of the Seventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1988

The Complexity of Ordering Subgoals.
Proceedings of the Seventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1988

0-1 Laws and Decision Problems for Fragments of Second-Order Logic
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

On the Complexity of Queries in the Logical Data Model (Extended Abstract).
Proceedings of the ICDT'88, 2nd International Conference on Database Theory, Bruges, Belgium, August 31, 1988

An Automata-Theoretic Approach to Protocol Verification (Abstract).
Proceedings of the Concurrency 88: International Conference on Concurrency, 1988

1987
The Complementation Problem for Büchi Automata with Appplications to Temporal Logic.
Theor. Comput. Sci., 1987

Unified Verification Theory.
Proceedings of the Temporal Logic in Specification, 1987

The Decision Problem for the Probabilities of Higher-Order Properties
Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987

Verification of Concurrent Programs: The Automata-Theoretic Framework
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

Undecidable Optimization Problems for Database Logic Programs
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986
Automata-Theoretic Techniques for Modal Logics of Programs.
J. Comput. Syst. Sci., 1986

Querying Logical Databases.
J. Comput. Syst. Sci., 1986

Notions of dependency satisfaction.
J. ACM, 1986

On the Expressive Power of Data Dependencies.
Acta Inf., 1986

Updating Logical Databases.
Advances in Computing Research, 1986

On Epistemic Logic and Logical Omniscience.
Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, 1986

Knowledge and Implicit Knowledge in a Distributed Environment: Preliminary Report.
Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, 1986

The Complexity of Reasoning about Knowledge and Time: Extended Abstract
Proceedings of the 18th Annual ACM Symposium on Theory of Computing, 1986

Reasoning about Fair Concurrent Programs
Proceedings of the 18th Annual ACM Symposium on Theory of Computing, 1986

On the Integrity of Databases with Incomplete Information.
Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1986

An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

What Can Machines Know? On the Epistemic Properties of Machines.
Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986

1985
Formal Systems for Join Dependencies.
Theor. Comput. Sci., 1985

The Implication Problem for Functional and Inclusion Dependencies is Undecidable.
SIAM J. Comput., 1985

A responce to "A complete axiomatisation for full join dependencies in relations".
Bulletin of the EATCS, 1985

A simple proof that connectivity of finite graphs is not first-order definable.
Bulletin of the EATCS, 1985

Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report
Proceedings of the 17th Annual ACM Symposium on Theory of Computing, 1985

An Internal Semantics for Modal Logic: Preliminary Report
Proceedings of the 17th Annual ACM Symposium on Theory of Computing, 1985

On the Expressive Power of the Logical Data Model (Preliminary Report).
Proceedings of the 1985 ACM SIGMOD International Conference on Management of Data, 1985

Querying Logical Databases.
Proceedings of the Fourth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1985

The Taming of Converse: Reasoning about Two-way Computations.
Proceedings of the Logics of Programs, 1985

A Model-Theoretic Analysis of Monotonic Knowledge.
Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, 1985

The Complementation Problem for Büchi Automata with Applications to Temporal Logic (Extended Abstract).
Proceedings of the Automata, 1985

Automatic Verification of Probabilistic Concurrent Finite-State Programs
Proceedings of the 26th Annual Symposium on Foundations of Computer Science, 1985

1984
On Acyclic Database Decompositions
Information and Control, May, 1984

On the Foundations of the Universal Relation Model.
ACM Trans. Database Syst., 1984

Formal Systems for Tuple and Equality Generating Dependencies.
SIAM J. Comput., 1984

The Implication and Finite Implication Problems for Typed Template Dependencies.
J. Comput. Syst. Sci., 1984

A Proof Procedure for Data Dependencies.
J. ACM, 1984

A Note on Lossless Database Decompositions.
Inf. Process. Lett., 1984

Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract)
Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984

A New Approach to Database Logic.
Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1984

On the Equivalence of Logical Databases.
Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1984

On the Complexity and Axiomatizability of Consistent Database States.
Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1984

The Theory of Data Dependencies - An Overview.
Proceedings of the Automata, 1984

A Model-Theoretic Analysis of Knowledge: Preliminary Report
Proceedings of the 25th Annual Symposium on Foundations of Computer Science, 1984

1983
Armstrong Databases for Functional and Inclusion Dependencies.
Inf. Process. Lett., 1983

Inferring Multivalued Dependencies From Functional and Join Dependencies.
Acta Inf., 1983

Second-Order Dependency Theory.
Proceedings of the XP4.5 Workshop on Database Theory, 1983 Palo Alto, California, USA, 1983

Unary Inclusion Dependencies have Polynomial Time Inference Problems (Extended Abstract)
Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 1983

The Revenge of the JD.
Proceedings of the Second ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1983

On the Semantics of Updates in Databases.
Proceedings of the Second ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1983

Yet Another Process Logic (Preliminary Version).
Proceedings of the Logics of Programs, 1983

Reasoning about Infinite Computation Paths (Extended Abstract)
Proceedings of the 24th Annual Symposium on Foundations of Computer Science, 1983

1982
The Complexity of Relational Query Languages (Extended Abstract)
Proceedings of the 14th Annual ACM Symposium on Theory of Computing, 1982

The Implication and Finite Implication Problems for Typed Template Dependencies.
Proceedings of the ACM Symposium on Principles of Database Systems, 1982

On Decomposition of Relational Databases
Proceedings of the 23rd Annual Symposium on Foundations of Computer Science, 1982

1981
A Note on Decompositions of Relational Databases.
SIGMOD Record, 1981

The Decision Problem for Database Dependencies.
Inf. Process. Lett., 1981

The Implication Problem for Data Dependencies.
Proceedings of the Automata, 1981

Global Decision Problems for Relational Databases
Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, 1981

1980
Decision Problems for Data Dependencies.
Proceedings of the XP1 Workshop on Relational Database Theory, 30 June, 1980

1979
On the Properties of Join Dependencies.
Proceedings of the Advances in Data Base Theory, 1979


  Loading...