Moshe Y. Vardi

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

Regular Real Analysis.

[BibT_eX]

[DOI]

Swarat Chaudhuri

Sriram Sankaranarayanan

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

Linear Temporal Logic and Linear Dynamic Logic on Finite Traces.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

Iterative temporal motion planning for hybrid systems in partially unknown environments.

[BibT_eX]

[DOI]

Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models.

[BibT_eX]

[DOI]

Sonali Dutta

Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, 2013

A Scalable Approximate Model Counter.

[BibT_eX]

[DOI]

Supratik Chakraborty

Kuldeep S. Meel

Proceedings of the Principles and Practice of Constraint Programming, 2013

A Scalable and Nearly Uniform Generator of SAT Witnesses.

[BibT_eX]

[DOI]

Supratik Chakraborty

Kuldeep S. Meel

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Query Processing under GLAV Mappings for Relational and Graph Databases.

[BibT_eX]

[DOI]

Proc. VLDB Endow., 2012

Once and for all.

[BibT_eX]

[DOI]

Amir Pnueli

J. Comput. Syst. Sci., 2012

2011 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2012

Optimized temporal monitors for SystemC.

[BibT_eX]

[DOI]

Kristin Y. Rozier

Formal Methods Syst. Des., 2012

2010 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2012

Temporal property verification as a program analysis task - Extended Version.

[BibT_eX]

[DOI]

Byron Cook

Eric Koskinen

Formal Methods Syst. Des., 2012

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

[BibT_eX]

[DOI]

Kurt Mehlhorn

Marc Herbstritt

Dagstuhl Reports, 2012

A Decidable Fragment of Strategy Logic

[BibT_eX]

[DOI]

CoRR, 2012

Büchi Complementation and Size-Change Termination

[BibT_eX]

[DOI]

Seth Fogarty

Log. Methods Comput. Sci., 2012

Will MOOCs destroy academia?

[BibT_eX]

[DOI]

Commun. ACM, 2012

Why ACM?

[BibT_eX]

[DOI]

Commun. ACM, 2012

Predatory scholarly publishing.

[BibT_eX]

[DOI]

Commun. ACM, 2012

Fair access.

[BibT_eX]

[DOI]

Commun. ACM, 2012

What is an algorithm?

[BibT_eX]

[DOI]

Commun. ACM, 2012

Artificial intelligence: past and future.

[BibT_eX]

[DOI]

Commun. ACM, 2012

Compositional Temporal Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking.

[BibT_eX]

[DOI]

Kristin Yvonne Rozier

Proceedings of the Hardware and Software: Verification and Testing, 2012

Synthesizing Probabilistic Composers.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2012

What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

Bma: Visual Tool for Modeling and Analyzing Biological Networks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Automatic aspectization of systemC.

[BibT_eX]

[DOI]

Proceedings of the 2012 Workshop on Modularity in Systems Software, 2012

2011

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

[BibT_eX]

[DOI]

Roberto Sebastiani

Stefano Tonetta

Int. J. Softw. Tools Technol. Transf., 2011

Motion Planning with Complex Goals.

[BibT_eX]

[DOI]

IEEE Robotics Autom. Mag., 2011

The Complexity of Integer Bound Propagation.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2011

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

[BibT_eX]

[DOI]

Dagstuhl Manifestos, 2011

Synthesis from Recursive-Components Libraries

[BibT_eX]

[DOI]

Yoad Lustig

Proceedings of Second International Symposium on Games, 2011

Computing for humans.

[BibT_eX]

[DOI]

Commun. ACM, 2011

Is Moore's Party over?

[BibT_eX]

[DOI]

Commun. ACM, 2011

Are you talking to me?

[BibT_eX]

[DOI]

Commun. ACM, 2011

Solving the unsolvable.

[BibT_eX]

[DOI]

Commun. ACM, 2011

Technology has social consequences.

[BibT_eX]

[DOI]

Commun. ACM, 2011

Fumbling the future.

[BibT_eX]

[DOI]

Commun. ACM, 2011

Where have all the workshops gone?

[BibT_eX]

[DOI]

Commun. ACM, 2011

Temporal Synthesis for Bounded Systems and Environments.

[BibT_eX]

[DOI]

Proceedings of the 28th International Symposium on Theoretical Aspects of Computer Science, 2011

Simplifying schema mappings.

[BibT_eX]

[DOI]

Proceedings of the Database Theory, 2011

Constraints, Graphs, Algebra, Logic, and Complexity (Invited Talk).

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Kristin Y. Rozier

Proceedings of the FM 2011: Formal Methods, 2011

The Only Way Is Up.

[BibT_eX]

[DOI]

Jasmin Fisher

Proceedings of the FM 2011: Formal Methods, 2011

Branching vs. Linear Time: Semantical Perspective.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2011

Dynamic Reactive Modules.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Temporal Property Verification as a Program Analysis Task.

[BibT_eX]

[DOI]

Byron Cook

Eric Koskinen

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Motion Planning With Dynamics by a Synergistic Combination of Layers of Planning.

[BibT_eX]

[DOI]

IEEE Trans. Robotics, 2010

LTL satisfiability checking.

[BibT_eX]

[DOI]

Kristin Y. Rozier

Int. J. Softw. Tools Technol. Transf., 2010

