More complete lists of publications can be found on individual members' web pages.

Automata-Theoretic Verification and Model Checking

• Verification by Augmented Abstraction: The Automata-Theoretic View (Full version of CSL'99 paper with Y. Kesten and A. Pnueli).

• The Complexity of Problems on Graphs Represented as OBDDs (with J. Feigenbaum, S. Kannan, and Mahesh Viswanathan, published in the Chicago J. of Theoretical Computer Science).

• Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting (SMC'99 paper with L. Fix, R. Fraer, and G. Kamhi).

• Model Checking of Safety Properties (Full version of CAV'99 paper with O. Kupferman).

• Automata-Theoretic Approach to Planning for Temporally Extended Goals (ECP'99 paper with G. De Giacomo).

• Bisimulation and Model Checking (CHARME'99 paper with K. Fisler).

• Vacuity Detection in Temporal Model Checking (CHARME'99 paper with O. Kupferman).

• Black Box Checking (PSTV'99 paper with D. Peled and M. Yannakakis).

• Robust Satisfaction (CONCUR'99 paper with O. Kupferman).

• Model Checking of Safety Properties (CAV'99 paper with O. Kupferman).

• Improved Automata Generation for Linear Temporal Logic (CAV'99 paper with M. Daniele and F. Giunchiglia).

• Rewriting of regular expressions and regular path queries (PODS'99 paper with D. Calvanese, G. DeGiacomo, and M. Lenzerini).

• Probabilistic linear-time model checking: an overview of the automata-theoretic approach (invited ARTS'99 paper).

• The Weakness of Self-Complementation (STACS'99 paper with O. Kupferman).

• Bisimulation Minimization in an Automata-Theoretic Verification Framework (K. Fisler and M.Y. Vardi, FMCAD'98 paper).

• Sometimes and Not Never Re-revisited: On Branching Versus Linear Time (M.Y.Vardi; CONCUR'98 invited paper).

• An Automata-Theoretic Approach to Branching-Time Model Checking (full version of CAV'94 paper by M.Y.Vardi, O. Kupferman and P. Wolper).

• Conjunctive-query containment and constraint satisfaction (M.Y.Vardi and P. Kolaitis; PODS'98 paper).

• Linear vs. Branching Time: A Complexity-Theoretic Perspective (M.Y.Vardi; invited LICS'98 paper).

• Freedom, Weakness, and Determinism: From Linear-time to Branching-time (M.Y.Vardi and O. Kupferman; LICS'98 paper).

• Computational Model Theory: an Overview (M.Y.Vardi; WOLLIC'97 paper)

• Complexity of Problems on Graphs Represented as OBDDs (J. Feigenbaum, S. Kannan, M.Y.Vardi, and M. Viswanathan; STACS'98 paper).

• Modular Model Checking (M.Y.Vardi and O. Kupferman; COMPOS'97 paper).

• Verification of Fair Transition Systems (M.Y.Vardi and O. Kupferman; published in the Chicago J. of Theoretical Computer Science).

• Weak Alternating Automata and Tree Automata Emptiness (M.Y.Vardi and O. Kupferman; STOC'98 paper).

• Logic in The Computer Science Curriculum (SIGCSE'98 panel with K. Bruce, P. Kolaitis, D. Leivant and M.Y. Vardi).

• Relating Linear and Branching Model Checking (M.Y.Vardi and O. Kupferman; PROCOMET'98 paper).

Other Verification Issues

• Modelling and Model Checking a Shared Memory Consistency Protocol.(K. Fisler and C. Girault. International Conference on Applications and Theory of Petri Nets, 1998).

Diagrams and Hardware Verification

• Timing Diagrams: Formalization and Algorithmic Verification. (K. Fisler, Journal of Logic, Language, and Information. Spring 1999).

• Containment of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. (K. Fisler, CAV '97, June 1997).