Moshe Y. Vardi

Affiliations:
  • Rice University, Department of Computer Science


According to our database1, Moshe Y. Vardi authored at least 653 papers between 1979 and 2024.

Collaborative distances:
  • Dijkstra number2 of three.
  • Erdős number3 of two.

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 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Computing, You Have Blood on Your Hands!
Commun. ACM, January, 2024

Model-Guided Synthesis for LTL over Finite Traces.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

2023
What Came First, Math or Computing?
Commun. ACM, November, 2023

To Regulate Tech, Nullify Click-Through Contracts.
Commun. ACM, September, 2023

Revisiting ACM's Open-Conference Principle.
Commun. ACM, July, 2023

On the power of finite ambiguity in Büchi complementation.
Inf. Comput., June, 2023

ACM for the Public Good.
Commun. ACM, May, 2023

Who Is Responsible Around Here?
Commun. ACM, March, 2023

On Strategies in Synthesis Over Finite Traces.
CoRR, 2023

Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints.
CoRR, 2023

How Not to Win a Tech War.
Commun. ACM, 2023

Logical Algorithmics: From Theory to Practice (Invited Talk).
Proceedings of the 40th International Symposium on Theoretical Aspects of Computer Science, 2023

Solving Quantum-Inspired Perfect Matching Problems via Tutte-Theorem-Based Hybrid Boolean Constraints.
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, 2023

Multi-Agent Systems with Quantitative Satisficing Goals.
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, 2023

Extracting generalizable skills from a single plan execution using abstraction-critical state detection.
Proceedings of the IEEE International Conference on Robotics and Automation, 2023

Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

How to Be An Ethical Technologist.
Proceedings of the Engineering of Computer-Based Systems - 8th International Conference, 2023

Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata.
Proceedings of the 34th International Conference on Concurrency Theory, 2023

Model Checking Strategies from Synthesis over Finite Traces.
Proceedings of the Automated Technology for Verification and Analysis, 2023

2022
Finite-trace and generalized-reactivity specifications in temporal synthesis.
Formal Methods Syst. Des., December, 2022

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition".
Dataset, May, 2022

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition".
Dataset, May, 2022

Functional synthesis via input-output separation.
Formal Methods Syst. Des., April, 2022

Sequential Relational Decomposition.
Log. Methods Comput. Sci., 2022

Comparator automata in quantitative verification.
Log. Methods Comput. Sci., 2022

Satisfiability checking for Mission-time LTL (MLTL).
Inf. Comput., 2022

Quantum-Inspired Perfect Matching under Vertex-Color Constraints.
CoRR, 2022

DPER: Dynamic Programming for Exist-Random Stochastic SAT.
CoRR, 2022

DPO: Dynamic-Programming Optimization on Hybrid Constraints.
CoRR, 2022

DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving.
CoRR, 2022

Accountability and liability in computing.
Commun. ACM, 2022

Technology and democracy.
Commun. ACM, 2022

An association of the members, by the members, for the members.
Commun. ACM, 2022

War and tech (and ACM).
Commun. ACM, 2022

ACM, ethics, and corporate behavior.
Commun. ACM, 2022

Will AI destroy education?
Commun. ACM, 2022

Automatic Cross-domain Task Plan Transfer by Caching Abstract Skills.
Proceedings of the Algorithmic Foundations of Robotics XV, 2022

Compositional Safety LTL Synthesis.
Proceedings of the Verified Software. Theories, Tools and Experiments, 2022

Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk).
Proceedings of the 29th International Symposium on Temporal Representation and Reasoning, 2022

ZDD Boolean Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Verification and Realizability in Finite-Horizon Multiagent Systems.
Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, 2022

Public and Private Affairs in Strategic Reasoning.
Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, 2022

Efficient Task Planning Using Abstract Skills and Dynamic Road Map Matching.
Proceedings of the Robotics Research, 2022

LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

DPSampler: Exact Weighted Sampling Using Dynamic Programming.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

Program Verification: A 70+-Year History.
Proceedings of the 17th International Conference on Software Technologies, 2022

Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Towards a Grand Unification of Büchi Complementation Constructions.
Proceedings of the Principles of Systems Design, 2022

Constraint-Driven Explanations for Black-Box ML Models.
Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022

Synthesis from Satisficing and Temporal Goals.
Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022

Efficiency vs. Resilience: Lessons from COVID-19.
Perspectives on Digital Humanism, 2022

2021
Approximate Model Counting.
Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Strategy Logic with Imperfect Information.
ACM Trans. Comput. Log., 2021

Automata Linear Dynamic Logic on Finite Traces.
CoRR, 2021

Congruence Relations for Büchi Automata.
CoRR, 2021