2009 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2010

View Synthesis from Schema Mappings

[BibT_eX]

[DOI]

CoRR, 2010

On P, NP, and computational complexity.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Science has only two legs.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Hypercriticality.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Globalization and Offshoring of Software revisited.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Revisiting the publication culture in computing research.

[BibT_eX]

[DOI]

Commun. ACM, 2010

More debate, please!

[BibT_eX]

[DOI]

Commun. ACM, 2010

Efficient Büchi Universality Checking.

[BibT_eX]

[DOI]

Seth Fogarty

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Optimized temporal monitors for SystemC.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - First International Conference, 2010

Monitoring temporal SystemC properties.

[BibT_eX]

[DOI]

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

Synthesis of Trigger Properties.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Sampling-based motion planning with temporal goals.

[BibT_eX]

[DOI]

Amit Bhatia

Proceedings of the IEEE International Conference on Robotics and Automation, 2010

Reasoning About Strategies.

[BibT_eX]

[DOI]

Fabio Mogavero

Aniello Murano

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

Motion planning with hybrid dynamics and temporal goals.

[BibT_eX]

[DOI]

Amit Bhatia

Proceedings of the 49th IEEE Conference on Decision and Control, 2010

An Automata-Theoretic Approach to Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Time for Verification, 2010

From Automated Verification to Automated Design.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Automated Planning and Scheduling, 2010

Node Selection Query Languages for Trees.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, 2010

2009

Intelligate: An Algorithm for Learning Boolean Functions for Dynamic Power Reduction.

[BibT_eX]

[DOI]

Roni Wiener

Gila Kamhi

J. Low Power Electron., 2009

Hybrid systems: from verification to falsification by combining motion planning and discrete search.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

From liveness to promptness.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

The 2008 CAV Award citation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

Is the image crisis over?

[BibT_eX]

[DOI]

Commun. ACM, 2009

The financial meltdown and computing.

[BibT_eX]

[DOI]

Commun. ACM, 2009

Open, closed, or clopen access?

[BibT_eX]

[DOI]

Commun. ACM, 2009

Conferences vs. journals in computing research.

[BibT_eX]

[DOI]

Commun. ACM, 2009

"Yes, it can be done".

[BibT_eX]

[DOI]

Commun. ACM, 2009

How are we doing?

[BibT_eX]

[DOI]

Commun. ACM, 2009

Constraints, Graphs, Algebra, Logic, and Complexity.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Models of Computation, 6th Annual Conference, 2009

Symbolic Techniques in Propositional Satisfiability Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Model Checking as A Reachability Problem.

[BibT_eX]

[DOI]

Proceedings of the Reachability Problems, 3rd International Workshop, 2009

Trace Semantics is Fully Abstract.

[BibT_eX]

[DOI]

Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

From Philosophical to Industrial Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic and Its Applications, Third Indian Conference, 2009

An Automata-Theoretic Approach to Regular XPath.

[BibT_eX]

[DOI]

Proceedings of the Database Programming Languages, 2009

2008

Multi-Objective Model Checking of Markov Decision Processes.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2008

The Complexity of Enriched Mu-Calculi.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2008

Let us---together---make CACM exciting.

[BibT_eX]

[DOI]

Commun. ACM, 2008

"Where do you come from? and where are you going?".

[BibT_eX]

[DOI]

Commun. ACM, 2008

CACM: past, present, and future.

[BibT_eX]

[DOI]

Commun. ACM, 2008

From Verification to Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2008

From Church and Prior to PSL.

[BibT_eX]

[DOI]

Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Intelligate: Scalable Dynamic Invariant Learning for Power Reduction.

[BibT_eX]

[DOI]

Roni Wiener

Gila Kamhi

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.

[BibT_eX]

[DOI]

Proceedings of the 2008 IEEE International Conference on Robotics and Automation, 2008

Open Implication.

[BibT_eX]

[DOI]

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

Automata-Theoretic Model Checking Revisited.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2008

A Framework for Inherent Vacuity.

[BibT_eX]

[DOI]

Dana Fisman

Sarai Sheinvald-Faragy

Proceedings of the Hardware and Software: Verification and Testing, 2008

A Temporal Language for SystemC.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2008

A Logical Approach to Constraint Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the Complexity of Constraints, 2008

Automata: from logics to algorithms.

[BibT_eX]

Thomas Wilke

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

From Monadic Logic to PSL.

[BibT_eX]

[DOI]

Proceedings of the Pillars of Computer Science, 2008

2007

Finite Model Theory and Its Applications

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

A continuous-discontinuous second-order transition in the satisfiability of random Horn-SAT formulas.

[BibT_eX]

[DOI]

Cristopher Moore

Gabriel Istrate

Demetrios D. Demopoulos

Random Struct. Algorithms, 2007

The Planning Spectrum - One, Two, Three, Infinity.

[BibT_eX]

[DOI]

Marco Pistore

J. Artif. Intell. Res., 2007

GSTE is partitioned model checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2007

Linear-Time Model Checking: Automata Theory in Practice.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2007

Property-Driven Partitioning for Abstraction Refinement.

[BibT_eX]

[DOI]

Roberto Sebastiani

Stefano Tonetta

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

The Büchi Complementation Saga.

[BibT_eX]

[DOI]

