David Basin, ETH Zurich Policy Monitoring in First-order Temporal Logic Abstract: In security and compliance, it is often necessary to ensure that agents and systems comply to complex policies. An example from financial reporting is the requirement that every transaction t of a customer c, who has within the last 30 days been involved in a suspicious transaction t', must be reported as suspicious within 2 days. We present an approach to monitoring such policies formulated in an expressive fragment of metric first-order temporal logic. We also report on case studies in security and compliance monitoring and use these to evaluate both the suitability of this fragment for expressing complex, realistic policies and the efficiency of our monitoring algorithm. (Joint work with Felix Klaedtke and Samuel Mueller) Bio: David Basin has the chair for Information Security at the Department of Computer Science, ETH Zurich, since 2003. He is also the director of the ZISC, the Zurich Information Security Center. He received his Ph.D. from Cornell University in 1989, and his Habilitation from the University of Saarbruecken in 1996. His appointments include a postdoctoral research position at the University of Edinburgh (1990-1991), and a senior research position within the Max-Planck-Institut fuer Informatik (1992-1997). From 1997-2002 he was a full professor at the University of Freiburg, where he held the chair for software engineering. His research focuses on information security, in particular methods and tools for modeling, building, and validating secure and reliable systems. He serves on the editorial boards of numerous journals including IEEE Transactions on Dependable and Secure Computing and Acta Informatica. He is also Editor-in-Chief of Springer-Verlag's book series in Information Security and Cryptography. J Strother Moore University of Texas at Austin Theorem Proving for Verification: The Early Days Abstract: Since Turing, computer scientists have understood that the question ``does this program satisfy its specifications?'' could be reduced to the question ``are these formulas theorems?'' But the theorem proving technology of the 50s and 60s was inadequate for the task. In 1971, here in Edinburgh, Boyer and I started building the first general-purpose theorem prover designed for a computational logic. This project continues today, with Matt Kaufmann as a partner; the current version of the theorem prover is ACL2 (A Computational Logic for Applicative Common Lisp). In this talk I'll give a highly personal view of the four decade long ``Boyer-Moore Project,'' including our mechanization of inductive proof, support for recursive definitions, rewriting with previously proved lemmas, integration of decision procedures, efficient representation of logical constants, fast execution, and other proof techniques. Along the way we'll see several interesting side roads: the founding of the Edinburgh school of logic programming, a structure-shared text editor that played a role in the creation of Word, and perhaps most surprisingly, the use of our ``Lisp theorem prover'' to formalize and prove theorems about commercial microprocessors and virtual machines via deep embeddings, including parts of processors by AMD, Centaur, IBM, Motorola, Rockwell-Collins, Sun, and others. The entire project helps shed light on the dichotomy between general-purpose theorem provers and special-purpose analysis tools. Bio: J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin. He is the author of many books and papers on automated theorem proving and mechanical verification of computing systems. Along with Boyer he is a co-author of the Boyer-Moore theorem prover and the Boyer-Moore fast string searching algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem prover. Moore got his PhD from the University of Edinburgh in 1973 and his SB from MIT in 1970. Moore was a founder of Computational Logic, Inc., and served as its chief scientist for ten years. He served as chair of the UT Austin CS department for eight years. He and Bob Boyer were awarded the McCarthy Prize in 1983 and the Current Prize in Automatic Theorem Proving by the American Mathematical Society in 1991. In 1999, they were awarded the Herbrand Award for their work in automatic theorem proving. Boyer, Moore, and Kaufmann were awarded the 2005 ACM Software Systems Award for the Boyer-Moore theorem prover. Moore is a Fellow of both the American Association for Artificial Intelligence and the ACM and is a member of the US National Academy of Engineering. Georg Gottlob, Oxford University, UK Datalog+-: A Family of Logical Query Languages for New Applications Abstract: I will report on a recently introduced family of Datalog-based languages, called Datalog+-, which is a new framework for tractable ontology querying, and for a variety of other applications. Datalog+-extends plain Datalog by features such as existentially quantified rule heads, and, at the same time, restricts the rule bodies so to achieve decidability and tractability. I will review a number of theoretical results and show how Datalog+- relates to both Database Dependency Theory and the Guarded Fragment of first order logic. I will show that popular tractable description logics translate into Datalog+- and illustrate how this formalism can be used in the context of web data extraction, data exchange, and other applications. Bio: Georg Gottlob is a Professor of Computing Science at Oxford University and an Adjunct Professor at TU Wien. His interests include data extraction, database theory, graph decomposition techniques, AI, knowledge representation, logic and complexity. Gottlob has received the Wittgenstein Award from the Austrian National Science Fund, is an ACM Fellow, an ECCAI Fellow, and a member of the Austrian Academy of Sciences, the German National Academy of Sciences, and the Academia Europaea. He chaired the Program Committees of IJCAI 2003 and ACM PODS 2000, was the Editor in Chief of the Journal Artificial Intelligence Communications, and is currently a member of the editorial boards of journals, such as CACM and JCSS. He is the main founder of Lixto, a company that provides tools and services for web data extraction. Homepage: http://web.comlab.ox.ac.uk/people/Georg.Gottlob/ David Harel, Weizmann Institute of Science "Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's" Bio: David Harel has been at the Weizmann Institute of Science in Israel since 1980. He was Department Head from 1989 to 1995, and was Dean of the Faculty of Mathematics and Computer Science between 1998 and 2004. He was also co-founder of I-Logix, Inc. He received his PhD from MIT in 1978, and has spent time at IBM Yorktown Heights, and sabbaticals at Carnegie-Mellon, Cornell, and the University of Edinburgh. In the past he worked mainly in theoretical computer science (logic, computability, automata, database theory), and he now works mainly on software and systems engineering and on modeling biological systems. He is the inventor of statecharts and co-inventor of live sequence charts, and co-designed Statemate, Rhapsody and the Play-Engine. Among his awards are the ACM Karlstrom Outstanding Educator Award (1992), the Israel Prize (2004), the ACM Software System Award (2007), and three honorary degrees. He is a Fellow of the ACM, the IEEE and the AAAS, and was elected to the Academia Europaea. Deepak Kapur, The University of New Mexico Induction, Invariants, and Abstraction Abstract: Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas in inductive reasoning is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, inductive reasoning, and generating invariants is investigated. Deepak Kapur is a distinguished professor of computer science at the University of New Mexico at Albuquerque. From 1998 until 2006, he served as the chair of the computer science department there. He has conducted research in areas of automated deduction, induction theorem proving, term rewriting, unification theory, formal methods, algebraic and geometric reasoning and their applications. His group built one of the first rewrite-based theorem provers, called Rewrite Rule Laboratory. He served as the editor-in-chief of the Journal of Automated Reasoning from 1993-2007. He is on the editorial board of Journal of Symbolic Computation and other journals. He received the Herbrand Award for distinguished contributions to automated reasoning in 2009. Gordon Plotkin, University of Edinburgh Robin Milner, a Craftsman of Tools for the Mind Bio: Gordon Plotkin obtained his BSc, in Mathematics and Physics, from Glasgow University, in 1967, and his PhD, in Artificial Intelligence, from Edinburgh University, in 1972. He then joined the faculty at Edinburgh, becoming a full professor in 1986. He is a Fellow of the Royal Society, a member of Academia Europaea, and a Fellow of the Royal Society of Edinburgh, and has held visiting positions at Syracuse, Stanford, Orsay, INRIA, Aarhus,  MIT, ENS, Paris 7, DEC SRC, ETL, and Microsoft. His research contributions include work on hypothesis discovery, theorem proving, situation theory, non-standard logics, and category theory, but he may be best known for his work on the semantics and logic of programming languages, with contributions to operational semantics, logical frameworks, concurrency, domain theory, security, type theory, lambda calculus, full abstraction, abstract syntax, nondeterminism and probabilistic computation. His current interests include the theory of algebraic computational effects and computational systems biology.