On the Power of Automata Minimization in Temporal Synthesis.
Proceedings of the Proceedings 12th International Symposium on Games, 2021

The paradox of choice in computing-research conferences.
Commun. ACM, 2021

The sand-heap paradox of privacy and influence.
Commun. ACM, 2021

Program verification: vision and reality.
Commun. ACM, 2021

The agency trilemma and ACM.
Commun. ACM, 2021

The people vs. tech.
Commun. ACM, 2021

Reboot the computing-research publication systems.
Commun. ACM, 2021

Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions.
Artif. Intell., 2021

On Satisficing in Quantitative Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Deep Tech Ethics: An Approach to Teaching Social Justice in Computer Science.
Proceedings of the SIGCSE '21: The 52nd ACM Technical Symposium on Computer Science Education, 2021

Panel on "Past and Future of Computer Science Theory" (Discussion Paper).
Proceedings of the 29th Italian Symposium on Advanced Database Systems, 2021

ProCount: Weighted Projected Model Counting with Graded Project-Join Trees.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Synthesizing Good-Enough Strategies for LTLf Specifications.
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Finite-Horizon Synthesis for Probabilistic Manipulation Domains.
Proceedings of the IEEE International Conference on Robotics and Automation, 2021

Congruence Relations for Büchi Automata.
Proceedings of the Formal Methods - 24th International Symposium, 2021

Adapting Behaviors via Reactive Synthesis.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle.
Proceedings of the Model Checking, Synthesis, and Learning, 2021

Linear Temporal Logic - From Infinite to Finite Horizon.
Proceedings of the Automated Technology for Verification and Analysis, 2021

Nash Equilibria in Finite-Horizon Multiagent Concurrent Games.
Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

On-the-fly Synthesis for LTL over Finite Traces.
Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

On Continuous Local BDD-Based Search for Hybrid SAT Solving.
Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

Verification.
Proceedings of the Handbook of Automata Theory., 2021

2020
FPRAS Approximation of the Matrix Permanent in Practice.
CoRR, 2020

LTLf Synthesis on Probabilistic Systems.
Proceedings of the Proceedings 11th International Symposium on Games, 2020

LTLf Synthesis under Partial Observability: From Theory to Practice.
Proceedings of the Proceedings 11th International Symposium on Games, 2020

Understanding Boolean Function Learnability on Deep Neural Networks.
CoRR, 2020

On Uniformly Sampling Traces of a Transition System (Extended Version).
CoRR, 2020

Computer-Aided Personalized Education.
CoRR, 2020

Parallel Weighted Model Counting with Tensor Networks.
CoRR, 2020

On the Power of Unambiguity in Büchi Complementation.
Proceedings of the Proceedings 11th International Symposium on Games, 2020

What should be done about social media?
Commun. ACM, 2020

Where have all the domestic graduate students gone?
Commun. ACM, 2020

A computational lens on economics.
Commun. ACM, 2020

Efficiency vs. resilience: what COVID-19 teaches computing.
Commun. ACM, 2020

Advancing computing as a science and profession: but to what end?
Commun. ACM, 2020

Publish <i>and</i> perish.
Commun. ACM, 2020

SAT-based explicit LTLf satisfiability checking.
Artif. Intell., 2020

Two-Stage Technique for LTLf Synthesis Under LTL Assumptions.
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020

Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective.
Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, 2020

Assume-Guarantee Synthesis for Prompt Linear Temporal Logic.
Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, 2020

On Uniformly Sampling Traces of a Transition System.
Proceedings of the IEEE/ACM International Conference On Computer Aided Design, 2020

Runtime Verification on FPGAs with LTLf Specifications.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees.
Proceedings of the Principles and Practice of Constraint Programming, 2020

LTLƒ Synthesis with Fairness and Stability Assumptions.
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints.
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

ADDMC: Weighted Model Counting with Algebraic Decision Diagrams.
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications.
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

On the Unreasonable Effectiveness of SAT Solvers.
Proceedings of the Beyond the Worst-Case Analysis of Algorithms, 2020

2019
Principled network reliability approximation: A counting-based approach.
Reliab. Eng. Syst. Saf., 2019

Automated Abstraction of Manipulation Domains for Cost-Based Reactive Synthesis.
IEEE Robotics Autom. Lett., 2019

SAT-based explicit LTL reasoning and its application to satisfiability checking.
Formal Methods Syst. Des., 2019

Efficient Contraction of Large Tensor Networks for Weighted Model Counting through Graph Decompositions.
CoRR, 2019

ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams.
CoRR, 2019

First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation.
CoRR, 2019

Not all FPRASs are equal: demystifying FPRASs for DNF-counting.
Constraints An Int. J., 2019

