TSD 2015
5th Tsinghua Software Day
               
 Home  Invited Speakers  Lectures  Program  Local Infomation  Contact Us  
               
Moshe Vardi

Moshe Vardi

Rice University, USA

Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology Institute at Rice University. He is the co-recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, and the Southeastern Universities Research Association's Distinguished Scientist Award. He is the author and co-author of over 500 papers, as well as two books: "Reasoning about Knowledge" and "Finite Model Theory and Its Applications". He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, and the Institute for Electrical and Electronic Engineers. He is a member of the US National Academy of Engineering, the American Academy of Arts and Science, the European Academy of Science, and Academia Europea. He holds honorary doctorates from the Saarland University in Germany and Orleans University in France. He is the Editor-in-Chief of the Communications of the ACM.
Jos Meseguer

Jos Meseguer

University of Illinois at Urbana Champaign, USA

Jose Meseguer received his Ph.D. in Mathematics from the University of Zaragoza, Spain. He is Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC). Prior to moving to UIUC he was a Principal Scientist at SRI International, where he worked from 1980 to 2001 after having held postdoctoral positions at the University of California at Berkeley and IBM Research. He was also an Initiator Member of Stanford University's Center for the Study of Language and Information (CSLI).

Meseguer has made fundamental contributions in the frontier between mathematical logic, executable formal specification and verification, declarative programming languages, programming methodology, programming language semantics, concurrency, and security. His work in all these areas, comprising over 350 publications, is very highly cited. His contributions to security include fundamental concepts such as nointerference, browser security verification, new algorithms and verification techniques to defend systems against Denial of Service (DoS) attacks, and new symbolic techniques to analyze cryptographic protocols modulo complex algebraic properties that have been embodied in the Maude-NPA Protocol Analyzer. He is the creator of rewriting logic, a very flexible computational logic to specify concurrent systems. The 2012 rewriting logic bibliography has about 1,000 publications The Maude rewriting logic language is one of the most advanced and efficient executable formal specification languages worldwide. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. It is also an advanced declarative concurrent language with sophisticated object-oriented features and powerful module composition and reflective meta-programming capabilities. He, his collaborators, and other researchers have used Maude and its tool environment to build sophisticated systems and tools, and to specify and analyze many systems, including cryptographic protocols, network protocols, web browsers, cyber-physical systems, models of cell biology, executable formal semantics of programming and software modeling languages, formal analyzers for conventional code, theorem provers, and tools for interoperating different formal systems. Meseguer has given numerous invited lectures at international scientific meetings and has taught advanced courses on his research at leading American, British, German, Spanish, Italian, and Japanese universities and research centers. He has also served in numerous program committees of international scientific conferences and as editor of various scientific journals.

Prakash Panangaden

Prakash Panangaden

McGill University, Canada

Many software systems are embedded real-time systems which interact with physical sensors and actuators. These devices are noisy and one is forced to reason probabilistically. Just as one has logical formalisms for reasoning about correctness, one has very closely related formalisms for reasoning about programs where the inputs are described by probability distributions and the programs are essentially transforming probabilities. I will introduce some basic probability ideas: conditional probability and conditional expectation. I will explain what Markov kernels are and argue that they are the probabilistic analogues of binary relations. Then I will describe how to reason about simple while programs with probabilistic inputs. One area where probability is used extensively is modern AI and especially machine learning. I will describe Bayes nets which are a ba- sic tool in probabilistic AI: a Turing Award was given to Judea Pearl in 2012 for his contributions to this field. I will close with a description of programming languages being designed for machine learning applications.
Vincent Danos

Vincent Danos

CNRS, France & University of Edinburgh, UK

Vincent Danos graduated from University Paris Diderot in Mathematical Logic, and became shortly after a CNRS Researcher. His research then moved to concurrency based on the linear Logic model. Biological processes were a natural area where to put these ideas into practice. Vincent spent 3 years at Harvard medical School as an invited Professor. He then took an appointment of full Professor at the University of Edimburgh, in both the Computer Science Department, and in the Biology Department where he holds the chair of computational biology.