Moshe Y. Vardi
According to our database1, Moshe Y. Vardi
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 OtherLinks
Homepages:
-
at www.acm.org
-
at viaf.org
-
at isni.org
-
at id.loc.gov
-
at d-nb.info
-
at dl.acm.org
On csauthors.net:
Bibliography
2018
Mode-Target Games: Reactive Synthesis for Control Applications.
IEEE Trans. Automat. Contr., 2018
An explicit transition system construction approach to LTL satisfiability checking.
Formal Asp. Comput., 2018
Open access and ACM.
Commun. ACM, 2018
A declaration of the dependence of cyberspace.
Commun. ACM, 2018
Computer professionals for social responsibility.
Commun. ACM, 2018
Comparator Automata in Quantitative Verification.
Proceedings of the Foundations of Software Science and Computation Structures, 2018
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
The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas.
CoRR, 2017
On Hashing-Based Approaches to Approximate DNF-Counting.
CoRR, 2017
A Symbolic Approach to Safety LTL Synthesis.
CoRR, 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
Would Turing have won the Turing award?
Commun. ACM, 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
Reactive synthesis for finite tasks under resource constraints.
Proceedings of the 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, 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
Safety model checking with complementary approximations.
Proceedings of the 2017 IEEE/ACM International Conference on Computer-Aided Design, 2017
A Symbolic Approach to Safety ltl Synthesis.
Proceedings of the Hardware and Software: Verification and Testing, 2017
On Hashing-Based Approaches to Approximate DNF-Counting.
Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2017
Flow Games.
Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2017
Factored boolean functional synthesis.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 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