Proceedings of the STACS 2007, 2007

Discrete Search Leading Continuous Exploration for Kinodynamic Motion Planning.

[BibT_eX]

[DOI]

Proceedings of the Robotics: Science and Systems III, 2007

Proving that programs eventually do something good.

[BibT_eX]

[DOI]

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Model Checking Buechi Specifications.

[BibT_eX]

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.

[BibT_eX]

[DOI]

Proceedings of the 2007 IEEE International Conference on Robotics and Automation, 2007

Interactive presentation: PowerQuest: trace driven data mining for power optimization.

[BibT_eX]

[DOI]

Pietro Babighian

Gila Kamhi

Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

07441 Abstracts Collection -- Algorithmic-Logical Theory of Infinite Structures.

[BibT_eX]

[DOI]

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

07441 Summary -- Algorithmic-Logical Theory of Infinite Structures.

[BibT_eX]

[DOI]

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

Formal Techniques for SystemC Verification; Position Paper.

[BibT_eX]

[DOI]

Proceedings of the 44th Design Automation Conference, 2007

An Analysis of Slow Convergence in Interval Propagation.

[BibT_eX]

[DOI]

Lucas Bordeaux

Youssef Hamadi

Proceedings of the Principles and Practice of Constraint Programming, 2007

Pushdown Module Checking with Imperfect Information.

[BibT_eX]

[DOI]

Benjamin Aminof

Aniello Murano

Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

Hybrid Systems: From Verification to Falsification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Branching vs. Linear Time: Semantical Perspective.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2007

Deeper Bound in BMC by Combining Constant Propagation and Abstraction.

[BibT_eX]

[DOI]

Proceedings of the 12th Conference on Asia South Pacific Design Automation, 2007

Automata-theoretic techniques for temporal reasoning.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Modal Logic., 2007

2006

Coverage metrics for formal verification.

[BibT_eX]

[DOI]

Hana Chockler

Int. J. Softw. Tools Technol. Transf., 2006

BDD-based decision procedures for the modal logic K.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 2006

Büchi Complementation Made Tighter.

[BibT_eX]

[DOI]

Ehud Friedgut

Int. J. Found. Comput. Sci., 2006

Aggregating disparate estimates of chance.

[BibT_eX]

[DOI]

Daniel N. Osherson

Games Econ. Behav., 2006

Coverage metrics for temporal logic model checking*.

[BibT_eX]

[DOI]

Hana Chockler

Formal Methods Syst. Des., 2006

Relating word and tree automata.

[BibT_eX]

[DOI]

Shmuel Safra

Ann. Pure Appl. Log., 2006

educational response to offshore outsourcing.

[BibT_eX]

[DOI]

Proceedings of the 37th SIGCSE Technical Symposium on Computer Science Education, 2006

Automata theory: its relevance to computer science students and course contents.

[BibT_eX]

[DOI]

Proceedings of the 37th SIGCSE Technical Symposium on Computer Science Education, 2006

On Locally Checkable Properties.

[BibT_eX]

[DOI]

Yoad Lustig

Proceedings of the Logic for Programming, 2006

Fixed-Parameter Hierarchies inside PSPACE.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Memoryful Branching-Time Logic.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

The Complexity of Enriched µ-Calculi.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006

Deterministic Dynamic Monitors for Linear-Time Assertions.

[BibT_eX]

[DOI]

Proceedings of the Formal Approaches to Software Testing and Runtime Verification, 2006

Safraless Compositional Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

The Phase Transition in the Random HornSAT Problem.

[BibT_eX]

Demetrios D. Demopoulos

Proceedings of the Computational Complexity and Statistical Physics., 2006

2005

From linear time to branching time.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2005

From complementation to certification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Decidable containment of recursive queries.

[BibT_eX]

[DOI]

Diego Calvanese

Theor. Comput. Sci., 2005

In memory of Seymour Ginsburg 1928 - 2004.

[BibT_eX]

[DOI]

Daniel J. Rosenkrantz

SIGMOD Rec., 2005

Symbolic Techniques in Satisfiability Solving.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Complementation Constructions for Nondeterministic Automata on Infinite Words.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Experimental Evaluation of Classical Automata Constructions.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

Treewidth in Verification: Local vs. Global.

[BibT_eX]

[DOI]

Andrea Ferrara

Proceedings of the Logic for Programming, 2005

Model Checking for Database Theoreticians.

[BibT_eX]

[DOI]

Proceedings of the Database Theory, 2005

Efficient LTL compilation for SAT-based model checking.

[BibT_eX]

[DOI]

Proceedings of the 2005 International Conference on Computer-Aided Design, 2005

Safraless Decision Procedures.

[BibT_eX]

[DOI]

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

05241 Abstracts Collection - Synthesis and Planning.

[BibT_eX]

[DOI]

Henry A. Kautz

Wolfgang Thomas

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

05241 Executive Summary - Synthesis and Planning.

[BibT_eX]

[DOI]

Henry A. Kautz

Wolfgang Thomas

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

Regular Vacuity.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

Formal Verification of Backward Compatibility of Microcode.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Complete Axiomatizations for Reasoning about Knowledge and Time.

[BibT_eX]

[DOI]

Ron van der Meyden

SIAM J. Comput., 2004

