Rice
FIS

FIS image header
  •  
  •  
  •  
  •  
  •  
Download 
Scholarly Interest Report
         
Moshe Y. Vardi
Professor
Karen Ostrum George Professor of Computational Engineering and Professor of Computer Science
 
e-mail:vardi@rice.edu
 
  • B.S. (1974) Bar-Ilan University
  • M.S. (1980) Feinberg Graduate School of the Weizmann Institute of Science
  • Ph.D. (1981) The Hebrew University of Jerusalem
 
Primary Department
   Department of Computer Science
Picture
 
Department Affiliations
 
  • Ken Kennedy Institute for Information Technology
  •  
     
    Research Areas
     Applications of logic to computer science: database systems, complexity theory, multi-agent systems, and specification and verification of hardware and software
     

    Research Statement

     

    In database theory, Professor Vardi's focus is on optimization of rule-based queries with an aim of delineating between decidable and undecidable optimization problems and developing techniques for automated optimization. Finite-model theory is the study of the logical properties of finite mathematical structures. He is exploring its connections to several areas of computer science, such as complexity theory and database theory. In knowledge theory, he is developing a theory of knowledge-based agents, i.e., agents that act on the basis of their knowledge. This theory has applications to the design and analysis of multiagent systems, such as distributed computer systems or teams of cooperating robots. In program specification and verification, he is studying techniques for automated verification of finite-state programs, i.e., programs whose state space is finite. His recent focus is on modular verification of such programs, which has applications to the design of control-intensive hardware and software, e.g., communication protocols.

     
    Teaching Areas
     Logic in Computer Science, Automated Program Verification, Databases
     
    Selected Publications
     Refereed articles
     

    Lustig, Y., Nain, S., Vardi, M.Y. "Synthesis from Probabilistic Components". Logic Methods in Computer Science 10(2:17), pp. 1–24, 2014 (special issue for the 2011 Conference on Computer Science Logic).."  (2014) : 1-24.

     
     

    Murano, A., Mogavero, F., Perelli, G., Vardi, M.Y "Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions on Computational Logic 15(4)."  (2014) : 1–49.

     
     

    Tsai, M.H., Fogarty, S., Vardi, M.Y. "State of B¨uchi complementation. Logical Methods in Computer Science ."  (2014) : 1–27.

     
     

    Plaku, E., Kavraki, L.E., Vardi, M.Y.: Motion Planning With Dynamics by a
    Synergistic Combination of layers of Planning, IEEE Trans. Robotics, 26:3(2010),
    pp. 469–482

     
     

    Rozier, K.Y., Vardi, M.Y.: LTL Satisfiability Checking. Int’l J. on Software Tools
    for Technology Transfer, 12:2(2010), pp. 123–137. (special issue for 14th Workshop
    on Model Checking Software)

     
     

    Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal
    Methods in Systems Design 34:2(2009), pp. 83–103 (special issue for 19th International
    Conference on Computer Aided Verification)

     
     

    Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification
    by combining motion planning and discrete search. Formal Methods in
    Systems Design 34:2(2009), pp. 157–182 (special issue for 19th International Conference
    on Computer-Aided Verification)

     
     

    Wiener, R., Kamhi, G., Vardi, M.Y.: Intelligate: an algorithm for learning Boolean
    functions for dynamic power reduction. J. Low Power Electronics 5(2009), pp. 106–
    112. (special issue for Proc. 18th Int’l Workshop on Integrated Circuit and System
    Design, Power and Timing Modeling, Optimization and Simulation)

     
     

    Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y. "The Complexity of Enriched Mu-Calculi." Logical Methods in Computer Science, 4:3:11 (2008) : 1-27.

     
     

    Etessami, K., Kwiatkowska, M., Vardi, M.Y., and Yannakakis, M. "Multi-objective Model Checking of Markov Decision Processes." Logical Methods in Computer Science, 4(4:8) (2008) : 121.

     
     

    Calvenese, D., De Giacomo, G., Lenzerini, M., Vardi, M.Y. "View-based query processing - on the relationship between rewriting, answering and losslessness." Theoretical Computer Science, 371 (2007) : 169-182.

     
     

    D. Demopoulos, M. Y. Vardi "The Phase Transition in the Eandom HornSAT Problem." Computational Complexity and Statistical Physics (2006) : 169-208.

     
     

    D. Osherson, M. Y. Vardi "Aggregating Desparate Estimated of Chance." Games and Economic Behavior, 56:1 (2006) : 148-173.

     
     

    G. Pan, U. Sattler, M.Y. Vardi "BDD-based Decision Procedures for the Modal Logic." K.J. of Applied Non-Classical Logics, 16:1-2 (2006) : 169-208.

     
     

    H. Chockler, O. Kuferman, M. U. Vardi "Coverage Metrics for Formal Verification." J. on Software Tools for Technology Transfer, 8:4-5 (2006) : 373-386.

     
     

    H. Chockler, O. Kupferman, M. Y. Vardi "Coverage Metrics for Temporal Logic Model Checking." Formal Methods in System Design, 28 (2006) : 189-212.

     
     

    O. Kupferman, S. Safra, M. Y. Vardi "Relating Word and Tree Automata." Annals of Pure and Applied Logic, 138 (2006) : 126-146.

     
     

    J.Y. Halpern, R. van der Meyden, and M.Y. Vardi "Complete Axiomatizations for Reasoning about Knowledge and Time." SIAM Journal on Computing, 33 (2004) : 674-703.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "Rewriting of Regular Expressions and Regular Path Queries." Journal of Computer and System Sciences, 64 (2002) : 443-465.

     
     

    D. Harel, O. Kupferman, and M.Y. Vardi "On the Complexity of Verifying Concurrent Transition Systems." Information and Computation, 173 (2002) : 143-161.

     
     

    Doron Peled, Mihalis Yannakakis, M.Y. Vardi "Black Box Checking." Journal of Automata, Languages and Combinatorics, 7(2) (2002) : 225-246.

     
     

    K. Etessami, T. Wilke, M.Y. Vardi "First-order Logic with Two Variables and Unary Temporal Logic." Information and Computation, 179 (2002) : 279-295.

     
     

    K. Fisler and M.Y. Vardi "Bisimulation Minimization and Symbolic Model Checking." Formal Methods in System Design, 21 (2002) : 39-78.

     
     

    R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, R. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, and Y. Zbar "The ForSpec Temporal Logic - A New Temporal Property-Specification Language." Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2280 (2002) : 296-311.

     
     Articles
     

    Abarbanel, Y., Singerman, E., Vardi, M.Y "Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions. Proc. 51st Design Automation Conference."  (2014) : 1–4.

     
     

    Vardi, M.Y "From L¨owenheim to PSL and SVA. In Language, Culture, Computation, Lecture Notes in Computer Science 8001."  (2014) : 78-102.

     
     

    Aminoff, B., Murano, A., Vardi, M.Y.: Pushdown module checking with imperfect information. Information and Computation 223(2013), pp. 1-17

     
     

    Calvanese, D., De Giacomo, G., Lenzerini, M., Vardi, M.Y.: Simplifying schema mappings. J. Computer and System Sciences 79:6(2013), pp. 816–834 (special issue on Foundations of Data Management).

     
     

    Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying Buchi Complementation Constructions. Logical Methods in Computer Science 9(1), pp. 1-25, 2013 special issue for the 20th Annual Conference on Computer Science Logic).

     
     

    Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. Int'l J. on Software Tools for Technology Transfer 15(5-6), pp. 603-618, 2013 (special issue on Algorithmic Program Synthesis).

     
     

    Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. Int'l J. on Software Tools for Technology Transfer 15(4), pp. 305-320, 2013 (special issue for 15th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems).

     
     

    Cook, B., Koskinen,  E. , Vardi, M.Y.: Temporal property verification  as a program analysis  task.   Formal Methods in System  Design 41:1(2012) , 66-82.  (special issue for 23rd Int'l Conf. on Computer-Aided Verification)

     
     

    Fogarty,  S.,  Vardi,  M.Y.:  Biichi  complementation and size-change termination. Logical Methods  in Computer Science 8(1:13), pp. 1-33, 2012

     
     

    Kupferman, 0., Pnueli,  A., Vardi, M.Y.:  Once and  for all.  JCSS 78:3(2012), 981-996. (special issue in commemoration of Amir Pnueli)

     
     

    Tabakov, D.,  Rozier , K.R., Vardi,  M.Y.:  Optimized  temporal   monitors  for SystemC.  Formal Methods in System  Design 41(3),  pp. 236-268, 2012.

     
     

    Bhatia, A., Maly, M.R., Kavraki, L.E., Vardi, M.Y.: Motion planning with complex goals.  IEEE Robotics and Automation Magazine pp. 55-64, 2011.

     
     

    Bordeauz, L., Katisrelos, G., Narodytska, N., Vardi, M.Y.: The Complexity of Integer Bound Propagation. J. Artificial Intelligence Research 40(2011), pp. 657-676

     
     

    Kreiker, J., Tarlecki, A., Vardi, M.Y., Wilhelm, R.,: Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010, Dagstuhl Manifestos 1:1001 (2011), pp. 21-40, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatic,

     
     

    Sebastiani, R., Tonetta, S., Vardi M.Y.: Symbolic systems, explicit properties-on hybrid approaches for LTL symbolic model checking.  Int'l J. on Software Tools for Technology Transfer 13:4 (2011), pp. 319-0335.

     
     

    Bhatia, A., Kavraki, L.E., Vardi, M.Y.: Motion planning with hybrid dynamics and
    temporal goals. Proc. 49th IEEE Conference on Decision and Control, pp. 1108–
    1115, 2010

     
     

    Bhatia, A., Kavraki, L.E., Vardi, M.Y.: Sampling-based motion planning with
    temporal goals. Proc. IEEE Int’l Conf. on Robotics and Automation, pp. 2689–
    2696, 2010

     
     

    Calvanese C., De Giacomo, G., Lenzerini, M., Vardi, M.Y.: Node selection query
    languages for trees. Proc. 24th AAAI Conf. on Artificial Intelligence, pp. 279–284,
    2010

     
     

    Fogarty, S., Vardi, M.Y.: B¨uchi Complementation and Size-Change Termination.
    Proc. 15th Int’l Conf. on Tools and Algorithms for the Construction and Analysis
    of Systems (TACAS’09) Lecture Notes in Computer Science 5505, Springer, pp. 16-
    30, 2009

     
     

    Kupferman, O., Vardi, M.Y.: Synthesis of trigger properties. Proc. 16th Int’l
    Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture
    Notes in Artificial Intelligence 6355, Springer, pp. 312-331, 2010

     
     

    Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning About Strategies. Proc. 30th
    Int’l Conf. on Foundations of Software Technology and Theoretical Computer Science,
    Leibniz International Proceedings in Informatics 8, Schloss Dagstuhl, pp. 133–
    144, 2010

     
     

    Mogavero, F., Murano, A., Vardi, M.Y.: Relentful Strategic Reasoning in Alternating-
    Time Temporal Logic. Proc. 16th Int’l Conf. on Logic for Programming, Artificial
    Intelligence, and Reasoning, Lecture Notes in Artificial Intelligence 6355, Springer,
    pp. 371-386, 2010

     
     

    Tabakov, D., Vardi, M.Y.: Monitoring temporal SystemC properties. Proc. 8th
    ACM/IEEE Int’l Conf. on Formal Methods and Models for Codesign, 2010, pp. 123–
    132

     
     

    Tabakov, D., Vardi, M.Y.: Optimized temporal monitors for SystemC. Proc. 1st
    Int’l Conf. on Runtime Verification, Lecture Notes in Computer Science 6418,
    Springer, pp. 436–451, 2010

     
     

    Calvanese, D., De Giacomo, G., Lenzerini, M., Vardi, M.Y.: An Automata-Theoretic
    Approach to Regular XPath. Proc. 12t Int’l Symp. on Database Programming
    Language. Springer-Verlag, Lecture Notes in Computer Science 5708, pp. 18–35,
    2009

     
     

    Fogarty, S., Vardi, M.Y.: Efficient B¨uchi universality checking. Proc. 16th Int’l
    Conf. on Tools and Algorithms for the Construction and Analysis of Systems
    (TACAS’10) Lecture Notes in Computer Science 6015, Springer, pp. 205–220, 2010

     
     

    Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. Proc. 12th Int’l Conf.
    on Foundations of Software Science and Computation Structures (F. Honsell and
    M. Miculan, eds.), Springer-Verlag, Lecture Notes in Computer Science 5504, 2009,
    pp. 395–409

     
     

    Nain, S., Vardi, M.Y.: Trace semantics is fully abstract. Proc. 24th IEEE Symp. on
    Logic in Computer Science, 2009, pp. 59–68

     
     

    Wiener, R., Kamhi, G., Vardi, M.Y.: Intelligate– scalable dynamic invariant learning
    for power reduction. Proc. 18th Int’l Workshop on Integrated Circuit and
    System Design, Power and Timing Modeling, Optimization and Simulation (PATMOS’
    08), Lecture Notes in Computer Science 5349, 52–61, 2009

     
     

    Pistore, M., and Vardi, M.Y. "The Planning Spectrum - One, Two, Three, Infinity." J. AI Research, 30 (2007) : 101-132.

     
     

    Sebastiani, R., Singerman, E., Tonetta, S., Vardi, M.Y. "GSTE Is Partitioned Model Checking." Formal Methods in System Design, 31 (2007) : 177-196.

     
     

    Vardi, M.Y., Wilke, T. "Automata - from logic to algorithms." Logic and Automata - History and Perspectives (2007)

     
     

    Calvanese, D., De Giacomo, G., Vardi, M. "Decidable contamment of recursive Queries.." Theoretical Computer Science, v 336 (May 2005) : pp 33-56.

     
     

    Kupferman, O., Vardi, M.Y. "From linear time to branching time." ACM Trans. Comput. Log, v 6 (2005) : pp 273-294.

     
     Books
     

    Gradel, E., Kolaitis, P.K., Libkin, L., Marx, M., Spencer, J., Vardi, M.Y., Venema, Y., Weinstein, S. "Finite Model Theory and Its Applications."  (2007)

     
     Refereed conference papers
     

    Barcelo, P., Romero, M., Vardi, M.Y. "Does query evaluation tractability help query containment? Proc. 33rd ACM Symposium on Principles of Database Systems."  (2014) : 188–199.

     
     

    Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y. "Distribution- Aware Sampling and Weighted Model Counting for SAT. Proc. 29th AAAI Conf. on Artificial Intelligence."  (2014) : 1722–1730.

     
     

    Chakraborty, S., Meel, K.S., Vardi, M.Y. "Balancing Scalability and Uniformity in SAT Witness Generator. Proc. 51st Design Automation Conference."  (2014) : 1–6.

     
     

    Chatterjee, K., Doyen, L., Nain, S., Vardi, M.Y. "The Complexity of Partial- Observation Stochastic Parity Games with Finite-Memory Strategies. Proc. 17th Int’l Conf. on Foundations of Software Science and Computation Structures."  (2014) : 242–257.

     
     

    Ehlers, R., Lafortune, S., Tripakis, S., Vardi, M.Y. "Bridging the Gap between Supervisory Control and Reactive Synthesis: Case of Full Observation and Centralized Control. Proc. 12th Int’l Workshop on Discrete Event Systems."  (2014) : 222–227.

     
     

    Lahijanian, M., Kavraki, L.E., Vardi, M.Y. "A Sampling-Based Strategy Planner for Nondeterministic Hybrid Systems. Proc. Int’l IEEE Conf. on Robotics and Automation."  (2014) : 3005-3012.

     
     

    Li, J., Zhang, L., Pu, G., Vardi, M.Y., and He, J. "LTLf satisfibility checking. In Proc 21th European Conf. on Artificial Intelligence, pp. 91–96, 2014.."  (2014) : 91–96.

     
     

    Query Processing under GLAV Mappings for Relational and Graph Databases (PVLDB'13 paper with C. Calvanese, G. De Giacomo, and M. Lenzerini).

     
     

    Linear Temporal Logic and Linear Dynamic Logic on Finite Traces G. De Giacomo (IJCAI'13 paper with G. De Giacomo).

     
     

    LTL Satisfiability Checking Revisited (TIME'13 paper with with J. Li, L. Zhang, G. Pu, and J. He).

     
     

    Semantic Acyclicity on Graph Databases (PODS'13 paper with P. Barcelo and M. Romero).

     
     

    A Scalable Apprximate Model Counter (CP'13 paper with S. Chakraborty and K. Meel)

     
     

    A Scalable and Nearly Uniform Generator of SAT Witnesses (CAV'13 paper with S. Chakraborty and K. Meel).

     
     

    Regular Real Analysis (LICS'13 paper with S. Chaudhuri and S. Sankaranarayanan).

     
     

    Profile Trees for Buchi Word Automata, with Application to Determinization (GANDALF'13 paper with S. Fogarty, O. Kupferman, and T. Wilke).

     
     

    Solving Partial-Information Stochastic Parity Games (LICS'13 paper with S. Nain).

     
     

    E. Friedgut, O. Kupferman, M.Y. Vardi "Buchi Complementation Made Tighter." Int'l J. of Foundations of Computer Science, 17:4 (2006) : 851-867.

     
     

    E. Friedgut, O. Kupferman, M.Y. Vardi "Buchi Complementation Made Tighter." Int'l J. of Foundations of Computer Science, 17:4 (2006) : 851-867.

     
     

    M.Y. Vardi "Automata-Theoretic techniques for Temporal Reasoning." In Handbook of Modal Logic (2006) : 971-989.

     
     

    A. Ferrara, G. Pan, M. Y. Vardi "Treewidth in Verificaton: Local vs. Global." Proceedings of the 12th Int'l Conf on Logic for Programming and Artificial Intelligence, LNCS 3835 (2005)

     
     

    D. Tabakov, M.Y. Vardi "Experimental evaluation of classical automata constructions." Proceedings of the 12th Int'l Conf on Logic for Programming and Artificial Intelligence, LNCS v 3835 (2005) : p 396-411.

     
     

    A. Atserias, P.G. Kolaitis, and M.Y. Vardi "Constraint Propagation as a Proof System." Proceedings of the International Conference on Principles and Practice of Constraint Programming (2004) : 77-91.

     
     

    B.J. McMahan, G. Pan, P. Porter, and M.Y. Vardi "Projection Pushing Revisited." 9th International Conference on Extending Database Technology (EDBT) (2004) : 441-458.

     
     

    D. Bustan, O. Kupferman, and M.Y. Vardi "A Measured Collapse of the Modal u-Calculus Alternation Hierarchy." Proceedings of the 21st Annual Symposium on Theoretical Aspects of Computer Science (2004) : 522-533.

     
     

    D. Bustan, S. Rubin, and M.Y. Vardi "Verifying Omega-Regular Properties of Markov Chains." Proceedings of the 16th International Conference on Computer Aided Verification (CAV) (2004) : 189-201.

     
     

    E. Friedgut, O. Kupferman, and M.Y. Vardi "Buchi Complementation Made Tighter." Proceedings of the 2nd Internatinal Conference on Automated Technology for Verification and Analysis (2004) : 64-78.

     
     

    G. Pan and M.Y. Vardi "Symbolic Decision Procedures for QBF." Proceedings of the 10th International Conference on Principles and Practice of Constraint Programming (2004) : 453-467.

     
     

    N. Piterman and M.Y. Vardi "Global Model-Checking of Infinite-State Systems." Proceedings of the 16th International Conference on Computer Aided Verification (CAV) (2004) : 387-400.

     
     

    O. Kupferman and M.Y. Vardi "From Complementation to Certification." Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2004) : 591-606.

     
     

    R. Sebastiani, E. Singerman, S. Tonetta, and M.Y. Vardi "GSTE is Partitioned Model Checking." Proceedings of the 16th International Conference on Computer Aided Verification (CAV) (2004) : 229-241.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "Query Containment Using Views." Proceedings of the 11th Italian Symposium on Advanced Database Systems (SEBD 2003) (2003) : 467-474.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "View-based Query Containment." Proceedings of the 22nd ACM Symposium on Principles of Database Systems (2003) : 56-67.

     
     

    H. Chockler, O. Kupferman, and M.Y. Vardi "Coverage Metrics for Formal Verification." Proceedings of the 10th conference on Correct Hardware Design and Verification Methods and in Springer-Verlag, Lecture Notes in Computer Science 2860 (2003) : 111-125.

     
     

    M. Glusman, G. Kamhi, S. Mador-Haim, R. Fraer, and M.Y. Vardi "Multiple-counterexample Guided Iterative Abstraction Refinement - an Industrial Evaluation." Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003) : 176-191.

     
     

    M. Pistore and M.Y. Vardi "The Planning Spectrum - One, Two, Three, Infinity." Proceedings of the 18th IEEE Symposium on Logic in Computer Science (2003) : 234-243.

     
     

    N. Piterman and M.Y. Vardi "Micro-macro Stack Systems - A New Frontier of Elementary Decidability for Sequential Systems." Proceedings of the 18th IEEE Symposium on Logic in Computer Science (2003) : 311-390.

     
     

    O. Kupferman and M.Y. Vardi "AFMC." Proceedings of the 30th International Colloquium on Automata, Languages and Programming (2003) : 697-713.

     
     

    R. Armoni, D. Bustan, O. Kupferman, and M.Y. Vardi "Resets vs Aborts in Linear Temporal Logic." Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003) : 65-80.

     
     

    R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, and M.Y. Vardi "Enhanced Vacuity Detection in Linear Temporal Logic." Proceedings of the 15th International Conference on Computer-Aided Verification and in Springer-Verlag's Lecture Notes in Computer Science 2725 (2003) : 368-380.

     
     

    S. Gurumurthy, O. Kupferman, F. Somenzi, and M.Y. Vardi "On Complementing Nondeterministic Buchi Automata." Proceedings of the 10th Conference on Correct Hardware Design and Verification methods and in Springer-Verlag, Lecture Notes in Computer Science 2860 (2003) : 96-110.

     
     

    T. Feder and M.Y. Vardi "Homomorphism Closed vs Existential Positive." Proceedings of the 18th IEEE Symposium on Logic in Computer Science (2003) : 311-320.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "Lossless Regular Views ." Proceedings of the 21st ACM Symposium on Principles of Database Systems (2002) : 247-258.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "Reasoning about Actions and Planning in LTL Action Theories." Proceedings on the 8th International Conference on the Principles of Knowledge Representation and Reasoning (KR 2002) (2002) : 593-602.

     
     

    G. Pan, U. Sattler, M.Y. Vardi "BBD-Based Decision Procedures for K.." Proceedings of the 18th International Conference on Automated Deduction (CADE'02) (2002) : 16-30.

     
     

    M.Y. Vardi, O. Kupferman and N. Piterman "Model Checking Linear Properties of Prefix-Recognizable Systems." Proceedings of the 14th International Conference on Computer-Aided Verification (CAV'02), Lecture Notes in Computer Science, 2404 (2002) : 371-385.

     
     

    M.Y. Vardi, O. Kupferman and N. Piterman "Pushdown Specification." Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'02), Lecture Notes in Artificial Intelligence, 2514 (2002) : 262-38.

     
     

    M.Y. Vardi, O. Kupferman and U. Sattler "The Complexity of the Graded u-calculus." Proceedings of the 18th International Conference on Automated Deduction (CADE'02), Lecture Notes in Artificial Intelligence, 2392 (2002) : 423-437.

     
     

    M.Y. Vardi, V. Dalmau & P.G. Kolaitis "Constraint Satisfaction, Bounded Treewidth, and Finite-variable Logics." Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming (CP2002), Lecture Notes in Computer Science, 2470 (2002) : 311-326.

     
     

    R. Batsell, L. Brenner, D. Osherson, S. Tsavachidis, R "Eliminating Incoherence from Subjective Estimates of Chance." Proceedings of the 8th International Conference on the Principles of Knowledge Representation and Reasoning (KR 2002) (2002) : 353-364.

     
     Conference papers
     

    CHIMP: a Tool for Assertion-Based Dynamic Verification of SystemC Models (DIFTS'13 paper with D. Tabakov and S. Dutta)

     
     

    Benque, D., Bour ton, A., Cockerton,  C., Cook, B., Fisher, J., Ishtiaq,  S., Piterman, N., Taylor,  A., Vardi, M,Y.: Bma:  Visual tool for modeling and analyzing biological networks. Proc.  24 Int'l  Conf.  on Computer-Aided  Verification,  pp. 686-692, 2012.

     
     

    Mogavero, F., Murano, A. , Perelli, G., Vardi, M.Y.: What  makes ATL** decidable?

    A decidable  fragment  of Strategy Logic.  Proc.  23rd Int'l  Conf.  on  Concurrency

    Theory, pp. 193-208, 2012.

     
     

    Nain, S., Vardi, M.Y.: Synthesizing  probabilistic composers.  Proc.  15th Int'l Conf. on Foundations  of Software  Science  and Computational  Structures,  pp.  421-436,

    2012

     
     

    Tabakov, D. , Vardi , M.Y.:  Automatic aspectization of SystemC,.  Proc. workshop on Modularity in Systems  Software, pp. 9-14,  2012

     
     

    Calvanese, D., De Giacomo, G., Lenzerini, M., Vardi, M.Y.: Simpligying schema mappings.  Proc. 14th Int'l Conf. on Database Theory, pp. 114-125, 2011.

     
     

    Cook, B., Koskinen, E., Vardi, M.Y.: Temporal Property Verification as a Program Analysis Task.  Proc. 23rd Int'l Conf. on Computer Aided Verification, Lecture Notes in Computer Science 6806, Springer, 2011, pp. 333-348.

     
     

    Fisher, J., Henzinger, T.A., Nickovic, D., Piterman, N., Singh, A.V., Vardi, M.Y.: Dynamic Reactive Modules.  Proc. 22nd Int'l Conf. on Concurrency Theory, pp. 404-418, 2011.

     
     

    Fisher, J., Piterman,N., Vardi, M.Y.: The Only Way Is Up. Proc. 17th Int'l Symp. on Formal Methods, Lecture Notes in Computer Science 6664, Spring, pp. 3-11, 2011.

     
     

    Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, Thomas: Unifying Buchi Complementation Constructions. Proc. 25th Annual Conf. on Computer Science Logic., pp. 248-263, 2011.

     
     

    Kupferman, O., Lustig, Y., Vardi, M.Y., Yannakakis, M.: Temporal synthesis for bounded systems and environments. Proc. 28th Int'l Symp. on Theoretical Aspects of Computer Science, pp. 615-626, 2011.

     
     

    Lustig, Y., Nain, S., Vardi, M.Y.: Synthesis from Probabilistic Components. Proc. 25th Annual Conf. on Computer Science Logic, pp. 412-427, 2011.

     
     

    Lustig, Y., Vardi, M.Y.: Synthesis from Recursive-Components Libraries.  Proc. 2nd Int'l Symp. on Games, Automata, Logics and Formal Verification, EPTCS 54, pp. 1-16, 2011

     
     

    Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. Proc. 17th Int'l Symp. on Formal Methods, Lecture Notes in Computer Science 6664, Springer pp. 417-431, 2011.

     
     

    Aminoff, B., Murano, A., Vardi, M.Y. "Pushdown module checking with imperfect information." Proc. 18th Int'l Conf. on Concurrency Theory, Lecture Notes in Computer Science, 4703 (2007) : 460-475.

     
     

    Armoni, R., Fix, L., Fraer, R., Heyman, T., Vardi, M.Y., Vizel, Y., and Zbar, Y. "Deeper bound in BMC by combining constant propagation and abstraction." Proc., 12th Asia and South Pacific Design Automation Conference (ASP-DAC) (2007)

     
     

    Bordeaux, L., Hamadi, Y., Vardi, M.Y. "An Analysis of Slow Convergence in Interval Propagation." Proc. 13th Int'l Conf. on Principle and Practice on Constraint Programming, Lecture Notes in Computer Science, 4741 (2007) : 790-797.

     
     

    Etessami, K., Kwiatkowska, M., Vardi, M.Y., and Yannakakis, M. "Multi-objective Model Checking of Markov Decision." 13th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 4424 (2007) : 50-65.

     
     

    Plaku, E., Kavraki, L.E., Vardi, M.Y. "A motion planner for a hybrid robotic system with kinodynamic constraints." Proc. IEEE Int'l Conf. on Robotics and Automation (2007) : 692-697.

     
     

    Rozier, K.Y., Vardi, M.Y. "LTL Satisfiability Checking." Proc. 14th Workshop on Model Checking Software (SPIN '07), Lecture Notes in Computer Science, 4595 (2007) : 149-167.

     
     

    Sebastiani, R., Tonetta, S., Vardi, M.Y. "Property-Driven Partitioning for Abstraction Refinement." Proc. 13th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 4424 (2007) : 389-404.

     
     

    G. Pan, M.Y. Vardi "Fixed-parameter Hierarchies Inside PSPACE." 21th IEEE Symp. on Logic in Computer Science (2006) : 27-36.

     
     

    M. Armoni, S. Rodger, M.Y. Vardi, R. Verma "Automata Theroy, Its Relevance to Computer Science Students and Course Contents." 37th ACM Symp. on Computer Science Education (2006) : 197-198.

     
     

    O. Kupferman, M.Y. Vardi "Memoryful Branching-Time Logic." 21th IEEE Symp on Loc in Computer Science (2006) : 265-274.

     
     

    O. Kupferman, N. Piterman, M.Y. Vardi "Safraless Compositional Synthesis." 18th Int'l Conference on Computer Aided Verification, Lector Notes in Computer Science, 4144 (2006) : 265-274.

     
     

    O. Kupferman, Y. Lustig, M.Y. Vardi "On Locally Checkable Properies." 13th Int'l Conf. on Logic for Programming, Artifical Intelligence, and Reasoning, Lecture Notes in Computer Science, 4246 (2006) : 302-316.

     
     

    P.A. Bonatti, C. Lutz, A. Murano, M.Y. Vardi "The Complexity of Enriched Mu-Calculi." 33rd Int'l Colloq. on Automata, Programming, and Lauguages Lecture Notes in Computer Science, 4052 (2006) : 540-551.

     
     

    R. Armoni, D. Korchemny, A. Tiemeyer, M.Y. Vardi, Y. Zbar "Deterministic Dynamic Monitors for Linear-Time Assertions." 1st combined Int'l Workshop of Formal Approaches to Sotware Testing and Runtime Verification, Lecture Notes in computer Science, 4262 (2006) : 163-177.

     
     

    W. Aspray, F. Mayadas, M.Y. Vardi, s. Zweben "Educational Response to Offshoring." 37th ACM Symp. on Computer Science Education (2006) : 330-331.

     
     

    Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi,M. Y. "Efficient LTL compilation for SAT-based model checking." Proc., 2005 Int'l Conf on Computer Aided Design (2005) : pp 877-884.

     
     

    Armoni, R., Fix, L., Fraer, Huddleston, S., Piterman, N., Vardi, M.Y. "SAT-based induction for temporal safety properties." Proc. 2004 Workshop on Bonded Model Checking, Electronic Notes in Theoretical Computer Science, v 119:2 (2005) : pp 3-16.

     
     

    Arons, T., Elster, E., Fix, L., Mador-Haim, S., Mishaeli, M., Shalev, J., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zuck, L.D. "Formal verification of backward compatibility of microcode." Proc 17th Init'l Conf on Computer Aided Verification, Lecture Notes in Computer Science, v 3576 (2005) : pp 185-198.

     
     

    Bustan, A., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y. "Regular Vacuity." Proc 13th IFIP Conf on Correct Hardware Design and Verification Methods, LNCS, 3725 (2005) : pp 191-206.

     
     

    Calvanese, D., De Giacomo, G., Lenzerini, M., Vardi, M. "View-based query processing - on the relatioship between rewriting, answering and loolessness." proc 10th Int'l Conf on Database Theory, Lecture Notes in Computer Science, v 3363 (January 2005) : pp 321-336.

     
     

    Kupferman, O., Vardi, M.Y. "Complementation constructions for nondeterministic automata on infinite words." Proc. 11th Int'l Conf on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, v 3340 (2005) : pp 206-221.

     
     

    Kupferman, O., Vardi, M.Y. "Safraless decision procedures." Proceedings of the 46th IEEE Symposium on Foundations of Computer Science (2005) : pp 531-540.

     
     

    Moore, C., Istrate, G., Demopoulos, D., Vardi, M.Y. "A Continuous-Discontinuous Second-Order Transition in the Satisfiability of Random Horn-SAT Formulas." Proc. APPROX-RANDOM 2005, Lecture Notes in Computer Science, v 3264 (2005) : pp 414-425.

     
     

    Sebastiani, R., Tonetta, Sl., Vardi, M.Y. "Symbolic systems, explicit properties-on hybrid approaches for LTL symbolic model checking." Proc 17th Init'l Conf on Computer Aided Verification, Lecture Notes in Computer Science, v 3576 (2005) : pp 350-363.

     
     

    Vardi, M. "Model checking for database theoreticians." Procedure of the 10th Int'l Conf on Database Theory, LNCS, v 3363 (January 2005) : pp 1-16.

     
     

    D. Calvanese, G. de Giacomo, and M.Y. Vardi "Decidable Containment of Recursive Queries." Proceedings of the International Conference on Tools and algorithms for the Construction and Analysis of Systems (2003) : 330-345.

     
     

    Vardi, M., D.A. Peled "Formal Techniques for Networked and Distributed Systems - FORTE 2002." Lecture Notes in Computer Science, 2529 (2002)

     
     Other
     

    F. Mogavero and A. Murano "Proc. 2nd International Workshop on Strategic Reasoning, with F. Mogavero and A. Murano, Electronic Proceedings in Theoretical Computer Science 146, Grenoble,France."  (April 2014)

     
     

    Rehof, J., Vardi, M.Y. "Design and Synthesis from Components (Dagstuhl Seminar 14232). Dagstuhl Reports 4(6)."  (2014) : 29-47.

     
     

    Vardi, M.Y. "Boolean satisfiability: theory and engineering. Commun. ACM 57(3)."  (2014) : 5.

     
     

    Vardi, M.Y. "Moore’s law and the sand-heap paradox. Commun. ACM 57(5)."  (2014) : 5.

     
     

    Vardi, M.Y. "Openism, IPism, fundamentalism, and pragmatism. Commun. ACM 57(8)."  (2014) : 5.

     
     

    Vardi, M.Y. "Scalable conferences. Commun. ACM 57(1)."  (2014) : 5.

     
     

    Vardi, M.Y. "Would Turing have passed the Turing Test? Commun. ACM 57(9)."  (2014) : 5.

     
     

    Vardi, M.Y. Where have all the workshops gone? Commun. ACM 54(1), p. 5, 2011.

     
     

    Vardi, M.Y.: Computing for humans. Commun. ACM 54(12), p.5, 2011.

     
     

    Vardi, M.Y.: Fumbling the future. Commun. ACM 54(3), p. 5, 2011.

     
     

    Vardi, M.Y.: Is Moore's party over? Commun. ACM 54(11), p. 5, 2011.

     
     

    Vardi, M.Y.: Solving the unsolvable. Commun. ACM 54(5), p. 5, 2011.

     
     

    Vardi, M.Y.: Solving the unsolvable. Commun. ACM 54(7), p. 5, 2011.

     
     

    Vardi, M.Y.: Are you talking to me? Commun. ACM 54(9), p. 5, 2011.

     
     

    Kupferman, O., Piterman, N., Vardi, M.Y,:: An Automata-Theoretic Approach to
    Infinite-State Systems. Time for Verification, Essays in Memory of Amir Pnueli,
    Lecture Notes in Computer Science 6200, Springer, pp. 202–259, 2010

     
     

    M.Y. Vardi: Revisitng the publication culture in computing research. Commun. CACM 53(3), p.5, 2010

     
     

    Vardi, M.,Y.: Globalization and Offshoring of Software revisited. Commun. ACM
    53(5), p. 5, 2010

     
     

    Vardi, M.Y.: Hypercriticality. Commun. ACM 53(7), p. 5, 2010

     
     

    Vardi, M.Y.: More debate, please! Commun. CACM 52(1), p.5, 2010

     
     

    Vardi, M.Y.: Science has only two legs. Commun. ACM 53(9), p. 5, 2010

     
     

    Vardi, M.Y.; Conferences vs. journals in computing research. Commun. ACM 52(5), p. 5, 2009.

     
     

    Vardi, M.Y.: From philosophical to industrial logics. Proc. 3rd Indian Conference
    on Logic and Its Applications, Lecture Notes in AI 5378, Springer, pp. 89-115, 2009

     
     

    Vardi, M.Y.: How are we doing? Commun. ACM 52(1), p.5, 2009

     
     

    Vardi, M.Y.: Is the image crisis over? Commun. ACM 52(11), p.5, 2009

     
     

    Vardi, M.Y.: Open, closed, or clopen access? Commun. ACM 52(7), p.5, 2009

     
     

    Vardi, M.Y.: The financial meltdown and computing. Commun. ACM 52(9), p.5, 2009

     
     

    Vardi, M.Y.; Yes, we can. Commun. ACM 52(3), p.5, 2009

     
     

    Greimel, K., Bloem, R., Jobstmann, B., Vardi, M.Y. "Open Implication." Proc. 35th Int. Colloquium on Automata, Languages and Programming (ICALP'08) (2008) : 361-372.

     
     

    Plaku, E., Kavraki, L.E., Vardi, M.Y. "Impact of workspace decompositions on discrete search leading continuous exploration (DSLX) motion planning." Proc. IEEE Int'l Conf. on Robotics and Automation (2008) : 3751-3756.

     
     

    Tabakov, D., Vardi, M.Y., Kamhi, G., Singerman, E. "A Temporal Language for System C.." Proc. 8th Int'l Conf. on Formal Methods in Computer-Aided Design, IEEE (2008) : 171-179.

     
     

    Vardi, M.Y. "A logical approach to constrant satisfaction." Complexity of Constraints (2008) : 125-155.

     
     

    Vardi, M.Y. "CACM - past, present, and future." Commun. ACM, 51(1) (2008) : 44-48.

     
     

    Vardi, M.Y. "From Church and Prior to PSL." 25 MC Festschrift (2008) : 150-171.

     
     

    Vardi, M.Y. "From monadic logic to PSL." Pillas of Computer Science (2008) : 656-681.

     
     

    Vardi, M.Y. "Let us-together-make CACM exciting." Commun. ACM, 51(10) (2008) : 5.

     
     

    Vardi, M.Y. "Where do you come from? and where are you going?." Commun, 51(7) (2008) : 5.

     
     

    Nain, S., Vardi, M.Y. "Branching vs. linear time - semantical perspective." Proc. 5th Int'l Symp. on Automated Technology for Verfication and Analysis, Lecture Notes in Computer Science, 4762 (2007) : 19-34.

     
     

    Vardi, M.Y. "Automata-theoretic model checking revisited." Proc. 7th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, 4349 (2007) : 137-150.

     
     

    Vardi, M.Y. "Formal techniques for SystemC verification." Proc. 44th ACM/IEEE Design Automation Conference (2007) : 188-192.

     
     

    Vardi, M.Y. "Linear-time model checking - automata theory in practice." Proc. 12th International Conference on Implementation and Applications of Automata, Lecture Notes in Computer Science, 4783 (2007) : 5-10.

     
     

    Vardi, M.Y. "The Buchi complementation saga." Proc. 24th Symp. on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, 4393 (2007) : 12-22.

     
     

    O. Kupferman, N. Piterman, and M.Y. Vardi "Fair Equivalence Relations." Lecture Notes in Computer Science, 2772 (2004) : 702-732.

     
     

    A. Voronkov and M. Vardi "Logic for Programming, Artificial Intelligence, and Reasoning." Lecture Notes in Artificial Intelligence, 2850 (2003)

     
     

    Accelera Formal Verification Technical Committee "Property Specification Language Reference Manual, Version 1.0."  (2003)

     
     

    M.Y. Vardi, T. Finin, and T. Henderson "Survey Results Show Better Ballance in Supply and Demand." Computing Research News, 15:2 (2003) : 6-13.

     
     

    N. Piterman and M.Y. Vardi "From Bidirectionality to Alternation." Theoretical Computer Science, 295 (2003) : 295-321.

     
     

    O. Kupferman and M.Y. Vardi "Vacuity Detection in Temporal Model Checking." Tools for Technology Transfer (2003) : 224-233.

     
     

    R.E. Bryant and M.Y. Vardi "Hope for More Balance in Supply and Demand ." Computing Research News, 14:2 (March 2002) : 4-11.

     
     

    A. San Miguel Aguirre and M.Y. Vardi "Random 3-SAT and BDDs - the Plot Thickens Further." Proceedings of Principles and Practice of Constraint Programming (CP'2001), 2239 (2001) : 121-136.

     
     

    D. Calvenese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "View-based Query Answering and Query Containment over Semistructured Data." Proceedings of the 8th International Workshop on Database Programming Languages (DBPL'01) (2001) : 17-28.

     
     

    E. Giunchiglia, M. Narizzano, A. Tacchella, and M.Y. Vardi "Towards an Efficient Library for SAT: A Maniafesto." Proceedings LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), 9 (June 2001)

     
     

    F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi "Benefits of Bounded Model Checking in an Industrial Setting." Lecture Notes in Computer Science, 2101 (July 2001) : 436-453.

     
     

    H. Chockler, O. Kupferman, R. Kurshan, and M.Y. Vardi "A Practical Approach to Coverage in Model Checking." Proceedings of the 13th International Conference on Computer-Aided Verification( (CAV'01), 2102 (2001) : 66-78.

     
     

    H. Chockler, O. Kupferman, and M.Y. Vardi "Coverage Metrics for Temporal Logic Model Checking." Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01) , 2031 (2001) : 528-542.

     
     

    J.Y. Halpern, R. Harper, N. Immerman, P.G. Kolaitis, M.Y. Vardi, and V. Vianu "On the Unusual Effectiveness of Logic in Computer Science." Bulletin of Symbolic Logic, 7:2 (2001) : 213-236.

     
     

    K. Fisler, R. Fraer, G. Kamhi, M.Y. Vardi, and Z Yang "Is There a Best Symbolic Cycle-detection Algorithm? ." Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01). (T. Margaria and W. Yi, Editors) Springer-Verlag, Lecture Notes in Computer Science, 2031 (2001) : 420-434.

     
     

    M.Y. Vardi "Branching vs. Linear Time: Final Showdown." Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), 2031 (2001) : 1-22.

     
     

    N. Piterman and M.Y. Vardi "From Bidirectionality to Alternation." Proceedings of the 26th International Symposium on Mathematical Foundations of Computer Science (MFCS'01), 2136 (2001) : 598-609.

     
     

    O. Kupferman and M.Y. Vardi "Model Checking of Safety Properties." Formal Methods in System Design, 19:3 (2001) : 291-314.

     
     

    O. Kupferman and M.Y. Vardi "On Bounded Specificatins." Proceedings of the International conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'01) (2001) : 24-38.

     
     

    O. Kupferman and M.Y. Vardi "Synthesizing Distributed Systems." Proceedings of the 16th IEEE Symposium on Logic in Computer Science (2001) : 389-398.

     
     

    O. Kupferman, M.Y. Vardi, P. Wolper "Module Checking ." Information and Computation, 164 (2001) : 322-344.

     
     

    O. Kupferman, N. Piterman, and M.Y. Vardi "Extended Temporal Logic Revisited ." Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01), 2154 (2001) : 519-535.

     
     

    U. Sattler and M.Y. Vardi "The Hybrid u-calculus." Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'01), 2083 (2001) : 76-91.

     
     

    V. King, O. Kupferman, and M.Y. Vardi "On the Complexity of Parity Word Automata." Proceedings of the 4th International Conference on Foundations of Software Science and Computational Structures, 2030 (2001) : 276-286.

     
     

    Y. Kesten, A. Pnueli, and M.Y. Vardi "Verification by Augmented Abstraction: the Automata-theoretic View." Journal of Computer and System Sciences, 62 (2001) : 668-690.

     
     

    C. Coarfa, D. Demopolous, A. San Miguel Aguirre, D. Subramanian, and M.Y. Vardi "Random 3-SAT - The Plot Thickens." Proceedings of Principles and Practice of Constraint Programming (CP'2000), Lecture Notes in Computer Science, R. Dechter, Editor , 1894 (2000) : 143-159.

     
     

    D. Calvanese, De Giacomo, G. Lenzerini, and M.Y. Vardi "What is Query Rewriting?." Proceedings of the 4th International Workshop on Cooperative Information Agents, 1260 (2000) : 51-59.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, M. Vardi "Answering Regular Path Queries Using Views." Proceedings of the 16th IEEE International Conference on Data Engineering (ICDE 2000) (2000) : 389-398.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, M.Y. Vardi "View-based Query Processing for Regular Path Queries with Inverse." Proceedings of the 19th ACM Symposium on Principles of Database Systems (2000) : 58-66.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M. Vardi "Containment of Conjunctive Regular Path Queries with Inverse." Proceedings of the 7th International Conference on Principles of Knowledge Representation (KR'2000) (2000) : 176-185.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "View-based Query Processing and Constraint Satisfaction." Proceedings of the 15th IEEE Symposium on Logic in Computer Science (2000) : 361-371.

     
     

    M. Y. Vardi "Constraints Satisfaction and Database Theory - a Tutorial." Proceedings of the 19th ACM Symposium on Principles of Database Systems (2000) : 76-85.

     
     

    O. Kuperman and M.Y. Vardi "Mu-Calculus Synthesis." Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS'00), Lecture Notes in Computer Science, M. Nielsen and B. Rovan, Editors, 1893 (2000) : 497-507.

     
     

    O. Kupferman and M.Y. Vardi "An Automata-theoretic Approach to Modular Model Checking.." ACM Transactions on Programming Languages and Systems, 22 (2000) : 87-128.

     
     

    O. Kupferman and M.Y. Vardi "An Automata-theoretic Approach to Reasoning about Infinite-state Systems." Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00) (2000)

     
     

    O. Kupferman, M.Y. Vardi, and P. Wolper "An Automata-Theoretic Approach to Branching-Time Model Checking ." Journal of the ACM, 47 (2000) : 312-360.

     
     

    O. Kupferman, P. Madhusudan, P.S. Thiagarajan, and M.Y. Vardi "Open Systems in Reactive Environments - Control and Synthesis." Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00) (2000)

     
     

    P.G. Kolaitis and M.Y. Vardi "0-1 Laws for Fragments of Second-order Logic - a Survey." 25th International Symposium on Mathematical Foundations of Computer Science (MFCS'00), Lecture Notes in Computer Science, M. Nielsen and B. Rovan, Editors, 1893 (2000) : 84-98.

     
     

    P.G. Kolaitis and M.Y. Vardi "Conjunctive-query Containment and Constraint Satisfaction." Information and Computation, 61 (2000) : 302-332.

     
     

    R. Fraer, G. Kamhi, B. Ziv, M.Y. Vardi, and L. Fix "Prioritized Traversal: Efficient ReachabilityAnalysis for Verification and Falsification." Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00) (2000)

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "Query Answering Using Views for Data Integration over the Web." Proceedings of the ACM SIGMOD Workshop on the Web and Databases (1999) : 73-78.

     
     

    D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi "Rewriting of Regular Expressions and Regular Path Queries." Proceedings of the 18th ACM Symposium on Principles of Database Systems (1999) : 194-204.

     
     

    D. Calvenese, G. De Giacomo, M. Lenzerini, and M. Vardi "Rewriting of Regular Expressions in Semi-structured Data." Proceedings of the Workshop on Query Processing for Semistructured Data and Nonstandard Data Format (1999) : 25-32.

     
     

    D. Peled, M.Y. Vardi, and M. Yannakakis "Black Box Checking." Proceedings of the Joint International Conference on Formal Description Techniques for Distributed systems and Communication Protocols (FORTE), and Protocol specification, Testing, and Verification (PSTV) (1999) : 225-240.

     
     

    G. De Giacomo and M.Y. Vardi "Automata-theoretic Approach to Planning for Temporally Extended Goals." Proceedings of the 5th European Conference on Planning (1999) : 228-240.

     
     

    J. Feigenbaum, S. Kannan, M.Y. Vardi, and M. Viswanathan "The Complexity of Problems on Graphs Represented as OBDDs." Chicago Journal of Theoretical Computer Science (1999) : Article 5.

     
     

    K. Fisler and M.Y. Vardi "Bisimulation and Model Checking." Proceedings of the 10th Conference on Correct Hardware Design and Verification Methods, 1703 (1999) : 338-341.

     
     

    M. Daniele, P. Traverso, and M.Y. Vardi "Strong Cyclic Plannign Revisited." Proceedings of the 5th European Conference on Planning (1999) : 34-36.

     
     

    N. Daniele, F. Guinchiglia, & M. Y. Vardi "Improved Automata Generation for Linear Temporal Logic." Proceedings of the 11th International Conference on Computer-Aided Verification (CAV'99); Lecture Notes in Computer Science, 1633 (1999) : 249-260.

     
     

    O. Kupferman and M.Y. Vardi "Church's Problem Revisited." Bulletin of Symbolic Logic, 5 (1999) : 245-263.

     
     

    O. Kupferman and M.Y. Vardi "Model Checking of Safety Properties." Proceedings of the International Conference on Computer-Aided (1999) : 172-183.

     
     

    O. Kupferman and M.Y. Vardi "Robust Satisfaction." Proceedings of the 10th International Conference on Concurrency Theory (CONCUR'99), 1664 (1999) : 383-398.

     
     

    O. Kupferman and M.Y. Vardi "The Weakness of Self-complementation." Proceedings of the 16th Symposium on Theoretical Aspects of Computer Science, 1563 (1999) : 455-466.

     
     

    O. Kupferman and M.Y. Vardi "Vacuity Detection in Temporal Model Checking." Proceedings of the 10th Conference on Correct Hardware Design and Verification Mothods, 1703 (1999) : 82-96.

     
     

    R. Fagin, J. Geanakopolos, J.Y. Halpern, and M.Y. Vardi "The Hierarchical Approach to Modeling Knowledge and Common Knowledge." International Journal of Game Theory, 28 (1999) : 331-365.

     
     

    R. Fraer, G. Kamhi, L. Fix, and M.Y. Vardi "Evaluating Semi-exhausting Verification Techniques for Bug Hunting." Proceedings of the 1st International Workshop on Symbolic Model Checking (SMC'99), Electronic Notes in Computer Science (1999) : 11-22.

     
     

    T. Feder and M.Y. Vardi "The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: a Study Through Datalog and Group Theory." SIAM Journal on Computing, 28 (1999) : 57-104.

     
     

    "The Truth, the Whole Truth, and Nothing but the Truth." Logic in Action 1998 (April 1999) : 33-34.

     
     

    J. Feigenbaum, S. Kannan, M. Vardi, and M. Viswanathan "Complexity of Problems on Graphs Represented by OBDDs." Proceedings of 15th Symposium on Theoretical Aspects of Computer Science (1998)

     
     

    K. Fisler and M. Vardi "Bisimulation Minimization in an Automata-theoretic Verification Framework." Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (1998)

     
     

    K.B. Bruce, P.G. Kolaitis, and D.M. Leivant "Panel - Logic in the Computer Science Curriculum." Proceedings of the 19th ACM Symposium on Computer Science Education (1998) : 376-377.

     
     

    M. Vardi "Computational Model Theory: an Overview." Logic Journal of the IGPL 6 (1998) : 601-623.

     
     

    Moshe Y. Vardi "Sometimes and Not Never Re-revisited: on Branching vs. Linear Time." Proceedings of 9th International Conference on Cuncurrency Theory (September 1998)

     
     

    O. Kupferman and M. Vardi "Freedom, Weakness, and Determinism: from Linear-time to Branching-time." Proceedings of the 13th IEEE Symposium on Logic in Computer Science (1998)

     
     

    O. Kupferman and M. Vardi "Relating Linear and Branching Model Checking." Programming Concepts and Methods (PROCOMET '98) (1998) : 304-326.

     
     

    O. Kupferman and Moshe Y. Vardi "Verification of Fair Transition Systems." Chicago Journal of Theoretical Computer Science, Article 2 (1998)

     
     

    O. Kupferman, and M. Vardi "Weak Alternating Automata and Tree Automata Emptiness." Proceedings of the 30th ACM Symposium on Theory of Computing (1998) : 224-233.

     
     

    P.G. Kolaitis and M. Vardi "Conjunctive-query Containment and Constraint Satisfaction." Conjunctive-query Containment and Constraint Satisfaction (1998) : 205-213.

     
     

    R. Alur, T.A. Henzinger, O. Kupferman, and M. Vardi "Alternating Refinement Relations." Proceedings of the 9th International Conference on Concurrency Theory (1998)

     
     

    R. Fagin, J. Geanakopolos, J.Y. Halpern, and M. Vardi "The Expressive Power of the Hierarchical Approach to Modeling Knowledge and Common Knowledge." International Journal of Game Theory (accepted)

     
     

    R. van der Mayden and Moshe Y. Vardi "Synthesis from Knowledge-based Specifications." Proceedings of 9th International Conference on Concurrency Theory (September 1998)

     
     

    S. Ramesh, G. Sivakumar, and M. Vardi "Verification of Open Systems." Proceedings of 17th Conference on Foundations of Software Technology and Theoretical Computer Science (December 1997)

     
    Presentations
     Conference Committee Member
     

    "General Chair, Federated Logic Conference, Vienna, Austria." (July 2014)

     
     

    "General chair, 2nd Int’l Workshop on Strategic Reasoning, Grenoble, France." (April 2014)

     
     

    "Workshop co-organizer: Dagstuhl Seminar 14232, Design and Synthesis from Components.." (June 2014)

     
     

    "Where Have All the IT Jobs Gone? There, There and Right Here." Conference on the New Knowledge Economy - Global Trends and Opportunities, IIT Alumni Association of North Texas, North Texas. (May 2007)

     
     

    Program committee member.  "20th Int'l Conf on Automated Deduction." 20th Int'l Conf on Automated Deduction, Tallin, Estonia. (July 2005)

     
     

    "3rd Int'l Symp on Automated Technology for Verification and Analysis." 3rd Int'l Symp on Automated Technology for Verification and Analysis, Taipei, Taiwan. (October 2005)

     
     Invited Papers
     

    "Symbolic Model Checking Revisited." Formal Technologies School, Intel Israel Design Center. (July 2005)

     
     

    "Symbolic methods for SAT and QBF." Formal technologies School, Intel Israel Design Center. (June 2005)

     
     Invited Talks
     

    "A Logical Revolution. Invited Talk, Workshop on Logic in Computer Science and Artificial Intelligence, University of Rome La Sapienza." (December 2014)

     
     

    "Compositional Temporal Synthesis. Invited Talk, From Programs to Systems – The Systems Perspective in Computing – ETAPS Workshop in honor of Joseph Sifakis, Grenoble, France." (April 2014)

     
     

    "Compositional Temporal Synthesis. Invited Talk, Seminar on Synthesis from Components, Scholss Dagstuhl." (June 2014)

     
     

    "Compositional Temporal Synthesis. Invited Talk, Workshop on Reactive Systems, Federated Logic Conference, Vienna." (July 2014)

     
     

    "Enhancing Academic Research and Scholarship. Invited Talk, Symposium on Modern Information and Communication Technologies in Higher Education, Rome, Italy." (April 2014)

     
     

    "Phase Transitions and Computational Complexity. Invited Talk, Workshop on Theoretical Foundations of Applied SAT Solving, Banff Int’l Research Station for Mathematical Innovation and Discovery." (January 2014)

     
     

    "Would Turing Have Passed the Turing Test? Invited Talk, Work on Beyond the Turing Test, Austin, TX." (January 2015)

     
     

    From Aristotle to The iPhone. Invited Talk, Conference on Logic Across The University - Foundations and Applications. Tsinghua University, Beijing, China, October 2013.

     
     

    If Machines Are Capable of Doing Almost Any Work Humans Can Do, What Will Humans do? Invited Talk, International Summit on Innovation for Jobs, Menlo Park, March 2013

     
     

    Database Queries – Logic and Complexity. AMS Special Session on Mathematical Underpinnings of Multivariate Complexity Theory and Algorithm Design, and the Field of Incrementalization, Joint Mathematics Meeting, San Diego, January 2013

     
     

    From Philosophical to Industrial Logics. Invited Talk, Symposium on Logical Foundations of Computer Science, San Diego, January 2013

     
     

    The Rise and Fall of Linear Temporal Logic. Invited Talk, Highlights of Logic,Games, and Automata. Paris, France, September 2013.

     
     

    The Rise and Fall of Linear Temporal Logic. Invited Talk, Workshop on Software Correctness and Reliability. ETH, Zurich, Switzerland, October 2013.

     
     

    The Rise and Fall of Linear Temporal Logic. Invited Talk, Horizons in TCS: A Celebration of Mihalis Yannakakis’s 60th Birthday. Princeton, August 2013.

     
     

    And Logic Begat  Computer Science.   CITRIX  Distinguished  Lecture,  Florida  International University, February,  2012.

     
     

    And Logic Begat Computer Science.  International Conference and the Second East­ Asian School on Logic,  Language and Computation, Chongqing, China, August 2012

     
     

    Database Queries  - Logic and  Complexity.    Course  on  Informatics and  Digital Science, College of France,  Paris,  France, March 2012

     
     

    From Philosophical to Indusrial Logics. Invited Talk, Annual  Meeting of the Association  for Symbolic Logic.  Madison,  April 2012

     
     

    Graduate Students, Marshmallows, and Academic Jobs.  Graduate-Training Workshop, Rice University, May, 2012.

     
     

    P  vs.  NP,  Computer Science  Colloquium,   University  of Orleans,   France,  March 2012.

     
     

    The Rise and Fall of Linear Temporal Logic. Invited Talk, 13th  Int'l Conference on Principles  of Knowledge  Representation and  Reasoning,  Rome, Italy,  June  2012

     
     

    And Logic Begat Computer Science.  Computer Science Colloquium, Universitye of Naples Napoli Federico II, June 2011.

     
     

    And Logic Begat Computer Science.  Institute Colloquium, IIT Bombay, December 2011

     
     

    And Logic Begat Computer Science.  Separtment of Informatics, University of Bergen, September 2011.

     
     

    Assertion-based Dynamic Verification for SystemC. Intel Design Center, Haifa, Isreal, December 2011.

     
     

    Automata-Theoretic verification.  Information Management Colloquium, National Taiwan University, Taiwan, March 2011.

     
     

    Branching vs. Linear Time: Semantical Perspective.  Invited talk, 20th Conference on Computer Science Logic, Bergen, Norway, September 2011.

     
     

    Constraints, Graphs, Algebra, Logic, and Complexity.  Invited talk, Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Mumbai, India, December 2011.

     
     

    Dynamic Assertion-Based Verification for SystemC.  Electrical Engineering Colloquium, National Taiwan University, Taiwan, March 2011.

     
     

    P vs. NP, Mathematics Colloquium, Rice University, Houston, September 2011.

     
     

    P vs. NP, Mathematics Colloquium, University of Houston, Houston, October 2011.

     
     

    Branching vs. Linear Time: Semantical Perspective.  Microsoft Research, Cambridge, UK

     
     

    The Rise and Fall of LTL.  Invited talk, 2nd Int'l Symp. on Games, Automata, Logics and Formal Verification, Minori, Italy, June 2011.

     
     

    The Rise and Fall of Linear Temporal Logic. Invited talk, Workshop on Games, Logic and Security, Rennes, France, October 2011.

     
     

    The Rise and Fall of Linear Temporal Logic. Computer Science Colloquium, Cornell University, Ithaca, November 2011

     
     

    The Rise, Fall, and Rise of Dependency Theory - Part I, Rise and Fall. Invited talk, 30th ACM Symp. on Principles of Database Systems, Athens, Greece, June 2011.

     
     

    Amir Pnueli, Ahead of His Time. Invited Talk, 22nd Computer-Aided Verification, Edinburgh,
    UK, July 2010

     
     

    And Logic Begat Computer Science. Unifying Keynote Talk, ETAPS 2010, Cyprus, March
    2010

     
     

    Branching vs. Linear Time: A Semantical Perspective. Israeli Verification Day, Weizmann
    Institute of Science, Israel, April 2010

     
     

    Constraints, Graphs, Algebra, Logic, and complexity. Invited Talk, 16th International
    Conference on Principles and Practice of Constraint Programming, St. Andrews, UK,
    September 2010

     
     

    Datalog Containment and Regular Queries. Datalog 2.0 Workshop, Magdalene College,
    Oxford University, UK, March 2010

     
     

    From Aristotle to the Pentium. Hebrew Speaking Professional Group, Houston,
    September 2010

     
     

    From Lowenheim to Pnueli, from Pnueli to PSL and SVA. Amir Pnueli Memorial Symposium,
    New York University, May 2010

     
     

    Hybrid Logics: The Search for Decidability and Tractability Frontiers. Invited Talk,
    Workshop on Hybrid Logic and Applications, Edinburgh, UK, July 2010

     
     

    P vs. NP. Kennedy Institute for Information Technology Lunch Talk, September
    2010

     
     

    Symbolic Techniques in Propositional Satisfiability Solving. Microsoft Research,
    Cambridge, UK, July 2010

     
     

    Symbolic Techniques in Propositional Satisfiability Solving. Invited talk, International
    Workshop on Comparing Logical Decision Methods, Edinburgh, UK, July 2010

     
     

    The Logic of Life. Invited talk, Symposium on Transformational Information Engineering
    and Science. Nanyang Technical University, Singapore, January 2010

     
     

    And Logic Begat Computer Science. Invited talk, Computer Science 50th Annversary,
    University of Birmingham, UK, November 2009

     
     

    And Logic Begat Computer Science. Tata Consultancy services, Chennai, India,
    January 2009

     
     

    And Logic Begat Computer Science. Milner Lecture, School of Informatics, Edinburgh
    University, Scotland, June 2009

     
     

    And Logic Begat Computer Science. Microsoft Research, Bangalore, India, January
    2009

     
     

    And Logic Begat Computer Science. Computer Science Colloquium, Pomona College,
    February 2009

     
     

    Constraints, Graphs, Algebra, Logic, and Complexity. Plenary talk, 6th Annual Conference
    on Theory and Applications of Models of Computation, ChangSha, China, May 2009

     
     

    Constraints, Graphs, Algebra, Logic, and Complexity. An Honorary Day for Robert L.
    Constable, Ben Gurion University, Israel, June 2009

     
     

    Constraints, graphs, algebra, logic, and complexity. Invited talk, Maltsev Meeting,
    Novosibirsk, Russia, August 2009

     
     

    Formal Techniques for System-Level Verification. Invited tutorial, 9th Conf. on Formal
    Methods in Computer-Aided Design, Austin, November 2009

     
     

    From Aristotle to the Pentium (part of a series on Breakthroughs in Engineering:
    Past, Present and Future). School of Continuing Studies, Rice University, April
    2009

     
     

    From Aristotle to the Pentium. Public Symposium on The Convergence of Logic, Mathematics and Computer Science, UCLA, April 2009

     
     

    From Philosophical to Industrial Logics. Invited Talk, 3rd Indian Conference on Logic
    and Its Applications, Chennai, India, January 2009

     
     

    From Verification to Synthesis. Microsoft Research, Cambridge, UK, July 2009

     
     

    From Verification to Synthesis. Keynote Talk, 29th Brazilian Computer Society Congress,
    Bento Goncalves, Brazil, July 2009

     
     

    From program synthesis to service composition. Bertinoro Workshop on Data and Service
    Integration. Bertinoro, Italy, March 2009

     
     

    Model checking as a reachability problem. Invited talk, 3rd Workshop on Reachability
    Problems, Paris, France, September 2009

     
     

    Symbolic Techniques in Propositional Satisfiability Solving. 12th Int’l Conf. on Theory
    and Applications of Satisfiability Testing, Swansea, Wales, July 2009

     
     

    The High-Tech Industry in Israel. The Houston Jewish Community 2009 Study
    Day, February 2009

     
     

    "And Logic Begat Computer Science." Algebra Mini-Conference, Sam Houston State University. (April 2008)

     
     

    "And Logic Begat Computer Science." DigiteoLabs Conference, INRIA Scalay, France. (November 2008)

     
     

    "And Logic Begat Computer Science." LIFO Seminar, Orleans University, France. (November 2008)

     
     

    "And Logic Begat Computer Science." Cray Lecture, Computer Science, University of Minnesota. (Minneapolis, Minnesota) With November 2008

     
     

    "Automated Verification=Graphcs, Logic, and Automata." Computer Science Coloquium, Christian-Albrechts University, Kiel, Germany. (June 2008)

     
     

    "Designing a property specification language." Workshop on 25 Years of Con-currency at CWI, Amsterdam. (May 2008)

     
     

    "From Philosophical to Industrial Logic." Symposium on XML, Logic, and Automata, Grantown-on-Spey, Scotland. (July 2008)

     
     

    "From Philosophical to Industrial Logic." Computer Science Coloquium, Haifa University. (May 2008)

     
     

    "From Philosophical to Industrial Logic." Microsoft Research, Cambridge, UK. (July 2008)

     
     

    "From Philosophical to Industrial Logic." Computer Science Seminar, University of Chicago. (April 2008)

     
     

    "From Verification to Synthesis." First BCS Conference on Visions of Computer Science, London, UK. (September 2008)

     
     

    "From philosophical to industrial logics." CS Seminar, ENS Cachan, France. (November 2008)

     
     

    "Logic and Computation." European Academy of Science, Brussels. Belgium. (November 2008)

     
     

    "Logic, Automata, Games and Algorithms." Institute of Informatics, University of Wroclaw, Poland. (September 2008)

     
     

    "Logic, Automata, Games, and Algorithms." Computability in Europe 2008, Athens, Greece. (June 2008)

     
     

    "Research Ethics: "To Publish Alone"." Rice Undergraduate Scholars Program, Rice University. (October 2008)

     
     

    "Temporal Languages for System C.." Formal Techniques Seminar, Intel Design Center, Haifa, Isreal. (June 2008)

     
     

    "The High-Tech Industry in Israel." The Houston Jewish Community 2008 Study Day, Houston. (February 2008)

     
     

    "Where have all the IT jobs gone?." Institute of Informatics, University of Wroclaw, Poland. (September 2008)

     
     

    "Automata-Theoretic Model Checking Revisited." Formal Techniques School, Intel Design Center, Haifa, Isreal. (July 2007)

     
     

    "Automata-Theoretic Model Checking Revisited." 8th International Conference on Verification, Model Checking and Abstract Interpretation, Nice, France. (January 2007)

     
     

    "Constraint Satisfaction." Workshop on Universal Algebra and the Constraint Satisfaction Problem, Nashville. (June 2007)

     
     

    "Formal Techniques for SystemC Verification." Intel's Annual Symposium on VLSI CAD and Validation - Design and Validation Challenges of Multi-Core Systems, Nanoscale Silicon, Haifa. (July 2007)

     
     

    "From Lowenheim to PSL." British Logic Colloquium, London. (September 2007)

     
     

    "Globalizationa and Offshoring of Software." American Distance Education Consortium, Seattle. (April 2007)

     
     

    "Linear-Time Model Checking - Automata Theory in Practice." 12th Int'l Conf. on Implementation and Applications of Automata, Prague. (July 2007)

     
     

    "Logic, Automata, Games, and Algorithms." 13th Int'l Congress on Logic, Methodology, and Philosophy of Science, Beijing. (August 2007)

     
     

    "Process Equivalene Revisited." 23rd Conference on the Mathematical Foundations of Programming Semantics, New Orleans, LA. (April 2007)

     
     

    "The Automata-Theoretic Approach." 5th International Symposium on Automated Technology for Verification and Analysis, Tokyo, Japan. (October 2007)

     
     

    "The Automata-Theoretic Approach." 5th International Symposium on Automated Technology for Verification and Analysis, Tokyo, Japan. (October 2007)

     
     

    "The Buchi Complementation Saga." 24th Symp. on Theoretical Aspects of Computer Science, Aachen, Germany. (February 2007)

     
     

    "The Buchi Complementation Saga." 1st Workshop on Omega-Automata, Tokyo, Japan. (October 2007)

     
     

    "The Buchi Complementaton Saga." 1st Workshop on Omega-Automata, Tokyo, Japan. (October 2007)

     
     

    "Alternation as an Algorithmic Construct." British colloquium of Theoretical Computer Science, Swansea. (April 2006)

     
     

    "From Church and Prior to PSL." Workshop on 25 Years of Model Checking, Federated Logic Conference, Seattle. (August 2006)

     
     

    "Games as an Algorithmic Construct." Annual Meeting, Games and Automata for Synthesis and Validationd Research Training Network, Cambridge, UK. (July 2006)

     
     

    "Games as an Algorithmic Construct." Department of Languages and Systems Informatics,, Polytechnic University of Catalonia. (December 2006)

     
     

    "Globalization and Offshoring of Software.." The Innovation Imperative - Globalization and National Competitiveness Conference, Stockholm. (April 2006)

     
     

    "Where Have All the IT Jobs Gone?." Computer and Information Technology Institute Lunch Talk, Fondren Library, Rice University. (November 2006)

     
     

    "A Game-theoretic approach to automated program generation." IFIP Working Group on Program Generation, (WG2.11), Rice University. (March 2005)

     
     

    Colloquium Honoris Causa.  "A call to regularity." IRISA, Rennes, France. (October 2005)

     
     

    "Alternation as an algorithmic construct." Workshop on Programming Logics in memory of Harald Ganzinger, MIP, Germany. (June 2005)

     
     

    "And logic begat computer science." Lamar University, Beaumont, Texas. (April 2005)

     
     

    "And logic begat computer science." University of Illinois, Chicago, IL. (February 2005)

     
     

    "And logic begat computer science." University of Illinois, (October 2005)

     
     

    "Automata-Theoretic Verification." Intel Research Pittsburgh, Pittsburgh, PA. (October 2005)

     
     

    "Buechi complementation -- a 40-year saga." 9th Asian Logic Conf, Novasibirsk, Russia. (August 2005)

     
     

    "Designing a property-specification language." Formal Methods Seminar, University of Illinois. (October 2005)

     
     

    "Invited tutorial on computer-aided verification (three lectures)." Annual meeting of the association for symbolic logic, Stanford University. (March 2005)

     
     

    "Model checking for database theoreticians." 10th Int'l Conf on Database Theory, Edinburgh, Scotland. (January 2005)

     
     

    "Tree automata in program synthesis." Dagstuhl workshop on Synthesis and Planning, (June 2005)

     
     

    "Who started the information revolution?." School of Continuing Studies, Rice University. (November 2005)

     
     

    "Alternation as an Algorithmic Construct." IBM Almaden Research Center, San Jose, California. (October 2004)

     
     

    "And Logic Begat Computer Science." Yale University, New Haven, Connecticut. (January 2004)

     
     

    "And Logic Begat Computer Science." Faculty of Mathematics, Weizmann Institute of Science, Israel. (May 2004)

     
     

    "And Logic Begat Computer Science." University of California, San Diego, California. (January 2004)

     
     

    "Markov Processes and Markov Decision Processes - The Verification Perspective." 20th Conference on Uncertainty in Artificial Intelligence, Banff, Canada. (July 2004)

     
     

    "The Logic of Life. Informatics - Defining the Research Agenda." Indiana University, Bloomington, Indiana. (September 2004)

     
     

    "A Call to Regularity." Symposium in Honor of Jeffrey D. Ullman, Stanford, California. (December 2002)

     
     

    "A Call to Regularity." Workshop on Principles of Computing and Knowledge (in memory of Paris C. Kanellakis), Federated Computing Research Conference. (June 2003)

     
     

    "And Logic Begat Computer Science." Department of Computer Science, University of Kentucky, Lexington, Kentucky. (November 2003)

     
     

    "And Logic Begat Computer Science." Symposium in Honor of Prof. Baruch Muskat, Bar Ilan University, Israel. (May 2003)

     
     

    "And Logic Begat Computer Science." Victoria University, Wellington, New Zealand. (December 2003)

     
     

    "And Logic Begat Computer Science." Auckland University, Auckland, New Zealand. (December 2003)

     
     

    "And Logic Begat Computer Science." Saul Gorn Memorial Lecture, University of Pennsylvania. (April 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Department of Compputer Science and Engineering, SUNY-Buffalo, Buffalo, New York. (October 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." International Joint Conference on Artificial Intelligence, Acapulco, Mexico. (August 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Victoria University, Wellington, New Zealand. (December 2003)

     
     

    "Constraints, Graphs, Algebra, and Logic." Third Haifa Workshop on Interdisciplinary Applications of Graph Theory, Combinatorics, and Algorithms, Haifa, Israel. (May 2003)

     
     

    "Constraints, Graphs, Algebra, and Logic." Victoria University, Wellington, New Zealand. (December 2003)

     
     

    "Designing a Property Specification Language." Dutch Theory Day, Utrecht, The Netherlands. (March 2003)

     
     

    "Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach." Dagstuhl Workshop on Probabilistic Methods in Verification and Planning, Dagstuhl, Germany. (May 2003)

     
     

    "0-1 Laws for Fragments of Existential Second-Order Logic: A Survey." Invited, AMS-MAA-ASL Joint Mathematics Meetings, (January 2002)

     
     

    "A Call to Regularity." Computer Science Symposium in Honor of Jeffrey D. Ullman, Stanford University, Stanford, California. (December 2002)

     
     

    "Alternation." 8th European Conference on Logics in Artificial Intelligence, Cosenza, Italy. (September 2002)

     
     

    "Automata and Logic: Words, Trees, and Forests." Invited, Workshop on Hybrid Logic, Federed Logic Conference, Copenhagen, Denmark. (July 2002)

     
     

    "Common Knowledge Revisited." Symposium on Epistemic Logic, Danish Network for Philosophical Logic, Roskilde University. (May 2002)

     
     

    "Common Knowledge: Now You Have It, Now You Don't." Approaches Formelles Outils D'Analyse et de Synthese, Orleans University, France. (September 2002)

     
     

    "Constraint Satisfaction and Database Theory." Database Seminar, Computer Science Department, University of Washington, Seattle, Washington. (November 2002)

     
     

    "Designing a Property Specification Language." Center for Research on Embedded Systems and Technology, Georgia Institute of Technology, Atlanta, Georgia. (October 2002)

     
     

    "Logic and Automata: a Match Made in Heaven." Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, International Max Planck Research School for Computer Science, Saarbrucken, Germany. (March 2002)

     
     

    "Model Checking: a Complexity-theoretic Perspective." First International Workshop on Parallel and Distributed Model Checking, Brno, Czech Republic. (August 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Workshop on Learning and Formal Verification - in Honor of Eli Shamir, Neve Ilan, Israel. (May 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Computer Science Department, University of Washington, Seattle, Washington. (November 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, International Max Planck Research School for Computer Science, Saarbrucken, Germany. (March 2002)

     
     

    "The Information Revolution - Reality or Hype?." International School on Disarmament and Research on Conflicts, Trento, Italy. (August 2002)

     
     

    "Verification=Logic+Algorithms." Games Network Kick-Off Meeting, Edinburgh, United Kingdom. (September 2002)

     
     Keynote Speaker
     

    "Compositional Temporal Synthesis. Keynote Talk, 6th NASA Formal Methods Symposium, Clear Lake, TX." (April 2014)

     
     

    "SAT Sampling and Counting: FromTheory to Practice. Keynote Talk, Haifa Verification Conference, Haifa, Israel." (November 2014)

     
     

    A Logical Revolution. Plenary Talk, 25th Academia Europaea Anniversary Conference, Wroclaw, Poland, September 2013.

     
     

    A Logical Revolution. Keynote Talk, 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, St. Petersburg, Russia, August 2013.

     
     

    Branching vs. Linear Time: Semantical Perspective. Distinguished Carl Adam Petri Lecture, 34th International Conference on Application and Theory of Petri Nets and Concurrency, Milan, Italy, June 2013.

     
     

    And Logic Begat Computer Science, Keynote Talk, 23rd Conference of the Chilean Computer Science Society, Vapapariso, Chile, November 2012

     
     

    Compositional Temporal Synthesis. Keynote Talk,  9th International Conferencr on Quantitative Evaluation of Systems  and  lOth Int'l  Conference on Formal  Modeling and  Analysis  of Timed Systems,  London,  UK, September 2012.

     
     

    The Rise and Fall of Linear Temporal Logic. Keynote Talk,  23rd Conference dr the Chilean Computer Science Society, Vapapariso, Chile, November 2012.

     
     

    The Tragedy of The Computing Research Commons. Keynote Talk, European Computer
    Science Summit, Prague, October 2010

     
     

    "Automata-Theories Model Checking Revisited." 4th Haifa Verification Conference, Haifa, Isreal. (October 2008)

     
     

    "From Philosophical to Industrial Logic." 6th NASA Langley Formal Methods Workshop, (April 2008)

     
     

    "From verification to synthesis." 2nd IFIP Working Conference on Verified Software - Theories, Tools, and Experiments, Toronto, Canada. (September 2008)

     
     

    "Branching vs. Linear Time: Semantical Perspective." 5th International Symposium on Automated Technology for Verification and Analysis, Tokyo, Japan. (October 2007)

     
     

    "From Verification To Synthesis." 5th International Symposium on Formal Methods for Components and Objects, Amsterdam. (November 2006)

     
     Lectures
     

    "A Logical Revolution. Invited Lecture, Reactive Systems – Modeling, Development, and Analysis – A Conference in Honor of David Harel. Weizmann Institute of Science, Rehovot, Israel." (April 2014)

     
     

    A Logical Revolution. Microsoft Research, Redmond, WA, August 2013.

     

     
     

    A Logical Revolution. Distinguihsed lecture, Dept. of Computer Science, Johns Hopkins University, January 2013

     
     

    A Logical Revolution. Distinguished Lecture, Software Engineering Institute, East China Normal University, Shanghai, China, October, 2013.

     
     

    Assertion-Based Dynamic Verification for SystemC. Intel Research and Development Center, Folsom, CA, May 2013.

     
     

    Building Rice’s Human and Organizational Capital, Public Lecture, Rice University, April 2013.

     
     

    If Machines Are Capable of Doing Almost Any Work Humans Can Do, What Will Humans do? Lunch Talk, Ken Kennedy Institute for Information Technology, Rice University, November 2013.

     
     

    On A Tower of Abstraction for Biology. Computational and Intergative Biomedical Research Center, Baylor College of Medicine, May 2013.

     
     

    Tablet computing. School of Continuing Studies, Rice University, February 2013.

     
     

    A Logical Revolution.   Award  Lecture, 39th  Int'l Colloquium  on Automata,  Languages and Programmi ng, Warwick,  UK,  July  2012

     
     

    Database Queries: Logic and Complexity. Computer Science Colloquium,  University of Rome  "La Sapienza", Italy,  December  2012.

     

     
     

    From Aristotle to the Pentium.  Distinguished Lect ure, Center for Advancing Electronics Dresden, Technical  University of Dresden,  May 2012

     
     

    From Aristotle to the Pentium. Distinguished Lecture, Centre de Recherches  Mathematiques, Montreal, February  2012

     
     

    Logic Sequence  Diagrams. Intel Strategic CAD Lab, Hillsboro, Oregon, September 2012.

     
     

    Synthesis  from  Components.  Newton  Institute for Mathematical Sciences,  Cambridge, UK, March 2012

     
     

    The  Rise and Fall of Linear Temporal Logic.  Seminar on Theory of Software Verification,  ENS Cachan,  France, March 2012

     
     

    Amir Pnueli - Ahead of His Time.  Pnueli Memorial Lecture, Weizmann Institute of Science, Rehovot, Israel, December 2011.

     
     

    And Logic Begat Computer Science.  Coxeter Lecturee, Fields Institute, Toronto, Canada, July 2011.

     
     

    And Logic Begal Computer Science.  Special Lecture, University of Rennes I, France, October 2011.

     
     

    And Logic Begat Computer Science.  Distinguished Lecture, Academica Sinica, Taiwan, March 2011.

     
     

    And Logic Begat Computer Science.  Research Lecture, Technical University of Vienna, January 2010.

     
     

    And Logic Begat Computer Science. Distinguished Lecture, Department of Computer Science, Virginia Tech, April 2011.

     
     

    Dynamic Assertion-Based Verification for SystemC.  Intel Design Center, August 2011.

     
     

    From Industrial to Philosophical Logics.  Ted and Janice Smith Distinguished Lecture, School of Information and Computer Science, University of California Irvine, February, 2010.

     
     

    From Industrial to Philosophical Logics.  10th Annual Paris C. Kanellakis Memorial Lecture, Brown University, December 2010.

     
     

    From Philosophical to Industrial Logics Coxeter Lecture, Fields Institute, Toronto, Canada, July 2011.

     
     

    Logic, Automata, Games, and Algorithms Coxeter Lecture, Fields Institute, Toronto, Canada, July 2011.

     
     

    P vs. NP, Fields Institute, Toronto, Canada, June 2011.

     
     

    And Logic Begat Computer Science. Inaugural Distinguished Lecture, Laboratory
    for Informatics, Grenoble, November 2010

     
     

    From Industrial to Philosophical Logics. 10th Annual Paris C. Kanellakis Memorial Lecture,
    Brown University, December 2010

     
     

    From Philosophical to Industrial Logics. Distinguished Lecture, Computer Science,
    University of Liverpool, UK, March 2010

     
     

    Automated Verification = Graphs, Automata, and Logic. Computer Science Distinguished
    Lecture, University of California Riverside, November 2009

     
     

    The Whole May Be Less than the Sum of the Parts: A Personal Perspective on the
    Rice-BCM Merger. Public Lecture, Rice University, October 2009

     
     

    "And Logic Begat Computer Science." Kiel Week Festival, Kiel, Germany. (June 2008)

     
     

    "And Logic Begat Computer Science." Matthew Vassar Lecture, Vassar College. (April 2007)

     
     

    "And Logic Begat Computer Science." IT Eminet Lecture Series, Louisiane Center for Computation and Technology. (June 2007)

     
     

    "Automated Verification=Graphs, Logic, and Automata." Matthew Vassar Lecture, April 2007.

     
     

    "From Lowenheim to PSL." Max Planck Institute for Software Systems, Kaiserlauten, Germany. (December 2007)

     
     

    "From Philosophical to Industrial Logic." Department of Computer Science, Ben Gurion University. (December 2007)

     
     

    "And Logic Begat Computer Science." University of Texas, Dallas. (September 2006)

     
     

    "And Logic Begat Computer Science." Godel Centenary Lecture, Reykjavik University, Iceland. (June 2006)

     
     

    "And Logic Begat Computer Science." Queen Mary University, London, UK. (May 2006)

     
     

    "And Logic Begat Computer Science." 6th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Hardware Verification, Bertinoro, Italy. (May 2006)

     
     

    "Automata in Verification." 5th International Ph.D. School in Formal Languages and Applications, Tarragona, Spain. (December 2006)

     
     

    "Compostional Safraless Synthesis, Theory Seminar." Division of Infomatics, University of Edinburgh. (April 2006)

     
     

    "Open Access Journals in the Promotion and Tenure Process." Fondren Library, Rice University. (November 2006)

     
     

    "Property-Specification Languages." 6th International School of Farmal Methods for the Design of Computer, Communication and Software Systems: Harware Verification, Bertinoro, Italy. (May 2006)

     
     

    "Where Have All The IT Jobs Gone?." ACM Distinguished Lectureship Program, Stanford, CA. (November 2006)

     
     

    "Where Have All the IT Jobs Gone?." ACM Distinguished Lectureship Program, Cambridge, MA. (September 2006)

     
     

    "Where Have All the IT Jobs Gone?." University of Texas, Dallas. (September 2006)

     
     

    "Where Have All the IT Jobs Gone?." ACM Distinguished Lectureship Program University of Texas, Dallas. (September 2006)

     
     

    "Where Have all the IT Jobs Gone?." Computer Research Association, (December 2006)

     
     

    Distinguished Lecture.  "And logic begat computer science." University of Toronto, Toronto, Canada. (September 2005)

     
     

    Distinguished lecture.  "Automated verification = graphs, logic, and automata." Simon Fraser University, Canada. (February 2005)

     
     

    teacher.  "Games-, Automata- and Logic-Based Systems Design." Summer School on Logic Aspects of Secure Computer Systems, Marktoberdorf, Germany. (August 2005)

     
     

    teacher.  "The Automata-Theoretic Approach to Verification." 17th International School for Computer Science Researchers, Lipari, Italy. (July 2005)

     
     

    "A Call to Regularity." IBM Almaden Research Center, San Jose, California. (July 2004)

     
     

    "A Formal Approach to the Verification Crisis." Computer Science Graduate Seminar, Rice University, Houston, Texas. (August 2004)

     
     

    "A Formal Approach to the Verification Crisis." Computer Science Graduate Seminar, Rice University, Houston, Texas. (January 2004)

     
     

    "And Logic Begat Computer Science." Institute of Mathematics, Hebrew University, Jerusalem, Israel. (May 204)

     
     

    "And Logic Begat Computer Science." University of Rome, Italy. (September 2004)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of Rome, Italy. (September 2004)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of California, San Diego, California. (January 2004)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of Connecticut, (January 2004)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Los Alamos National Lab, Albuquerque, New Mexico. (April 2004)

     
     

    "Constraints, Graphs, Algebra, and Logic." Logic and Semantics Seminar, Cambridge University, United Kingdom. (June 2004)

     
     

    "Designing a Property-specification Language." Microsoft Research, Redmond, Washington. (September 2004)

     
     

    "GSTE Is Partitioned Model Checking." Intel Design Center, Haifa, Israel. (June 2004)

     
     

    "LTL Model Checking Tutorial." Intel Design Center, Haifa, Israel. (June 2004)

     
     

    "Liveness and Co-liveness." Beyond Safety - An International Workshop, Schloss Ringberg, Germany. (April 2004)

     
     

    "Research Ethics: "The Rat Race"." Undergraduate Scholars Program, Rice University, Houston, Texas. (February 2004)

     
     

    "The State of Computer Science." IBM Almaden Research, San Jose, California. (July 2004)

     
     

    "Research Ethics: "Authorship vs. Friendship"." Rice University Undergraduate Scholars Program, Houston, Texas. (January 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of Texas, Dallas, Texas. (January 2002)

     
     

    "Automated Verification = Graphs, Logic, and Automata ." 2002 Clifford Lectures, Mathematical Logic for Computer Science, Tulane University, New Orleans, Louisiana. (March 2002)

     
     

    "Designing a Peoperty Specification Language." CAD Seminar, University of California, Berkeley, California. (December 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Tel Aviv University, Israel. (August 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Department of Computer Science, Technion, Haifa, Israel. (July 2002)

     
     Other
     

    "Distinguished Lecture Series: A Logical Revolution, The Rise and Fall of Linear Temporal Logic, and Enhancing Academic Research and Scholarship. Institute of Informatics, UFRGS, Porto Alegre, Brazil." (March 2014)

     
     

    "How to Get Published. Panel for STEM Graduate Students, Rice University." (November 2014)

     
     

    "If Machines Are Capable of Doing Almost Any Work Humans Can Do, What Will Humans do? Artificial Intelligence Summit, New York." (February 2014)

     
     

    "If Machines Are Capable of Doing Almost Any Work Humans Can Do, What Will Humans do? Lunch&Learn Talk, Norway House, Houston." (February 2014)

     
     

    "If machines are capable of doing almost any work humans can do, what will humans do? Adult Education at Covenant Church, Houston." (June 2014)

     
     

    "If machines are capable of doing almost any work humans can do, what will humans do? ScienceCafe, Houston." (September 2014)

     
     

    "Philosophical Olympic Games, Federated Logic Conference." (July 2014)

     
     

    "Publication Culture in Computing Research. Colloquium, Schloss Dagstuhl, Germany." (July 2014)

     
     

    "The Ethics of Artificial Intelligence, Logic Lounge, Vienna Summer of Logic." (July 2014)

     
     

    "The Rise and Fall of Linear Temporal Logic. IIT Bombay, India." (January 2015)

     
     

    From Philosophical to Industrial Logics.  Affliated Symposium: Analysing Programs-Logic to the Rescue, 14th International Congress of Logic, Methodology and Philosophy of Science, Nancy, France, July 2011.

     
     

    Branching vs. Linear Time: A Semantical Perspective. Computer Science Colloquium,
    National University of Singapore, January 2010

     
     

    Constraints, Graphs, Logic, Algebra, and Complexity. Computer Science Colloquium,
    Weizmann Institute of Science, Rehovot, Israel, May 2010

     
     

    From Philosophical to Industrial Logics. Computer Science Colloquium, Technion,
    Haifa, Israel, June 2010

     
     

    From Philosophical to Industrial Logics. Colloquium, School of Physical and Mathematical
    Sciences, Nanyang Technical University, Singapore, January 2010

     
     

    From Philosophical to Industrial Logics. Computer Science Colloquium, Tel-Aviv
    University, Israel, April 2010

     
     

    Logic, Automata, Games, and Algorithms. Computer Science Colloquium, Interdisciplinary
    Center, Herzliya, Israel, April 2010

     
     

    P vs. NP. Computer Science Colloquium, Rice University, December 2010

     
     

    Symbolic Techniques in Propositional Satisfiability Solving. Computer Science Colloquium,
    IBM Haifa Research Lab, June 2010

     
     

    "From Philosophical to Industrial Logic." Computer Engineering Colloquium, University of Rome 1. (December 2007)

     
     

    "Research Ethics "How Much Help Is Too Much"." Rice Undergraduate Scholars Program, Rice University. (January 2007)

     
     

    "Where have all the IT jobs gone?." Computer Science Corporate Affiliate Meeting, Rice University. (September 2007)

     
     

    "Who Started the Information Revolution?." School of Continuing Studies, Rice University. (September 2007)

     
     

    "A Formal Approach to The Verification Crisis." Graduate student pizza talk, Rice University, Houston, Texas. (October f2003)

     
     

    "And Logic Begat Computer Science." Institute for Logic, Language, and Computation, University of Amsterdam, The Netherlands. (March 2003)

     
     

    "And Logic Begat Computer Science." HP High-Performance Technical Computing, Nashua, New Hampshire. (April 2003)

     
     

    "And Logic Begat Computer Science." Computer Science Department, CUNY Graduate Center, New York, NY. (January 2003)

     
     

    "And Logic Begat Computer Science." Inaugural Distinguished Lecture in Computer Science, Concordia University, Montreal, Canada. (June 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." HP High-Performance Technical Computing, Nashua, NH. (April 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Intel Design Center, Haifa, Israel. (July 2003)

     
     

    "Who Started the Information Revolution?." School of Continuing Studies, Rice University, Houston, Texas. (October 2003)

     
     

    "Who Started the Information Revolution?." School of Continuing Studies, Rice University, Houston, Texas. (November 2003)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Net IQ, Houston, Texas. (September 2002)

     
     

    "Automated Verification = Graphs, Logic, and Automata." IBM Almaden Research Center, (January 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." IBM Almaden Research Center, San Jose, California. (November 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Corporate Affiliate Meeting, Department of Computer Science, Rice University, Houston, Texas. (October 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." Intel's Israel Design Center, (July 2002)

     
     

    "On the Unusual Effectiveness of Logic in Computer Science." IBM Haifa Research Center, Haifa, Israel. (June 2002)

     
     

    "Research Ethics:." Rice University Undergraduate Scholars Program, Houston, Texas. (February 2002)

     
     

    "Rice and the Information Revolution." Rice Houston-Area Annual Alumni Meeting, Houston, Texas. (February 2002)

     
     

    "Automated Verification = Graphs, Logic, and Automata." (Invited) Bar-Ilan International Symposium on Foundations of Artificial Intelligence, Ramat Gan, Israel. (June 2001)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Department of Communication, Computer and System Sciences, University of Genoa, Genoa, Italy. (October 2001)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Five Great Lectures in Computer Science, the University of Victoria, Canada. (February 2001)

     
     

    "Branching vs. Linear Time: Final Showdown." (Invited) European Joint Conferences on Theory and Practice of Software, Genova, Italy. (April 2001)

     
     

    "Branching vs. Linear Time: Final Showdown." Microsoft Research, (January 2001)

     
     

    "CITI: Past and Future." Computer and Information Technology Institute Lunch Talk, Rice University, Houston, Texas. (May 2001)

     
     

    "CITI: The Future." Development Officers Briefing, Rice University, Houston, Texas. (June 2001)

     
     

    "Common Knowledge: Now You Have It, Now You Don't ." (Invited) Logic and Logistics: Modeling and Cross-Disciplinary Discourse, New Mexico State University, Las Cruces, New Mexico. (January 2001)

     
     

    "Designing a Property Specification Language." Weizmann Institute of Science, Rehovot, Israel. (August 2001)

     
     

    "Designing a Property Specification Language." Helsinki University of Technology, Helsinki, Finland. (August 2001)

     
     

    "Designing a Property Specification Language ." (Invited) Intel Symposium on Formal Verification, Haifa, Israel. (July 2001)

     
     

    "Erecting a Tall Building: Integrating Research and Education." Scholarly Productivity Workshop, Quality Education for Minority (QEM) Network, Texas Southern University, Houston, Texas. (March 2001)

     
     

    "Logic as the Calculus of Computer Science." NSF/CISE Workshop on the Unusual Effectiveness of Logic in Computer Science, Arlington, Virginia. (January 2001)

     
     

    "Research Ethics: "So You Wanted to be a Co-author"." Rice Undergraduate Scholars Program, Rice University, Houston, Texas. (February 2001)

     
     

    "The Information Revolution: Reality or Hype ." Society of Women Engineers, Rice University, Houston, Texas. (March 2001)

     
     

    "0-1 Laws for Fragments of Existential Second-Order Logic: A Survey (Invited)." 25th International Symposium on Mathematical Foundations of Computer Science, Bratislava, Slovak Republic. (August 2000)

     
     

    "0-1 Laws for Logics on Finite Structures." Department of Mathematics, Rice University, Houston, Texas. (December 2000)

     
     

    "0-1 Laws for Logics on Finite Structures ." Department of Mathematics, University of Houston, Houston, Texas. (November 2000)

     
     

    "A Formal Approach to the Verification Crisis." Computer and Information Technology Institute, Rice University, Houston, Texas. (February 2000)

     
     

    "A Formal Approach to the Verification Crisis." Graduate Student Pizza Talk, Rice University. (September 2000)

     
     

    "A Formal Approach to the Verification Crisis." Intel Texas Design Center, Houston, Texas. (December 2000)

     
     

    "A Formal Approach to the Verification Crisis (Short Course)." Innovation Series - IBM Austin Learning Center, Austin, Texas. (October 2000)

     
     

    "Alternation (Invited)." Advances in Modal Logic, International Conference on Temporal Logic, Leipzig, Germany. (October 2000)

     
     

    "Alternation. Advances in Modal Logic." International Conference on Temporal Logic, Leipzig, Germany. (October 2000)

     
     

    "Automata Theory: What is New Since 1959." Workshop on Model Checking and Program Analysis, Schloss Ringberg, Germany. (February 2000)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Computer Science Colloquium, Brown University. (September 2000)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Computer and Communications Research Lab, NEC, Princeton, New Jersey. (October 2000)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Informatics Colloquium, University of Edinburgh, Edinburgh, Scotland. (June 2000)

     
     

    "Automated Verification = Graphs, Logic, and Automata (Distinguished Speaker Series)." Computer and Information Sciences Department, University of Pennsylvania. (October 2000)

     
     

    "Automated Verification = Graphs, Logic, and Automata (Invited)." Journees de Verification Formelle, LIFO, University of Orleans, Orleans, France. (June 2000)

     
     

    "Automated Verification = Graphs, Logic, and Automata (Invited)." Annual Conference of the European Association for Computer Science Logic, Fischbauchau, Germany. (August 2000)

     
     

    "Common Knowledge: Now You Have It, Now You Don't." Microeconomics Seminar, Rice University. (September 2000)

     
     

    "Computer Science at Rice University." Dell Corporation, Austin, Texas. (March 2000)

     
     

    "Constraint Satisfaction and Database Theory." ENS Cachan, France. (June 2000)

     
     

    "Constraint Satisfaction and View Integration (Invited)." First International Conference on Computational Logic, London, England. (July 2000)

     
     

    "From Verification to Synthesis (Invited)." Journees de Verification Formelle, LIFO, University of Orleans, Orleans, France. (June 2000)

     
     

    "Model Checking Safety Properties." Intel Strategic CAD Lab, Hillsboro, Oregon. (January 2000)

     
     

    "Research Ethics: the Case of the Temporary Postdoc." Rice Undergraduate Scholars Program, Rice University, Houston, Texas. (February 2000)

     
     

    "The Information Revolution: Reality or Hype." Society of Women Engineers, Rice University, Houston, Texas. (April 2000)

     
     

    "The Information Revolution: Reality or Hype." 3rd Annual Rice University Forum on Global Competitiveness in the Engineering and Construction Industry, Rice University. (September 2000)

     
     

    "The Information Revolution: Reality or Hype." Jewish Business & Professional Women's Breakfast Club, Houston, Texas. (January 2000)

     
     

    "The Ultimate Temporal Specification Language (Invited)." IBM Formal Verification Summer Symposium, Israel. (August 2000)

     
     

    "Vacuity Detection in Temporal Model Checking." Intel Strategic CAD Lab, Hillsboro, Oregon. (January 2000)

     
     

    "Who Started the Information Revolution?." Ten Events that Shaped our Century, School of Continuing Studies, Rice University, Houston, Texas. (March 2000)

     
     

    "Who Started the Information Revolution?." Hebrew Speaking Professional Group, Houston, Texas. (April 2000)

     
     

    "A Formal Approach to the Verification Crisis." Graduate Student Pizza Talk, Department of Computer Science, Rice University. (November 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." IBM Austin Research Lab, Austin, Texas. (February 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Computer Science Colloquium, University of Toronto, Canada. (March 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of Cape Town, Cape Town, South Africa. (December 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of Rome, Italy. (November 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of Witwatersrand, Johanesburg, South Africa. (December 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." University of South Africa, Pretoria. (December 1999)

     
     

    "Beyond College." Rice Computer Science Club, Rice University, Houston, Texas. (November 1999)

     
     

    "Constraint Satisfaction." Computer Science Colloquium, Hebrew University, Jerusalem, Israel. (January 1999)

     
     

    "Emptiness of Tree Automata." Dagstuhl Seminar on Finite-Model Theory, Databases, and Computer-Aided Verification, Dagstuhl, Germany. (October 1999)

     
     

    "Finite-model Theory and Constraint-satisfaction Problems." IRCS/DIMACS Tutorial on Logic and Cognitive Science, University of Pennsylvania. (April 199)

     
     

    "From Boole to the Pentium." Annual Meeting of the American Association for the Advancement of Science, (January 1999)

     
     

    "From Boole to the Pentium. Symposium on the Unusual Effectiveness of Logic in Computer Science." Annual Meeting of the American Association for the Advancement of Science, (January 1999)

     
     

    "Logic and Computer-aided Verification, Mini-course." Second Pan-Hellenic Logic Symposium, Invited Presentation, Delphi, Greece. (July 1999)

     
     

    "Logic and Computer-aided Verification, Mini-course." Second Pan-Hellenic Logic Symposium, Delphi, Greece. (July 1999)

     
     

    "Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach." Fifth International AMAST Workshop on Real-Time and Probabilistic Systems, Invited Presentation, Bamberg, Germany. (May 1999)

     
     

    "The Automata-theoretic Approach to Design Verification." First Southern African Summer School and Workshop on Logic, Universal Algebra, and Theoretical Computer Science (LUATCS'99), Rand Afrikaans University, Johannesburg, South Africa. (December 1999)

     
     

    "The Complexity of Constraint-Satisfaction Problem." IRCS/DIMACS Tutorial on Logic and Cognitive Science, Invited Presentation, University of Pennsylvania. (April 1999)

     
     

    "The Descriptive Complexity of Constraint Satisfaction." Workshop in Implicit Computational Complexity, Federated Logic Conference, Invited Presentation, Trento, Italy. (July 1999)

     
     

    "The Development of the Silicon Chip." Series on Ten Events that Shaped our Century, School of Continuing Studies, Rice University, Houston, Texas. (October 1999)

     
     

    "The Information Revolution: Reality or Hype." Texas Society of CPAs Spring Accounting EXPO, Houston, Texas. (May 1999)

     
     

    "The Information Revolution: Reality or Hype." Society of Women Engineers, Rice University, Houston, Texas. (April 1999)

     
     

    "The Information Revolution: Reality or Hype." Houston Chapter of the National Council of Jewish Women, Houston, Texas. (March 1999)

     
     

    "The Mu-Calculus and Tree Automata." First Southern African Summer School and Workshop on Logic, Universal Algebra, and Theoretical Computer Science (LUATCS'99), Rand Afrikaans University, Johannesburg, South Africa. (December 1999)

     
     

    "The Quest for a Temporal Specification Language." Strategic CAD Lab, Intel, Oregon. (January 1999)

     
     

    "The Truth, the Whole Truth, and Nothing but the Truth." 6th International Workshop on Knowledge Representation Meets Databases, Invited Presentation, Linkoping, Sweden. (July 1999)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Computer Science Colloquium, Cornell University, Ithaca, New York. (October 1998)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Intel Design Center, Haifa, Israel. (October 1998)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Logic Colloquium, University of Athens, Athens, Greece. (November 1998)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Information Systems Seminar, Industrial Engineering Faculty, Technion, Israel. (December 1998)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Intel Design Center, Haifa, Israel. (July 1998)

     
     

    "Automated Verification = Graphs, Logic, and Automata." Computer Science Colloquium, New York University, New York, New York. (October 1998)

     
     

    "Automated Verification = Graphs, Logic, and Automata, Invited Presentation." Intel Symposium on Formal Verification, Portland, Oregon. (June 1998)

     
     

    "Computational Model Theory." Computer Science Colloquium, Weizmann Institute, Rehovot, Israel. (November 1998)

     
     

    "Computational Model Theory." Computer Science Colloquium, Technion, Israel. (November 1998)

     
     

    "Computational Model Theory." Computer Science Seminar, University of Athens, Athens, Greece. (November 1998)

     
     

    "Computational Model Theory, Computing Science Seminar." Uppsala University, Sweden. (November 1998)

     
     

    "Conjunctive-query Containment and Constraint Satisfaction, Invited Presentation." Workshop on Finite-Model Theory, Oberwolfach, Germany. (February (1998))

     
     

    "Design Verification: the New Frontier." Microsoft Research, (May 1998)

     
     

    "Linear Time vs. Branching Time: the Complexity-theoretic Perspective." Istituto Ricercado Scientifica e Technologica (IRST), Trento, Italy. (September 1998)

     
     

    "Linear Time vs. Branching Time: the Complexity-theoretic Perspective, Invited Presentation." 13th IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana. (June 1998)

     
     

    "Logic in the Computer Science Curriculum." 21st Century Engineering Consortium Workshop, Melbourne, Florida. (March 1998)

     
     

    "Something and Not Never Re-revisited: on Branching vs. Linear time." Computer Science Seminar, IBM Haifa Research Lab, Haifa, Israel. (November 1998)

     
     

    "Sometimes and Not Never Re-revisited: on Branching vs. LIenar Time." Istituto Ricerca Scientifica e Technologica (IRST), Trento, Italy. (September 1998)

     
     

    "Sometimes and Not Never Re-revisited: on Branching vs. Linear Time." Computer Science Seminar, IBM Haifa Research Lab, Heifa, Israel. (December 1998)

     
     

    "Sometimes and Not Never Re-revisited: on Branching vs. Linear Time, Invited Presentation." 9th International Conference on Concurrency Theory, Nice, France. (September 1998)

     
     

    "Synthesis with Incomplete Information." Logic Seminar, Cornell University, Ithaca, New York. (October 1998)

     
     

    "Temporal Logic - Finite-Model Theory vs. Automata, Invited Presentation Theory." School on Finite-Model Theory, Chennai, India. (December 1998)

     
     

    "The Digital Revolution: Reality or Hype." Dover Business Club, (March 1998)

     
     

    "The Information Revolution: Reality or Hype." Exchange Club of Sugarland, Sugarland, Texas. (June 1998)

     
     

    "The Information Revolution: Reality or Hype." Engineering Dean's Series, School of Continuing Studies, Rice University, Houston, Texas. (May 1998)

     
     

    "Verification of Open Systems." DIMACS 10th Year Anniversary, Rutgers University, New Brunswick, New Jersey. (October 1998)

     
     Panelist
     

    Reactive Synthesis. NSF Expeditions in Computer Augmented Program Engineering (ExCA PE), Kickoff Meeting,  Philadelphia, June 2012

     
     

    Starting and Running an Open Access Journal, Panel, Open Access Week, Rice
    University, October 2009

     
     Seminar Speaker
     

    A Logical Revolution. Computer Science seminar, University of Maryland, April, 2013.

     
     

    The Rise and Fall of Linear Temporal Logic. Computer Science  Seminar, lmperial College, London, UK , September 2012

     
     

    From Industrial to Philosophical Logics. Computer Science Seminar, Technical University of Graz, January 2010.

     
     

    The Tragedy of the Computing-Research Commons.  Computer Science Seminar, School of Information and Computer Science, University of California Irvine, February 1010.

     
     

    From Industrial to Philosophical Logics. Seminar, VERIMAG, Grenoble, November
    2010

     
     

    Symbolic Techniques in Propositional Satisfiability Solving. Seminar, Laboratory
    for Specification andet Verification (LSV), Cachan, France, November 2010

     
     

    Symbolic Techniques in Propositional Satisfiability Solving. Formal Verification
    Seminar, Intel Design Center, Haifa, Israel, June 2010

     
     

    Branching vs. Linear Time: A Semantical Perspective. Concurrency seminar,
    Universty of Birmingham, UK, November 2009

     
     

    From Philosophical to Industrial Logic. Computer Science Seminar, CalTech,
    February 2009

     
     

    From Verification to Synthesis. Robotics Seminar, Rice University, November 2009

     
     

    "From Philosophical to Industrial Logic." Dept. of Computer Science and Applied Mathematics, Weizmann Institute. (December 2007)

     
     

    "Logic, Automata, Games and Algorithms." School of Informatics, Edinburgh University, September 2007.

     
     

    "Where have all the IT jobs gone?." College of Science Seminar, Texas State University, San Marcos, Texas. (January 2007)

     
     

    "And Logic Begat Computer Science." Newton Institute for Mathematical Science, Cambridge, Uk. (June 2006)

     
     

    "Designing a Property-Specification Language. Research Seminar." Microsoft Research, Cambridge UK. (January 2006)

     
     

    "Logic and Algorithms, Research Seminar.." Newton Institute for Mathematical Sciences, Cambridge U<. (March 2006)

     
     

    "The Design of Propery-Specification Language." Second Incelandic Sympoium on Theoretical Computer Science, (May 2006)

     
     Workshops
     

    A Logical Revolution.  Workshop on Language, Logic, and Computation.  Tel Aviv University, Isreal, December 2012.

     
     

    Graduate Students, Marshmallows,  and  Academic Jobs.  Graduate-Traning Workshop,  Rice University,  May 2012

     
     

    Phase Transitions and Computational Complexity.  Workshop on Logical Approaches to Barriers  in Complexity.   Newton Institute, Cambridge,  UK, March 2012

     
     

    Phase Transitions and Computational Complexity.  Workshop on Finite and Algorithmic Model Theory, Les Bouches, May 2012

     
     

    To Boycott or Not to Boycott, Dagstuhl Perspective Workshop on  Publication­ Culture in Computing Research,  Schloss Dagstuhl, November 2012.

     
     

    A Multi-layered Synergistic Approach to Motion Planning with Temporal Goals.  Workshop on Formal Methods for Robotics and Automation, Snowbird, July 2011.

     
     

    Parallelism: A Siren Song? 10th International Workshop on Parallel and Distributed Methods in VerifiCation, Snowbird, July 2011.

     
     

    Logic, Databases, and Catriel Beeri. Workshop Honoring Catriel Beeri, Hebrew
    University of Jerusalem, Israel, February 2010

     
     

    "From Lowenheim to PSL." Workshop on Automata and Logic, Aachen, Germany. (December 2007)

     
    Editorial Positions
     Associate Editor, Electronic Notes in Theoretical Computer Science. (2009 - 2009)

     Editor in Chief, Communications of the ACM. (2008 - 2008)

     Editor in Chief, Communications of the ACM. (2009 - 2009)

     Editor in Chief, Communications of the ACM. (2010 - 2010)

     Editor in Chief, Communications of ACM. (2008 - 2014)

     Other, International Journals on Software Tools for Technology Transfer. (2010 - 2010)

     Other, Logical methods on Computer Science. (2010 - 2010)

     Other, International Journals on Software Tools for Technology Transfer. (2008 - 2008)

     Other, International Journals on Software Tools for Technology Transfer. (2009 - 2009)

     Other, Logical methods on Computer Science. (2008 - 2008)

     Other, Logical methods on Computer Science. (2009 - 2009)

     Other, Logical Methods on Computer Science. (2004 - 2014)

     Associate Editor, J. of Computer and System Sciences. (2008 - 2008)

     Associate Editor, J. of Computer and System Sciences. (2010 - 2010)

     Associate Editor, Chicago J. of Theoretical Computer Science. (2008 - 2008)

     Associate Editor, J. of Computer and System Sciences. (2009 - 2009)

     Associate Editor, Chicago J. of Theoretical Computer Science. (2009 - 2009)

     Associate Editor, Chicago J. of Theoretical Computer Science. (2010 - 2010)

     Associate Editor, Electronic Notes in Theoretical Computer Science. (2010 - 2010)

     Associate Editor, Information and Computation. (2008 - 2008)

     Associate Editor, Information and Computation. (2009 - 2009)

     Associate Editor, Information and Computation. (2010 - 2010)

     Associate Editor, Electronic Notes in Theoretical Computer Science. (2008 - 2008)

     Associate Editor, Information and Computation. (2005 - 2005)

     Associate Editor, Information and Computation. (2003 - 2003)

     Associate Editor, Information and Computation. (2007 - 2007)

     Editor, Formal Techniques for Networked and Distributed Systems - FORTE 2002, Proceedings of the 22nd IFIP WG 6.1 International Conference. Springer-Verlag, Lecture Notes in Computer Science 2529. (2002 - 2002)

     Associate Editor, Journal of Computer and System Science. (2005 - 2005)

     Associate Editor, Information and Computation. (2002 - 2002)

     Associate Editor, J. of Computer and System Sciences. (2007 - 2007)

     Associate Editor, Journal of Computer and System Sciences. (2003 - 2003)

     Member of the Editorial Board, SIAM Journal on Computing. (2005 - 2005)

     Associate Editor, Journal of Computer and System Sciences. (2002 - 2002)

     Associate Editor, Chicago Journal of Theoretical Computer Science. (2003 - 2003)

     Associate Editor, Chicago J. of Theoretical Computer Science. (2007 - 2007)

     Member of the Editorial Board, SIAM J. on Computing. (2007 - 2007)

     Member of the Editorial Board, SIAM Journal on Computing. (2003 - 2003)

     Associate Editor, Chicago Journal of Theoretical Computer Science. (2002 - 2002)

     Associate Editor, Formal Methods in System Design. (2005 - 2005)

     Other, Logical Methods on Computer Science. (2005 - 2005)

     Associate Editor, Formal Methods in System Design. (2003 - 2003)

     Associate Editor, Formal Methods in System Design. (2007 - 2007)

     Member of the Editorial Board, SIAM Journal on Computing. (2002 - 2002)

     Associate Editor, Formal Methods in System Design. (2007 - 2007)

     Associate Editor, Formal Methods in System Design. (2002 - 2002)

     Other, International Journals on Software Tools for Technology Transfer. (2003 - 2003)

     Other, International Journals on Software Tools for Technology Transfer. (2007 - 2007)

     Other, International Journals on Software Tools for Technology Transfer. (2002 - 2002)

     Associate Editor, Electronic Notes in Theoretical Computer Science. (2007 - 2007)

     Associate Editor, Electronic Notes in Theoretical Computer Science. (2002 - 2002)

     Member of the Editorial Board, Lecture Notes in Computer Science, Springer-Verlag. (2007 - 2007)

     Other, Logical Methods on Computer Science. (2007 - 2007)

     Editor in Chief, CACM. (2007 - 2007)

    Supervised Theses & Dissertations
     Dorai Sitaram, Doctor of Philosophy Models of Control and Their Implications for Programming Language Design. (1994) (Thesis Committee Member)

     Donald G. Baker, Doctor of Philosophy Memento: A Collaborative, Semantic-Based Infrastructure for Building Assistant Applications. (1997) (Thesis Committee Member)

     Sameer Siruguri, Master of Science Tracking the Evolution of Learning on a Visualmotor Task. (2001) (Thesis Committee Member)

     Rajarshi Bandyopadhyay, Master of Science Predicting protein-protein interactions from primary structure. (2002) (Thesis Committee Member)

     Guoqiang Pan, Master of Science BDD-Based Decision Procedures for Modal Logic K. (2003) (Thesis Director)

     Spiridon Tsavachidis, Master of Science Eliminating Incoherence from Subjective Estimates of Chance. (2003) (Thesis Director)

     Demetrios D. Demopoulos, Master of Science Probabilistic Phenomena in Random Comdinatorial. (2003) (Thesis Director)

     James I. Hsia, Master of Science Adding Support for Language Levels to DrJava. (2004) (Thesis Committee Member)

     Stephan J. Ellner, Master of Science PreVIEW: An Untyped Graphical Calculus for Resource-aware Programming. (2004) (Thesis Committee Member)

     Deian Tabakov, Master of Science Experimental Evaluation of Explicit and Symbolic Automata-Theoretic Algorithms. (2005) (Thesis Director)

     Xiaoxu Wang, Master of Science Analysis of the Assignment Landscape of 3-SAT Problems. (2005) (Thesis Director)

     Brian Chen, Doctor of Philosophy Geometry-based Methods for Protein Function Prediction. (2006) (Thesis Committee Member)

     Guoqiang Pan, Doctor of Philosophy Complexity and Structural Heuristics for Propositional and Quantified Satisfiability. (2006) (Thesis Director)

     Seth Fogarty, Master of Science Buchi Containment and Size-Change Termination. (2008) (Thesis Director)

     Roni Wiener, M.S. Intelligate: An Algorithm for Learning Boolean Functions for Dynamic Power Reduction. (2008) (Thesis Director)

     Erion Plaku, Doctor of Philosophy From High-Level Tasks to Low-Level Motions: Motion Planning for High-Domensional Nonlinear Hybrid Robotic Systems. (2008) (Thesis Committee Member)

     Derek Ruths, Doctor of Philosophy Deriving Executable Models of Biochemical Network Dynamics from Qualitative Data. (2009) (Thesis Committee Member)

     Sumit Nain, Master of Science Linear vs. Branching Time: A Semantical Perspective. (2009) (Thesis Director)

     Scott Alexander Crosby, Doctor of Philosophy Efficient Tamper-Evident Data Structures for Untrusted Servers. (2010) (Thesis Committee Member)

     Yousra Alkabani, Doctor of Philosophy N-variant Hardware Design. (2010) (Thesis Committee Member)

     Deian Tabakov, Doctor of Philosophy Dynamic Assertion-Based Verification for SystemsC. (2011) (Thesis Director)

     Kristin Yvonne Rozier, Doctorate of Philosophy Explicit or Symbolic Transltion of Linear Temporal Logic to Automata. (2013) (Thesis Director)

     Seth Fogarty, Doctoral Riichi Automata as Specifications for Reactive Systems. (2013) (Thesis Director)

     Kuldeep Meel, Masters Sampling Techniques for Boolean Satisfiablility. (2014) (Thesis Director)

     Sailesh Prabhu, Masters Sampling-Based Approach to the Integrated Task and Motion Planning Problem. (2014) (Thesis Committee Member)

     Sumit Nain, Ph.D Synthesis from Probabilistic Components. (Thesis Director)

    Awards, Prizes, & Fellowships
     Distinguished Scientist Award, Southeastern Universities Research Association's (April, 2013)

     European Association of Theoretical Computer Science, Distinguished Achievements Award (July 2012)

     ACM Outstanding Contribution Award, ACM (April 2010)

     American Academy of Arts and Sciences, Member, American Academy of Arts and Sciences (April 2010)

     Computing Research Association, Distinguished Service Award, Computing Research Association (February 2010)

     EATCS Award for Best ETAPS Paper, EATCS (March 2009)

     Outstanding Contributions to ACM Award,

     Computing Research Association - Distinguished Service Award,

     IEEE Fellow, IEEE (January 2009)

     American Academy of Arts & Science - Fellow,

     ACM Presidential Award, (June 2008)

     The ACM PODS Alberto O. Mendelzon Test-of-Time-Award (w/P.Kolaitis), (June 2008)

     Blaise Pascal Medal, European Academy of Sciences, (November 2008)

     ACM SIGMOD Edgar F. Codd Innovations Award, (June 2008)

     Foreign member, Academia Europaea, (April 2007)

     IEEE Symp. on Logic in Computer Science Test-of-Time Award, W.P. Wolper (August 2006)

     ACM Paris Kanellakis Award, W.G. Holzmann, R. Kurshan, and P. Wolper (May 2006)

     LICS Test-of-Time, IEEE (2006)

     Guggenheim Fellow, John Simon Guggenheim Memorial Foundation (May 2005)

     Paris Kanellakis Theory and Practice, ACM (2005)

     Fellow, American Association for Artificial Intelligence (July 2004)

     AAAS Fellow, American Association for the Advancement of Science (2002)

     Doctor Honoris Causa, accompanied by a special symposium, Saarland University, Germany (March 2002)

     Member, European Academy of Sciences (2002)

     Member, U.S. National Academy of Engineering (2002)

     Doctor Honoris Causa, Orleans University (2002)

     Meeting, Led and Organized, NSF/CISE Workshop on the Unusual Effectiveness of Logic in Computer Science, Arlington, Virginia (January 2001)

     Board Member, European Association for Computer Science Logic (August 1997 to present)

     Member, Organizing Committee, IEEE Symposium on Logic in Computer Science (June 1991 to present)

     Member, Board of Directors, Theoretical Aspects of Reasoning about Knowledge, Inc. (1991 to present)

     Program Committee, 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, (2001)

     Program Committee, 8th International Conference on Database Theory (2001)

     Research Evaluation Committee, Department of Computer Science, Aalborg University, Denmark (January 2001)

     Program Committee, 8th International Symposium on Temporal Representation and Reasoning, (2001)

     Program Committee, 5th Annual Conference of the European Association for Computer Science Logic, (2001)

     Program Committee, 8th International Workshop on Knowledge Representation Meets Databases, (2001)

     Program Committee, Joint Workshop on Process Algebra and Performance Modelling and Probabilistic Methods in Verification, (2001)

     Program Committee, 3rd ACM Conference on Electronic Commerce, (2001)

     Program Committee, International Joint Conference on Automated Reasoning, (2001)

     Computer Science Advisory Committee, Worcester Polytechnic Institute (January 1999 to present)

     Oversight Committee, Master's Program in Logic and Algorithms, University of Athens, Greece (April 1997 to present)

     Award Committee, ACM Kanellakis Award Theory and Practice (1996 to present)

     Steering Committee Chair, Federated Conference (2002)

     General Chair, 8th International SPIN Workshop on Model Checking of Software (2001)

     Program Committee, 8th International Conference on Database Theory (2001)

     Program Committee, 17th International Conference on Automated Deduction (June 2000)

     Program Committee, 19th ACM Symposium on Principles of Database Systems (May 2000)

     Program Committee, Conference on Foundations of Software Science and Computation Structures (March 2000)

     Program Committee, 6th International Symposium on Artificial Intelligence and Mathematics (January 2000)

     ACM Fellow, (May 2000)

     Godel Prize, (May 2000)

     Workshop Co-organizer, Model Checking and Program Analysis (February 2000)

     Visiting Faculty, Intel Design Center, Haifa, Israel (June - August 2000)

     Visiting Professor, Laboratoire d'Informatique Fondamentale d'Orleans, University of Orleans, France (May, June 2000)

     Program Committee, 7th International SPIN Workshop on Model Checking of Software (August 2000)

     Program Committee, Annual Conference of the European Association for Computer Science Logic (August 2000)

     Steering Committee Chair, Federated Logic Conference (July 2002)

     Program Committee, 11th International Conference on Concurrency Theory (August 2000)

     Workshop Co-organizer, Dagstuhl Seminar on Probabilistic Methods in Verification (May 2000)

     Hiring Committee, Department of Computer Science, University of Cyprus, Greece (2000)

     Computer Science Advisory Committee, Worcester Polytechnic Institute, Massachusetts (1999 - present)

     Panel member, NSF Career Panel, Computer and Commuinication Research (October 2000)

     Program Committee, 5th International Conference on Logic Programming and Nonmonotonic Reasoning, El Paso, Texas (December 1999)

     Member, Board of Directors, Theoretical Aspects of Reasoning about Knowledge, Inc. (1991 to present)

     Symposium Organizer, Annual Meeting of the American Association for the Advancement of Science (January 1999)

     Program Committee, 6th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (January 2000)

     ACM Fellow, Association for Computing Machinery (1999)

     Steering Committee Chair, Federated Logic Conference (July 1999)

     Workshop Co-organizer, Dagstuhl Seminar on Finite-Model Theory, Databases, and Computer-Aided Verification (October 1999)

     Workshop Co-organizer, IRCS/DIMACS Tutorial and Workshop on Logic and Cognitive Science: Linking Finite Model Theory, Descriptive Complexity, and the Study of Cognition, Uni (April 1999)

     Program Committee, 6th Workshop on Logic, Language, Information and Computation, Rio de Janeiro, Brazil (May 1999)

     Computer Science Advisory Committee, Worcester Polytechnic Institute (January 1999 to present)

    Positions Held
     Panel, member, 9th Joint Meeting of European Software Engineering Conf.. (2013 - 2013)

     Dissertation Committee for Ruediger Ehlers, Saarlands University. (2013 - 2013)

     Program co-chair, 1st Int'l Workshop on Strategic Reasoning, Rome, Italy. (2013 - 2013)

     General Chair, 9th International SPIN Workshop on Model Checking of Software. (2002 - 2002)

     Panel Moderator: Educational Responce to Offshoring., 37th ACM Symp.on Computer Science Education. (2006 - 2006)

     Associate Editor, Information and Computation. (2008 - 2008)

     Steering Committee Chair, Federated Logic Conference. (2002 - 2002)

     Associate Editor, Journal of Computer and System Sciences. (2008 - 2008)

     Panel Member: Automata Theory-Its Relevamce to Computer Science, Student and Course Contents., 37th ACM Symp. on Computer Science Education.. (2006 - 2006)

     Associate Editor, Chicago Journal of Theoretical Computer Science. (2008 - 2008)

     Workshop Co-organizer, Workshop on Learning and Formal Verification - in Honor of Eli Shamir. (2002 - 2002)

     Co-director, Special Programme on Logic and Algorithms, Isaac Newton Institute for Mathematical Science, Cambridge. (2006 - 2006)

     Symposium Chair, GCC/Keck Bioinformatics 2002. (2002 - 2002)

     Workshop on Comstraints and Verification, Isaac Newton Institute for Mathematical Science, Cambridge, UK. (2006 - 2006)

     Advisory Board, International Journals on Software Tools for Technology Transfer. (2008 - 2008)

     Associate Editor, Electronic Notes in Theoretical Computer Science. (2008 - 2008)

     Local Organizer, 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and distributed systems. (2002 - 2002)

     General Chair,, 4th Federated Logic Conference, Seattle. (2006 - 2006)

     Managing Editor, Logical Methods on Computer Science. (2008 - 2008)

     Editor in Chief, Communications of ACM. (2008 - 2008)