The winner-takes-all tech corporation.
Commun. ACM, 2019

The long game of research.
Commun. ACM, 2019

To serve humanity.
Commun. ACM, 2019

Quantum hype and quantum skepticism.
Commun. ACM, 2019

Lost in math?
Commun. ACM, 2019

Are we having an ethical crisis in computing?
Commun. ACM, 2019

Intersection and Rotation of Assumption Literals Boosts Bug-Finding.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2019

First-Order vs. Second-Order Encodings for \textsc ltl_f -to-Automata Translation.
Proceedings of the Theory and Applications of Models of Computation, 2019

Partitioning Techniques in LTLf Synthesis.
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019

Not All FPRASs are Equal: Demystifying FPRASs for DNF-Counting (Extended Abstract).
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019

Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks.
Proceedings of the International Conference on Robotics and Automation, 2019

On Symbolic Approaches for Computing the Matrix Permanent.
Proceedings of the Principles and Practice of Constraint Programming, 2019

Satisfiability Checking for Mission-Time LTL.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Learning to Solve NP-Complete Problems: A Graph Neural Network for Decision TSP.
Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

Labor Division with Movable Walls: Composing Executable Specifications with Machine Learning and Search (Blue Sky Idea).
Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

On the Hardness of Probabilistic Inference Relaxations.
Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

Unbounded Orchestrations of Transducers for Manufacturing.
Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018
Mode-Target Games: Reactive Synthesis for Control Applications.
IEEE Trans. Autom. Control., 2018

Accelerating LTL satisfiability checking by SAT solvers.
J. Log. Comput., 2018

4th International Workshop on Strategic Reasoning (SR 2016).
Inf. Comput., 2018

An explicit transition system construction approach to LTL satisfiability checking.
Formal Aspects Comput., 2018

Network Reliability Estimation in Theory and Practice.
CoRR, 2018

Self-reference and section 230.
Commun. ACM, 2018

Move fast and break things.
Commun. ACM, 2018

How the hippies destroyed the internet.
Commun. ACM, 2018

How we lost the women in computing.
Commun. ACM, 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

Solving Parity Games: Explicit vs Symbolic.
Proceedings of the Implementation and Application of Automata, 2018

The Siren Song of Temporal Synthesis (Invited Talk).
Proceedings of the 29th International Conference on Concurrency Theory, 2018

SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Automata vs Linear-Programming Discounted-Sum Inclusion.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Synthesis of Orchestrations of Transducers for Manufacturing.
Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 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.
Bull. EATCS, 2017

Supervisory control and reactive synthesis: a comparative introduction.
Discret. Event Dyn. Syst., 2017

Reasoning about Strategies: on the Satisfiability Problem.
Log. Methods Comput. Sci., 2017

Would Turing have won the Turing award?
Commun. ACM, 2017

Divination by program committee.
Commun. ACM, 2017

Ten years at the helm of <i>communications of the ACM</i>.
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

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 Syst. Des., 2016

Alonzo Church Award 2016 - Call for Nominations.
Bull. EATCS, 2016

Viewpoints on "Logic activities in Europe", twenty years later.
Bull. EATCS, 2016

Approximate Reachability.
CoRR, 2016

On computing minimal independent support and its applications to sampling and counting.
Constraints An Int. J., 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

LTL<sub>f</sub> and LDL<sub>f</sub> 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.
ACM SIGLOG News, 2015

Special issue on SR 2013.
Inf. Comput., 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

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

Controller Synthesis for Mode-Target Games.
Proceedings of the 5th IFAC Conference on Analysis and Design of Hybrid Systems, 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.
Log. Methods Comput. Sci., 2014

Synthesis from Probabilistic Components.
Log. Methods Comput. Sci., 2014

Fast LTL Satisfiability Checking by SAT Solvers.
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

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.
Int. J. Softw. Tools Technol. Transf., 2013

Synthesis from component libraries.
Int. J. Softw. Tools Technol. Transf., 2013

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

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

Unifying Büchi Complementation Constructions
Log. Methods Comput. Sci., 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

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

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.
Proc. VLDB Endow., 2012

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

2011 CAV award announcement.
Formal Methods Syst. Des., 2012

Optimized temporal monitors for SystemC.
Formal Methods Syst. Des., 2012

2010 CAV award announcement.
Formal Methods Syst. Des., 2012

Temporal property verification as a program analysis task - Extended Version.
Formal Methods Syst. Des., 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
Log. Methods Comput. Sci., 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

Automatic aspectization of systemC.
Proceedings of the 2012 Workshop on Modularity in Systems Software, 2012

2011
Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking.
Int. J. Softw. Tools Technol. Transf., 2011