SAT-based Induction for Temporal Safety Properties.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Bounded Model Checking, 2004

A Measured Collapse of the Modal µ-Calculus Alternation Hierarchy.

[BibT_eX]

[DOI]

Doron Bustan

Proceedings of the STACS 2004, 2004

Search vs. Symbolic Techniques in Satisfiability Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2004

Pattern search in hierarchical high-level designs.

[BibT_eX]

[DOI]

Proceedings of the 2004 11th IEEE International Conference on Electronics, 2004

Projection Pushing Revisited.

[BibT_eX]

[DOI]

Proceedings of the Advances in Database Technology, 2004

Symbolic Decision Procedures for QBF.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2004

Constraint Propagation as a Proof System.

[BibT_eX]

[DOI]

Albert Atserias

Proceedings of the Principles and Practice of Constraint Programming, 2004

Global Model-Checking of Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Verifying omega-Regular Properties of Markov Chains.

[BibT_eX]

[DOI]

Doron Bustan

Sasha Rubin

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

From bidirectionality to alternation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Vacuity detection in temporal model checking.

[BibT_eX]

[DOI]

Alfonso San Miguel Aguirre

Int. J. Softw. Tools Technol. Transf., 2003

Reasoning on regular path queries.

[BibT_eX]

[DOI]

SIGMOD Rec., 2003

Random 3-SAT: The Plot Thickens.

[BibT_eX]

[DOI]

Cristian Coarfa

Demetrios D. Demopoulos

Devika Subramanian

Constraints An Int. J., 2003

Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Resets vs. Aborts in Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Query Containment Using Views.

[BibT_eX]

Proceedings of the Eleventh Italian Symposium on Advanced Database Systems, 2003

View-based query containment.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Homomorphism Closed vs. Existential Positive.

[BibT_eX]

[DOI]

Tomás Feder

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Automated Verification: Graphs, Logic, and Automata.

[BibT_eX]

[DOI]

Proceedings of the IJCAI-03, 2003

Logic and Automata: A Match Made in Heaven.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Π2 ∩ Σ2 ≡ AFMC.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

On Complementing Nondeterministic Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Enhanced Vacuity Detection in Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Optimizing a BDD-Based Modal Solver.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

A Call to Regularity.

[BibT_eX]

[DOI]

Proceedings of the PCK50, 2003

Fair Equivalence Relations.

[BibT_eX]

[DOI]

Proceedings of the Verification: Theory and Practice, 2003

In Memoriam: Paris C. Kanellakis.

[BibT_eX]

[DOI]

Alexander A. Shvartsman

Proceedings of the PCK50, 2003

2002

Rewriting of Regular Expressions and Regular Path Queries.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2002

Black Box Checking.

[BibT_eX]

[DOI]

Doron A. Peled

Mihalis Yannakakis

J. Autom. Lang. Comb., 2002

On the Complexity of Verifying Concurrent Transition Systems.

[BibT_eX]

[DOI]

David Harel

Inf. Comput., 2002

First-Order Logic with Two Variables and Unary Temporal Logic.

[BibT_eX]

[DOI]

Kousha Etessami

Thomas Wilke

Inf. Comput., 2002

Bisimulation Minimization and Symbolic Model Checking.

[BibT_eX]

[DOI]

Kathi Fisler

Formal Methods Syst. Des., 2002

Model Checking: A Complexity-Theoretic Perspective (invited talk).

[BibT_eX]

[DOI]

Proceedings of the Parallel and Distributed Model Checking, 2002

A Rice University perspective on software engineering licensing.

[BibT_eX]

[DOI]

Ken Kennedy

Commun. ACM, 2002

The ForSpec Temporal Logic: A New Temporal Property-Specification Language.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Lossless Regular Views.

[BibT_eX]

[DOI]

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

Pushdown Specifications.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

Reasoning about Actions and Planning in LTL Action Theories.

[BibT_eX]

Diego Calvanese

Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), 2002

Eliminating Incoherence from Subjective Estimates of Chance.

[BibT_eX]

Proceedings of the Eights International Conference on Principles and Knowledge Representation and Reasoning (KR-02), 2002

Alternation.

[BibT_eX]

[DOI]

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

Constraint Satisfaction, Bounded Treewidth, and Finite-Variable Logics.

[BibT_eX]

[DOI]

Víctor Dalmau

Proceedings of the Principles and Practice of Constraint Programming, 2002

Model Checking Linear Properties of Prefix-Recognizable Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

BDD-Based Decision Procedures for K.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

The Complexity of the Graded µ-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

2001

Weak alternating automata are not that weak.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2001

Verification by Augmented Abstraction: The Automata-Theoretic View.

[BibT_eX]

[DOI]

Yonit Kesten

Amir Pnueli

J. Comput. Syst. Sci., 2001

Module Checking.

[BibT_eX]

[DOI]

Inf. Comput., 2001

Model Checking of Safety Properties.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

A New Heuristic for Bad Cycle Detection Using BDDs.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

Towards an Efficient Library for SAT: a Manifesto.

[BibT_eX]

[DOI]

Electron. Notes Discret. Math., 2001

On the unusual effectiveness of logic in computer science.

[BibT_eX]

[DOI]

Bull. Symb. Log., 2001

