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
Ken Kennedy Institute for Information Technology
Email: vardi@rice.edu
Phone: 713-348-5977
Office: Duncan Hall 3131
http://www.cs.rice.edu/~vardi/
|
 |
Moshe Y. Vardi
Karen Ostrum George Professor of Computational Engineering and Professor of Computer Science
Applications of logic to computer science: database systems, complexity theory, multi-agent systems, and specification and verification of hardware and software
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.
Selected Publications
Articles
Pistore, M., and Vardi, M.Y. "The Planning Spectrum - One, Two, Three, Infinity." J. AI Research, 30 (2007): 101-132.(Published)
Sebastiani, R., Singerman, E., Tonetta, S., Vardi, M.Y. "GSTE Is Partitioned Model Checking." Formal Methods in System Design, 31 (2007): 177-196.(Published)
Vardi, M.Y., Wilke, T. "Automata - from logic to algorithms." Logic and Automata - History and Perspectives (2007).(Published)
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).(Published)
Conference papers
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.(Published)
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).(Published)
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.(Published)
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.(Published)
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.(Published)
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.(Published)
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.(Published)
Refereed Articles
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.(Published)
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.(Published)
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.(Published)
Refereed Conference Papers
E. Friedgut, O. Kupferman, M.Y. Vardi "Buchi Complementation Made Tighter." Int'l J. of Foundations of Computer Science, 17:4 (2006): 851-867.(Published)
M.Y. Vardi "Automata-Theoretic techniques for Temporal Reasoning." In Handbook of Modal Logic (2006): 971-989.(Published)
Other
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.(Published)
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.(Published)
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.(Published)
Vardi, M.Y. "A logical approach to constrant satisfaction." Complexity of Constraints (2008): 125-155.(Published)
Vardi, M.Y. "CACM - past, present, and future." Commun. ACM, 51(1) (2008): 44-48.(Published)
Vardi, M.Y. "From Church and Prior to PSL." 25 MC Festschrift (2008): 150-171.(Published)
Vardi, M.Y. "From monadic logic to PSL." Pillas of Computer Science (2008): 656-681.(Published)
Vardi, M.Y. "Let us-together-make CACM exciting." Commun. ACM, 51(10) (2008): 5.(Published)
Vardi, M.Y. "Where do you come from? and where are you going?." Commun, 51(7) (2008): 5.(Published)
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.(Published)
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.(Published)
Vardi, M.Y. "Formal techniques for SystemC verification." Proc. 44th ACM/IEEE Design Automation Conference (2007): 188-192.(Published)
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.(Published)
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.(Published)
Theses
Derek Ruths, Doctor of Philosophy. "Deriving Executable Models of Biochemical Network Dynamics from Qualitative Data." (2009).(Committee Member)
Sumit Nain, Master of Science. "Linear vs. Branching Time: A Semantical Perspective." (2009).(Thesis or Dissertation Director)
Erion Plaku, Doctor of Philosophy. "From High-Level Tasks to Low-Level Motions: Motion Planning for High-Domensional Nonlinear Hybrid Robotic Systems." (2008).(Committee Member)
Roni Wiener, M.S. "Intelligate: An Algorithm for Learning Boolean Functions for Dynamic Power Reduction." (2008).(Thesis or Dissertation Director)
Seth Fogarty, Master of Science. "Buchi Containment and Size-Change Termination." (2008).(Thesis or Dissertation Director)
Brian Chen, Doctor of Philosophy. "Geometry-based Methods for Protein Function Prediction." (2006).(Committee Member)
Guoqiang Pan, Doctor of Philosophy. "Complexity and Structural Heuristics for Propositional and Quantified Satisfiability." (2006).(Thesis or Dissertation Director)
Deian Tabakov, Master of Science. "Experimental Evaluation of Explicit and Symbolic Automata-Theoretic Algorithms." (2005).(Thesis or Dissertation Director)
Xiaoxu Wang, Master of Science. "Analysis of the Assignment Landscape of 3-SAT Problems." (2005).(Thesis or Dissertation Director)
James Hsia, Master of Science. "Adding Support for Language Levels to DrJava." (2004).(Committee Member)
Stephan Ellner, Master of Science. "PreVIEW: An Untyped Graphical Calculus for Resource-aware Programming." (2004).(Committee Member)
Demetrios Demopoulos, Master of Science. "Probabilistic Phenomena in Random Comdinatorial." (2003).(Thesis or Dissertation Director)
Guoqiang Pan, Master of Science. "BDD-Based Decision Procedures for Modal Logic K." (2003).(Thesis or Dissertation Director)
Spiridon Tsavachidis, Master of Science. "Eliminating Incoherence from Subjective Estimates of Chance." (2003).(Thesis or Dissertation Director)
Rajarshi Bandyopadhyay, Master of Science. "Predicting protein-protein interactions from primary structure." (2002).(Committee Member)
Sameer Siruguri, Master of Science. "Tracking the Evolution of Learning on a Visualmotor Task." (2001).(Committee Member)
Zijiang Yang, Masters. "Performance Analysis of Symbolic Reachability Algorithms in Model Checking." (1999).
Donald Baker, Doctor of Philosophy. "Memento: A Collaborative, Semantic-Based Infrastructure for Building Assistant Applications." (1997).(Committee Member)
Dorai Sitaram, Doctor of Philosophy. "Models of Control and Their Implications for Programming Language Design." (1994).(Committee Member)
|