Motion Planning with Complex Goals.
IEEE Robotics Autom. Mag., 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

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

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.
Int. J. Softw. Tools Technol. Transf., 2010

2009 CAV award announcement.
Formal Methods Syst. Des., 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

<i>Globalization and Offshoring of Software</i> revisited.
Commun. ACM, 2010

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

More debate, please!
Commun. ACM, 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

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

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 Electron., 2009

Hybrid systems: from verification to falsification by combining motion planning and discrete search.
Formal Methods Syst. Des., 2009

From liveness to promptness.
Formal Methods Syst. Des., 2009

The 2008 CAV Award citation.
Formal Methods Syst. Des., 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

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

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

2008
Multi-Objective Model Checking of Markov Decision Processes.
Log. Methods Comput. Sci., 2008

The Complexity of Enriched Mu-Calculi.
Log. Methods Comput. Sci., 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 Syst. Des., 2007

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

Property-Driven Partitioning for Abstraction Refinement.
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

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

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

Automata-theoretic techniques for temporal reasoning.
Proceedings of the Handbook of Modal Logic., 2007

2006
Coverage metrics for formal verification.
Int. J. Softw. Tools Technol. Transf., 2006

BDD-based decision procedures for the modal logic K.
J. Appl. Non Class. Logics, 2006

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

Aggregating disparate estimates of chance.
Games Econ. Behav., 2006

Coverage metrics for temporal logic model checking<sup>*</sup>.
Formal Methods Syst. Des., 2006

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

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

Automata theory: its relevance to computer science students and course contents.
Proceedings of the 37th 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 <i>µ</i>-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

The Phase Transition in the Random HornSAT Problem.
Proceedings of the Computational Complexity and Statistical Physics., 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 Rec., 2005

Symbolic Techniques in Satisfiability Solving.
J. Autom. Reason., 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

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

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

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

SAT-based Induction for Temporal Safety Properties.
Proceedings of the 2nd International Workshop on Bounded Model Checking, 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 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

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

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

Vacuity detection in temporal model checking.
Int. J. Softw. Tools Technol. Transf., 2003

Reasoning on regular path queries.
SIGMOD Rec., 2003

Random 3-SAT: The Plot Thickens.
Constraints An Int. J., 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

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

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

Π<sub>2</sub> ∩ Σ<sub>2</sub> ≡ 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

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.
J. Autom. Lang. Comb., 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 Syst. Des., 2002

Model Checking: A Complexity-Theoretic Perspective (invited talk).
Proceedings of the Parallel and Distributed Model Checking, 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 Syst. Des., 2001

A New Heuristic for Bad Cycle Detection Using BDDs.
Formal Methods Syst. Des., 2001

Towards an Efficient Library for SAT: a Manifesto.
Electron. Notes Discret. Math., 2001

On the unusual effectiveness of logic in computer science.
Bull. Symb. Log., 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

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

Automated Verification = Graphs, Automata, and Logic.
Proceedings of the Computer Science Logic, 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 Rec., 1999

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

Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting.
Proceedings of the First International Workshop on Symbolic Model Checking, 1999

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

Church's problem revisited.
Bull. Symb. Log., 1999

Common Knowledge Revisited.
Ann. Pure Appl. Log., 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

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

Bisimulation and Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 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.
Log. J. IGPL, 1998

Verification of Fair Transition Systems.
Chic. 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

Relating linear and branching model checking.
Proceedings of the Programming Concepts and Methods, 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 Mach., 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 Comput., 1997

On the decision problem for two-variable first-order logic.
Bull. Symb. Log., 1997

Verification of Open Systems.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 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.
Chic. J. Theor. Comput. Sci., 1996

Implementing Knowledge-Based Programs.
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

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

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, 1995

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

Reasoning About Knowledge.
MIT Press, ISBN: 9780262562003, 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 <i>Real</i> 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 Syst. Des., 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

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

Infinitary Logic for Computer Science.
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 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. Log., 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 Artificial and Mathematical Theory of Computation, 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

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

Global Optimization Problems for Database Logic Programs.
Proceedings of the Logic Programming, 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

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 Softw., 1988

The Universal-Relation Data Model for Logical Independence.
IEEE Softw., 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

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

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 Informatica, 1986

Updating Logical Databases.
Adv. Comput. Res., 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".
Bull. EATCS, 1985

A simple proof that connectivity of finite graphs is not first-order definable.
Bull. 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

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
Inf. 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 Informatica, 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

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

1981
בעיית הגרירה לתלויות בין נתונים במסדי נתונים יחסיים (The implication problem for data dependencies in relational databases.).
PhD thesis, 1981

A Note on Decompositions of Relational Databases.
SIGMOD Rec., 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...