Branching vs. Linear Time: Final Showdown.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Is There a Best Symbolic Cycle-Detection Algorithm?

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Coverage Metrics for Temporal Logic Model Checking.

[BibT_eX]

[DOI]

Hana Chockler

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

On Bounded Specifications.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

Synthesizing Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

On the Complexity of Parity Word Automata.

[BibT_eX]

[DOI]

Valerie King

Alfonso San Miguel Aguirre

Proceedings of the Foundations of Software Science and Computation Structures, 2001

View-Based Query Answering and Query Containment over Semistructured Data.

[BibT_eX]

[DOI]

Proceedings of the Database Programming Languages, 8th International Workshop, 2001

Random 3-SAT and BDDs: The Plot Thickens Further.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2001

Extended Temporal Logic Revisited.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2001, 2001

Benefits of Bounded Model Checking at an Industrial Setting.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

A Practical Approach to Coverage in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

The Hybrid µ-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

An automata-theortetic approach to modular model checking.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2000

Conjunctive-Query Containment and Constraint Satisfaction.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2000

An automata-theoretic approach to branching-time model checking.

[BibT_eX]

[DOI]

J. ACM, 2000

Constraint Satisfaction and Database Theory: a Tutorial.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2000

µ-Calculus Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

0-1 Laws for Fragments of Existential Second-Order Logic: A Survey.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

View-Based Query Processing and Constraint Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

What is View-Based Query Rewriting?

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Knowledge Representation meets Databases (KRDB 2000), 2000

Containment of Conjunctive Regular Path Queries with Inverse.

[BibT_eX]

Proceedings of the KR 2000, 2000

Answering Regular Path Queries Using Views.

[BibT_eX]

[DOI]

Proceedings of the 16th International Conference on Data Engineering, San Diego, California, USA, February 28, 2000

Automated Verification = Graphs, Automata, and Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2000

Open Systems in Reactive Environments: Control and Synthesis.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2000, 2000

What is Query Rewriting?

[BibT_eX]

[DOI]

Proceedings of the Cooperative Information Agents IV, 2000

An Automata-Theoretic Approach to Reasoning about Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

A Game-Theoretic Approach to Constraint Satisfaction.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

SIGMOD Rec., 1999

The hierarchical approach to modeling knowledge and common knowledge.

[BibT_eX]

[DOI]

Int. J. Game Theory, 1999

Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Symbolic Model Checking, 1999

The Complexity of Problems on Graphs Represented as OBDDs.

[BibT_eX]

[DOI]

Chic. J. Theor. Comput. Sci., 1999

Church's problem revisited.

[BibT_eX]

[DOI]

Bull. Symb. Log., 1999

Common Knowledge Revisited.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1999

Query Answering Using Views for Data Integration over the Web.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGMOD Workshop on The Web and Databases, 1999

The Weakness of Self-Complementation.

[BibT_eX]

[DOI]

Proceedings of the STACS 99, 1999

Rewriting of Regular Path Queries.

[BibT_eX]

Proceedings of the Atti del Settimo Convegno Nazionale Sistemi Evoluti per Basi di Dati, 1999

Automata-Theoretic Approach to Planning for Temporally Extended Goals.

[BibT_eX]

[DOI]

Proceedings of the Recent Advances in AI Planning, 5th European Conference on Planning, 1999

Strong Cyclic Planning Revisited.

[BibT_eX]

[DOI]

Marco Daniele

Paolo Traverso

Proceedings of the Recent Advances in AI Planning, 5th European Conference on Planning, 1999

Robust Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '99: Concurrency Theory, 1999

Bisimulation and Model Checking.

[BibT_eX]

[DOI]

Kathi Fisler

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Improved Automata Generation for Linear Temporal Logic.

[BibT_eX]

[DOI]

Marco Daniele

Fausto Giunchiglia

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Tomás Feder

SIAM J. Comput., 1998

Computational Model Theory: An Overview.

[BibT_eX]

[DOI]

Log. J. IGPL, 1998

Verification of Fair Transition Systems.

[BibT_eX]

[DOI]

Chic. J. Theor. Comput. Sci., 1998

Weak Alternating Automata and Tree Automata Emptiness.

[BibT_eX]

[DOI]

Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, 1998

Complexity of Problems on Graphs Represented as OBDDs (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the STACS 98, 1998

Panel: logic in the computer science curriculum.

[BibT_eX]

[DOI]

Proceedings of the 29th SIGCSE Technical Symposium on Computer Science Education, 1998

Relating linear and branching model checking.

[BibT_eX]

Proceedings of the Programming Concepts and Methods, 1998

Linear vs. Branching Time: A Complexity-Theoretic Perspective.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Reasoning about The Past with Two-Way Automata.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Bisimulation Minimization in an Automata-Theoretic Verification Framework.

[BibT_eX]

[DOI]

Kathi Fisler

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Sometimes and Not Never Re-revisited: On Branching Versus Linear Time.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '98: Concurrency Theory, 1998

Synthesis from Knowledge-Based Specifications (Extended Abstract).

[BibT_eX]

[DOI]

Ron van der Meyden

Proceedings of the CONCUR '98: Concurrency Theory, 1998

Alternating Refinement Relations.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '98: Concurrency Theory, 1998

1997

Reasoning about Knowledge: A Response by the Authors.

[BibT_eX]

[DOI]

Minds Mach., 1997

Special Selection in Logic in Computer Science.

[BibT_eX]

[DOI]

J. Symb. Log., 1997

On the Equivalence of Recursive and Nonrecursive Datalog Programs.

[BibT_eX]

[DOI]

Surajit Chaudhuri

J. Comput. Syst. Sci., 1997

Fixpoint logics, relational machines, and computational complexity.

[BibT_eX]

[DOI]

Victor Vianu

J. ACM, 1997

Knowledge-Based Programs.

[BibT_eX]

[DOI]

Distributed Comput., 1997

On the decision problem for two-variable first-order logic.

[BibT_eX]

[DOI]

Erich Grädel

Bull. Symb. Log., 1997

Verification of Open Systems.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1997

Modular Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

Module Checking Revisited.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Model Checking and Transitive-Closure Logic.

[BibT_eX]

[DOI]

Neil Immerman

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1997

1996

In Memoriam: Paris C. Kanellakis (1953-1995).

[BibT_eX]

[DOI]

Inf. Comput., 1996

In Memoriam Paris C. Kanellakis.

[BibT_eX]

[DOI]

Harry G. Mairson

Alexander A. Shvartsman

ACM Comput. Surv., 1996

Rank Predicates vs. Progress Measures in Concurrent-Program Verification.

[BibT_eX]

[DOI]

Chic. J. Theor. Comput. Sci., 1996

Implementing Knowledge-Based Programs.

[BibT_eX]

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

In Memoriam: Paris C. Kanellakis.

[BibT_eX]

[DOI]

Christos H. Papadimitriou

Proceedings of the Fifteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1996

On the Expressive Power of Variable-Confined Logics.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1996

Database Research: Lead, Follow, or Get Out of the Way? - Panel Abstract.

[BibT_eX]

Proceedings of the Twelfth International Conference on Data Engineering, February 26, 1996

Why is Modal Logic So Robustly Decidable?

[BibT_eX]

[DOI]

Proceedings of the Descriptive Complexity and Finite Models, 1996

A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking.

[BibT_eX]

[DOI]

Thomas A. Henzinger

Proceedings of the CONCUR '96, 1996

Verification of Fair Transisiton Systems.

[BibT_eX]

[DOI]

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

Module Checking.

[BibT_eX]

[DOI]

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

1995

On Monadic NP vs. Monadic co-NP

[BibT_eX]

[DOI]

Larry J. Stockmeyer

Inf. Comput., July, 1995

Computing with Infinitary Logic.

[BibT_eX]

[DOI]

Victor Vianu

Theor. Comput. Sci., 1995

Undecidable Boundedness Problems for Datalog Programs.

[BibT_eX]

[DOI]

J. Log. Program., 1995

On the Expressive Power of Datalog: Tools and a Case Study.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1995

A Nonstandard Approach to the Logical Omniscience Problem.

[BibT_eX]

[DOI]

Artif. Intell., 1995

Simple on-the-fly automatic verification of linear temporal logic.

[BibT_eX]

Proceedings of the Protocol Specification, 1995

On the Complexity of Bounded-Variable Queries.

[BibT_eX]

[DOI]

Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1995

On the Complexity of Modular Model Checking

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1995

On the Complexity of Branching Modular Model Checking (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the CONCUR '95: Concurrency Theory, 1995

An Automata-Theoretic Approach to Fair Realizability and Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 1995

An Automata-Theoretic Approach to Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Logics for Concurrency, 1995

Alternating Automata and Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Today: Recent Trends and Developments, 1995

Reasoning About Knowledge.

[BibT_eX]

[DOI]

MIT Press, ISBN: 9780262562003, 1995

1994

Reasoning About Infinite Computations

[BibT_eX]

[DOI]

Inf. Comput., November, 1994

Algorithmic Knowledge.

[BibT_eX]

Yoram Moses

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

Nontraditional Applications of Automata Theory.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computer Software, 1994

On the Complexity of Equivalence between Recursive and Nonrecursive Datalog Programs.

[BibT_eX]

[DOI]

Surajit Chaudhuri

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).

[BibT_eX]

[DOI]

Orna Bernholtz

Proceedings of the Computer Aided Verification, 6th International Conference, 1994

An Operational Semantics for Knowledge Bases.

[BibT_eX]

[DOI]

Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31, 1994

1993

The Logical Data Model.

[BibT_eX]

[DOI]

ACM Trans. Database Syst., 1993

On the Complexity of Queries in the Logical Data Model.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1993

Logical Query Optimization by Proff-Tree Transformation.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1993

Undecidable Optimization Problems for Database Logic Programs.

[BibT_eX]

[DOI]

J. ACM, 1993

Monotone monadic SNP and constraint satisfaction.

[BibT_eX]

[DOI]

Tomás Feder

Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, 1993

Parametric real-time reasoning.

[BibT_eX]

[DOI]

Rajeev Alur

Thomas A. Henzinger

Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, 1993

Optimization of Real Conjunctive Queries.

[BibT_eX]

[DOI]

Surajit Chaudhuri

Proceedings of the Twelfth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1993

The Complexity of Set Constraints.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 7th Workshop, 1993

On Monadic NP vs. Monadic co-NP (Extended Abstract).

[BibT_eX]

[DOI]

Larry J. Stockmeyer

Proceedings of the Eigth Annual Structure in Complexity Theory Conference, 1993

1992

Infinitary Logics and 0-1 Laws

[BibT_eX]

[DOI]

Inf. Comput., June, 1992

What Is an Inference Rule?

[BibT_eX]

[DOI]

J. Symb. Log., 1992

What Can Machines Know? On the Properties of Knowledge in Distributed Systems.

[BibT_eX]

[DOI]

J. ACM, 1992

Memory-Efficient Algorithms for the Verification of Temporal Properties.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1992

The Expressive Power of the Kierarchical Approach to Modeling Knowledge and Common Knowledge.

[BibT_eX]

Proceedings of the 4th Conference on Theoretical Aspects of Reasoning about Knowledge, 1992

Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory

[BibT_eX]

[DOI]

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

Infinitary Logic for Computer Science.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Automata Theory for Database Theoreticans.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Studies in Computer Science, 1992

1991

Database Logic Programming.

[BibT_eX]

[DOI]

J. Log. Program., 1991

A Model-Theoretic Analysis of Knowledge.

[BibT_eX]

[DOI]

J. ACM, 1991

Verification of Concurrent Programs: The Automata-Theoretic Framework.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1991

Tools for Datalog Boundedness.

[BibT_eX]

[DOI]

Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1991

Logic Programs as Types for Logic Programs

[BibT_eX]

[DOI]

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

Model Checking vs. Theorem Proving: A Manifesto.

[BibT_eX]

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

[BibT_eX]

[DOI]

Stavros S. Cosmadakis

Paris C. Kanellakis

J. ACM, January, 1990

Endmarkers can Make a Difference.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1990

0-1 Laws and Decision Problems for Fragments of Second-Order Logic

[BibT_eX]

[DOI]

Inf. Comput., 1990

0-1 Laws for Infinitary Logics (Preliminary Report)

[BibT_eX]

[DOI]

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)

[BibT_eX]

[DOI]

David Harel

Roni Rosner

Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

Global Optimization Problems for Database Logic Programs.

[BibT_eX]

Proceedings of the Logic Programming, 1990

1989

The Complexity of Reasoning about Knowledge and Time. I. Lower Bounds.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1989

A Note on the Reduction of Two-Way Automata to One-Way Automata.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1989

On omega-Automata and Temporal Logic (Preliminary Report)

[BibT_eX]

[DOI]

Shmuel Safra

Proceedings of the 21st Annual ACM Symposium on Theory of Computing, 1989

Safety of Datalog Queries over Infinite Databases.

[BibT_eX]

[DOI]

Yehoshua Sagiv

Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1989

Proof-Tree Transformation Theorems and Their Applications.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1989

On the Complexity of Epistemic Reasoning

[BibT_eX]

[DOI]

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

1988

Response to a Letter to the Editor.

[BibT_eX]

IEEE Softw., 1988

The Universal-Relation Data Model for Logical Independence.

[BibT_eX]

[DOI]

IEEE Softw., 1988

Reasoning about Knowledge and Time in Asynchronous Systems

[BibT_eX]

[DOI]

Proceedings of the 20th Annual ACM Symposium on Theory of Computing, 1988

Decidable Optimization Problems for Database Logic Programs (Preliminary Report)

[BibT_eX]

[DOI]

Stavros S. Cosmadakis

Haim Gaifman

Paris C. Kanellakis

Proceedings of the 20th Annual ACM Symposium on Theory of Computing, 1988

Database Logic Programming, Deductive Databases, and Expert Database Systems.

[BibT_eX]

Proceedings of the 1988 ACM SIGMOD International Conference on Management of Data, 1988

A Temporal Fixpoint Calculus.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Seventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1988

The Complexity of Ordering Subgoals.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

Proceedings of the ICDT'88, 2nd International Conference on Database Theory, Bruges, Belgium, August 31, 1988

An Automata-Theoretic Approach to Protocol Verification (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Concurrency 88: International Conference on Concurrency, 1988

1987

The Complementation Problem for Büchi Automata with Appplications to Temporal Logic.

[BibT_eX]

[DOI]

A. Prasad Sistla

Theor. Comput. Sci., 1987

Unified Verification Theory.

[BibT_eX]

[DOI]

Proceedings of the Temporal Logic in Specification, 1987

The Decision Problem for the Probabilities of Higher-Order Properties

[BibT_eX]

[DOI]

Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987

1986

Automata-Theoretic Techniques for Modal Logics of Programs.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1986

Querying Logical Databases.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1986

Notions of dependency satisfaction.

[BibT_eX]

[DOI]

Marc H. Graham

Alberto O. Mendelzon

J. ACM, 1986

On the Expressive Power of Data Dependencies.

[BibT_eX]

[DOI]

Johann A. Makowsky

Acta Informatica, 1986

Updating Logical Databases.

[BibT_eX]

Adv. Comput. Res., 1986

On Epistemic Logic and Logical Omniscience.

[BibT_eX]

Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, 1986

Knowledge and Implicit Knowledge in a Distributed Environment: Preliminary Report.

[BibT_eX]

Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, 1986

The Complexity of Reasoning about Knowledge and Time: Extended Abstract

[BibT_eX]

[DOI]

Proceedings of the 18th Annual ACM Symposium on Theory of Computing, 1986

Reasoning about Fair Concurrent Programs

[BibT_eX]

[DOI]

Costas Courcoubetis

Proceedings of the 18th Annual ACM Symposium on Theory of Computing, 1986

On the Integrity of Databases with Incomplete Information.

[BibT_eX]

[DOI]

Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1986

An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

[BibT_eX]

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

What Can Machines Know? On the Epistemic Properties of Machines.

[BibT_eX]

[DOI]

Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986

1985

Formal Systems for Join Dependencies.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1985

The Implication Problem for Functional and Inclusion Dependencies is Undecidable.

[BibT_eX]

[DOI]

Ashok K. Chandra

SIAM J. Comput., 1985

A responce to "A complete axiomatisation for full join dependencies in relations".

[BibT_eX]

Bull. EATCS, 1985

A simple proof that connectivity of finite graphs is not first-order definable.

[BibT_eX]

Haim Gaifman

Bull. EATCS, 1985

Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report

[BibT_eX]

[DOI]

Larry J. Stockmeyer

Proceedings of the 17th Annual ACM Symposium on Theory of Computing, 1985

An Internal Semantics for Modal Logic: Preliminary Report

[BibT_eX]

[DOI]

Proceedings of the 17th Annual ACM Symposium on Theory of Computing, 1985

On the Expressive Power of the Logical Data Model (Preliminary Report).

[BibT_eX]

[DOI]

Proceedings of the 1985 ACM SIGMOD International Conference on Management of Data, 1985

The Taming of Converse: Reasoning about Two-way Computations.

[BibT_eX]

[DOI]

Proceedings of the Logics of Programs, 1985

A Model-Theoretic Analysis of Monotonic Knowledge.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

A. Prasad Sistla

Proceedings of the Automata, 1985

Automatic Verification of Probabilistic Concurrent Finite-State Programs

[BibT_eX]

[DOI]

Proceedings of the 26th Annual Symposium on Foundations of Computer Science, 1985

1984

On Acyclic Database Decompositions

[BibT_eX]

[DOI]

Inf. Control., May, 1984

On the Foundations of the Universal Relation Model.

[BibT_eX]

[DOI]

David Maier

ACM Trans. Database Syst., 1984

Formal Systems for Tuple and Equality Generating Dependencies.

[BibT_eX]

[DOI]

SIAM J. Comput., 1984

The Implication and Finite Implication Problems for Typed Template Dependencies.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1984

A Proof Procedure for Data Dependencies.

[BibT_eX]

[DOI]

J. ACM, 1984

A Note on Lossless Database Decompositions.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1984

Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract)

[BibT_eX]

[DOI]

Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984

A New Approach to Database Logic.

[BibT_eX]

[DOI]

Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1984

On the Equivalence of Logical Databases.

[BibT_eX]

[DOI]

Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1984

On the Complexity and Axiomatizability of Consistent Database States.

[BibT_eX]

[DOI]

Marc H. Graham

Proceedings of the Third ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1984

The Theory of Data Dependencies - An Overview.

[BibT_eX]

[DOI]

Proceedings of the Automata, 1984

A Model-Theoretic Analysis of Knowledge: Preliminary Report

[BibT_eX]

[DOI]

Proceedings of the 25th Annual Symposium on Foundations of Computer Science, 1984

1983

Armstrong Databases for Functional and Inclusion Dependencies.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1983

Inferring Multivalued Dependencies From Functional and Join Dependencies.

[BibT_eX]

[DOI]

Acta Informatica, 1983

Second-Order Dependency Theory.

[BibT_eX]

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)

[BibT_eX]

[DOI]

Paris C. Kanellakis

Stavros S. Cosmadakis

Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 1983

The Revenge of the JD.

[BibT_eX]

[DOI]

David Maier

Proceedings of the Second ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1983

On the Semantics of Updates in Databases.

[BibT_eX]

[DOI]

Proceedings of the Second ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, 1983

Yet Another Process Logic (Preliminary Version).

[BibT_eX]

[DOI]

Proceedings of the Logics of Programs, 1983

Reasoning about Infinite Computation Paths (Extended Abstract)

[BibT_eX]

[DOI]

A. Prasad Sistla

Proceedings of the 24th Annual Symposium on Foundations of Computer Science, 1983

1982

The Complexity of Relational Query Languages (Extended Abstract)

[BibT_eX]

[DOI]

Proceedings of the 14th Annual ACM Symposium on Theory of Computing, 1982

On Decomposition of Relational Databases

[BibT_eX]

[DOI]

Proceedings of the 23rd Annual Symposium on Foundations of Computer Science, 1982

1981

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

[BibT_eX]

[DOI]

PhD thesis, 1981

A Note on Decompositions of Relational Databases.

[BibT_eX]

[DOI]

SIGMOD Rec., 1981

The Decision Problem for Database Dependencies.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1981

The Implication Problem for Data Dependencies.

[BibT_eX]

[DOI]

Proceedings of the Automata, 1981

Global Decision Problems for Relational Databases

[BibT_eX]

[DOI]

Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, 1981

1980

Decision Problems for Data Dependencies.

[BibT_eX]

Proceedings of the XP1 Workshop on Relational Database Theory, 30 June, 1980

1979

On the Properties of Join Dependencies.

[BibT_eX]