Invited Talks

Jump to: Plenary and Keynotes · Conference invited talks · Workshop invited talks


Plenary and Keynote Invited Talks

All these talks will be held in the George Square Lecture Theatre, and are freely open to members of the public.

Sunday, July 11th

14:00‑14:30 Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
David Harel (Weizmann Institute of Science)
plenary
14:30‑15:00 Robin Milner, a Craftsman of Tools for the Mind.
Gordon Plotkin (University of Edinburgh)
plenary

Tuesday, July 13th

09:00‑10:00 Datalog+-: A Family of Logical Query Languages for New Applications.
Georg Gottlob (University of Oxford)
plenary
14:00‑15:00 Theorem Proving for Verification: The Early Days.
J Strother Moore (University of Texas)
keynote

Friday, July 16th

09:00‑10:00 Policy Monitoring in First-order Temporal Logic.
David Basin (ETH Zurich)
plenary

Sunday, July 18th

14:00‑15:00 Induction, Invariants, and Abstraction.
Deepak Kapur (University of New Mexico)
keynote


Abstracts and short Biographies of the Speakers


David Basin (ETH Zurich)

Friday July 16th, 9:00-10:00 - George Square Lecture Theatre.

Policy Monitoring in First-order Temporal Logic.

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)

Biography

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.


Georg Gottlob (University of Oxford)

Tuesday July 13th, 9:00-10:00 - George Square Lecture Theatre.

Datalog+-: A Family of Logical Query Languages for New Applications.

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.

Biography

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.


David Harel (Weizmann Institute of Science)

Sunday July 11th, 14:00-14:30 - George Square Lecture Theatre.

Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.

Biography

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 (University of New Mexico)

Sunday July 18th, 14:00-15:00 - George Square Lecture Theatre.

Induction, Invariants, and Abstraction.

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.

Biography

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.


J Strother Moore (University of Texas)

Tuesday July 13th, 14:00-15:00 - George Square Lecture Theatre.

Theorem Proving for Verification: The Early Days.

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.

Biography

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.


Gordon Plotkin (University of Edinburgh)

Sunday July 11th, 14:30-15:00 - George Square Lecture Theatre.

Robin Milner, a Craftsman of Tools for the Mind.

Biography

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.

Conference invited talks

Sunday, July 11th

09:00-10:00 The Big Deal: Applying Constraint Satisfaction Technologies Where It Makes the Difference
Yehuda Naveh
SAT invited talk
14:00‑14:30 Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
David Harel (Weizmann Institute of Science)
FLoC plenary talk
14:30‑15:00 Robin Milner, a Craftsman of Tools for the Mind.
Gordon Plotkin (University of Edinburgh)
FLoC plenary talk

Monday, July 12th

09:00-10:00 A Formally Verified OS Kernel. Now What?
Gerwin Klein
ITP invited talk
09:00-10:00 The Fine Print of Security
Martin Abadi
LICS invited talk
09:00-10:00 Automata for Data Words and Data Trees
Mikolaj Bojanczyk
RTA invited talk
09:00-10:00 Exact Algorithms and Complexity
Ramamohan Paturi
SAT invited talk
14:00-15:00 Realising Optimal Sharing
Vincent van Oostrom
RTA invited talk

Tuesday, July 13th

09:00‑10:00 Datalog+-: A Family of Logical Query Languages for New Applications.
Georg Gottlob (University of Oxford)
FLoC plenary talk
14:00‑15:00 Theorem Proving for Verification: The Early Days.
J Strother Moore (University of Texas)
FLoC keynote talk

Wednesday, July 14th

09:00‑10:00 Proof Assistants as Teaching Assistants: A View from the Trenches
Benjamin C. Pierce
ITP invited talk
09:00‑10:00 Probabilistic Information Flow
Catuscia Palamidessi
LICS invited talk
09:00‑10:00 A Primer on the Algorithmic Aspects of Satisfiability Modulo Theories
Daniel Kroening
SAT invited talk
14:00-15:00 Abstracting the ODE semantics of rule-based models: exact and automatic model reduction
Vincent Danos
LICS invited talk

Thursday, July 15th

09:00‑11:00 ABC: An Academic Industrial-Strength Verification Tool
Robert Brayton
CAV Tutorial 1
11:00‑12:30 Software Model Checking (TBC)
Ken McMillan
CAV Tutorial 2
14:00‑16:00 There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
Thomas Reps
CAV Tutorial 3
16:00‑17:30 Constraint Solving for Program Verification: Theory and Practice by Example
Andrey Rybalchenko
CAV Tutorial 4

Friday, July 16th

09:00‑10:00 Policy Monitoring in First-order Temporal Logic.
David Basin (ETH Zurich)
FLoc plenary talk

Saturday, July 17th

09:00‑10:00 The end of anonymity, the beginning of privacy
Vitaly Shamtikov
Hewlett-Packard Security Lecture, CSF
09:00‑10:00 Logic between Expressivity and Complexity
Johan van Benthem
IJCAR invited talk
09:00‑10:00 Quantitative Information Flow: from Theory to Practice?
Pasquale Malacaria
CAV invited talk
09:00‑10:00 A Logical Paradigm for Systems Biology
Francois Fages
ICLP invited talk

Sunday, July 18th

09:00‑10:00 Retrofitting Legacy Code for Security
Somesh Jha
CAV invited talk
14:00‑15:00 Induction, Invariants, and Abstraction.
Deepak Kapur (University of New Mexico)
FLoC keynote talk

Monday, July 19th

09:00‑10:00 Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
Leonardo de Moura
IJCAR invited talk
09:00‑10:00 TBA
Molham Aref
ICLP invited talk
09:00‑10:00 Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
Leonardo de Moura
IJCAR invited talk

Workshop invited talks

Jump to: Friday 9th · Saturday 10th · Wednesday 14th · Thursday 15th · Tuesday 20th · Wednesday 21st

Friday, July 9th

09:00 Hierarchical Petri Nets
Gordon Plotkin (with Nicolas Oury)
DCM
10 Years of Partiality and General Recursion
Ana Bove (Chalmers University)
DTP 2010
Church-style and Curry-style Subtyping
Adriana Compagnoni, Stevens Inst. of Technology, New-Jersey
ITRS 2010
Game Strategies and Rule-Based Systems
Dan Dougherty, Worcester Polytechnic Institute, MA, USA
IWS2010
What could be the right balance between abstract and fine-grain computational properties?
Gerard Berry (INRIA, College de France)
LOLA 2010
Reflexive domains and coherence numbers
Andrej Bauer, Ljubljana
PCARC
10:30 Geometry of Synthesis: Semantics-directed hardware compilation (tutorial)
Dan Ghica (University of Birmingham)
LOLA 2010
Some more on relative realizability
Jaap van Oosten, Utrecht
PCARC
11:30 Remarks on realizability
Pino Rosolini, Genova
PCARC
14:00 Rule-based Modeling: Theory and Practice
Russ Harmer
DCM
A Logic Foundation for Intersection and Union Types
Simona Ronchi Della Rocca, Univ. degli Studi di Torino
ITRS 2010
Organizing and using algebraic structures in large developments of formalized mathematics
Assia Mahboubi, INRIA Saclay -- Île-de-France
IWS2010
The Complexity of Proofs in Parameterized Resolution
Nicola Galesi
LCC/PPC
Linear types for continuations
Alex Simpson (LFCS, University of Edinburgh)
LOLA 2010
In what 2-category do PCAs most naturally live?
John Longley, Edinburgh
PCARC
15:30 A categorical account of Krivine's classical realizability
Thomas Streicher, Darmstadt
PCARC

Saturday, July 10th

09:00 Phase Estimation with Mixed States: Quantum Coherence versus Correlations
Vlatko Vedral
DCM
Elaborations in Type Theory
Matthieu Sozeau (Harvard University)
DTP 2010
Implicit Complexity in a Concurrency Scenario
Ugo Dal Lago
LCC/PPC
Software Configuration: What can we learn from Product Configuration?
Carsten Sinz (University of Karlsruhe)
LoCoCo 2010
Probabilistic Model Checking for Systems Biology
Marta Kwiatkowska, Oxford University
LSB 10
Recent developments in concurrent program logics
Viktor Vafeiadis
PSPL
10:30 Hybrid Logic: The Search for The Decidability Frontier
Moshe Vardi (Rice University, USA)
HyLo 2010
Modelling Yeast Osmoregulation at Different Levels of Resolution
Peter Gennemark, University of Gothenburg and Uppsala University
LSB 10
11:30 Understanding the Quantum Computational Speed-up via De-quantisation
Cristian Calude (with Alastair A. Abbott)
DCM
Molecular Self-Assembly Models of Variable Resolution
Ion Petre, Åbo Akademi University
LSB 10
14:00 Operational Computing with Quantum Stuff
Lucien Hardy
DCM
Tableau-Based Decision Procedures for Hybrid Logic
Gert Smolka (Saarland University, Germany)
HyLo 2010
TBA
Stephen Cook
LCC/PPC
Bio-Logic: The Challenges Facing Formal Modelling of Biology
Jasmin Fisher, Microsoft Research Cambridge
LSB 10
Proof Systems for Hybrid System Logics
André Platzer
PSPL
15:30 TBA
Albert Atserias
LCC/PPC
Protein Computing: a Phospho-Calculus?
John K Heath, University of Birmingham
LSB 10
16:30 Signalling Pathway Logic in the Immune Response. How Can We Make Complex Problems More Tractable?
Steven Watterson, The University of Edinburgh
LSB 10

Wednesday, July 14th

09:00 Closed nominal rewriting: properties and applications
Maribel Fernández, Kings College London
HOR 2010
The Practice and Promise of Substructural Frameworks
Frank Pfenning (Carnegie Mellon University)
LFMTP 2010
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
Lawrence C. Paulson (University of Cambridge)
PAAR-2010
Antipatterns: how to say what you don't want to match to
Claude Kirchner (INRIA Bordeaux-Sud-Ouest, France)
UNIF
TBA
Elvira Albert (Complutense University of Madrid)
WST
10:30 SMT-Solvers In (Tracing) Just-in-Time Compilers
Nikolai Tillman, Microsoft
SMT
14:00 Privacy and security issues in e-ticketing
Bart Jacobs, Technical University Eindhoven
FCS-PrivMod 2010
Computational interpretations of logic
Silvia Ghilezan, University of Novi Sad
HOR 2010
TBA
Andrei Voronkov (University of Manchester)
PAAR-2010
Nominal Unification - Hitting a Sweet Spot
Christian Urban (Technical University Munich, Germany)
UNIF
16:00 TBA
Chung-chieh Shan (Rutgers, The State University of New Jersey)
LFMTP 2010

Thursday, July 15th

08:30 Formal verification of numerical programs: from C annotated programs to Coq proofs
Sylvie Boldo
NSV 2010
09:00 Solving Constraint Satisfaction Problems by a SAT Solver
Naoyuki Tamura, Kobe University (Japan)
CICLOPS-WLPE-2010
Symbolic Techniques in Propositional Satisfiability Solving
Moshe Vardi, Rice University, TX, US:
CLoDeM2010
Symbolic and computational proofs of security
Hubert Comon-Lundh, CNRS & ENS de Cachan
FCS-PrivMod 2010
Managing State Explosion through Runtime Verification
Sharad Malik, Princeton University, USA
HWVW10
Possession as Linear Knowledge
Frank Pfenning (Carnegie Mellon University)
LAM10
Integrating Answer Set Programming and Satisfiability modulo Theories
Ilkka Niemela (Aalto University)
LaSh
The Quantitative Agenda in System Analysis
Thomas A. Henzinger (IST Austria)
LfSA 2010
Modules and records in Agda
Ulf Norell
MLPA-10
Recursive Definitions of Monadic Functions.
Alexander Krauss, Technische Universitat Muenchen.
PAR-10
SMT model checking for array-based systems
Silvio Ghilardi, U. Milano
SMT
10:30 Large-scale proof and libraries in Isabelle
Gerwin Klein
MLPA-10
11:30 Presburger Automata
Jerome Leroux, LaBRI, Bordeaux, FR
CLoDeM2010
Mizar Mathematical Library - a large repository of formalized mathematics
Andrzej Trybulec
MLPA-10
13:00 Applications of control to formal software semantics
Eric Feron
NSV 2010
14:00 Programming with Boolean Satisfaction
Michael Codish, Ben-Gurion University of the Negev
CICLOPS-WLPE-2010
Privacy in Electronic Voting
Michael Clarkson, Cornell University
FCS-PrivMod 2010
Why Work on Hardware Verification?
Cindy Eisner, IBM, Israel
HWVW10
(TBA)
David Pym (University of Bath)
LAM10
TBA
Don Sannella
MLPA-10
Djinn, monotonic.
Conor McBride, University of Strathclyde.
PAR-10
TBA
Sean McLaughlin, Carnegie Mellon University
PSTT
15:30 Kodkod: A Constraint Solver for Relational Logic
Emina Torlak.
LaSh
Towards a broad spectrum proof certificate
Dale Miller
MLPA-10
15:50 The Intelligent Grounder of DLV
Gelsomina Catalano, Nicola Leone, and Simona Perri
LaSh
16:00 Consequence-Based Reasoning for Description Logic Ontologies
Yevgeny Kazakov, Oxford, UK
CLoDeM2010
A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems
César A. Muñoz (NASA Langley)
LfSA 2010
16:10 The Life of Gringo
Martin Gebser, Roland Kaminski and Torsten Schaub.
LaSh
16:30 A Bottom-Up Approach to Safe Low-Level Programming
Adam Chlipala
MLPA-10

Tuesday, July 20th

09:00 ASP Solving and Other Computing Paradigms
Torsten Schaub, University of Potsdam, Germany:
ASPOCP10
Drools Business Logic integration Platform
Mark Proctor from JBoss
CHR 2010
Parallel Programming Needs New Foundations.
Keshav Pingali (UT Austin)
EC2-2010
Evaluation Opportunities in Mechanized Theories
Joe Hurd, Galois, Inc.
EMSQMS 2010
public key encryption schemes with special properties
Dennis Hofheinz
FCC 10
Abstractions Before Proofs
Cliff Jones (Newcastle University, UK)
VERIFY
09:05 A Probabilistic Abduction Engine for Media Interpretation based on Ontologies
Ralf Möller (University of Hamburg-Harburg)
UniDL
12:05 SWI Forms - Bringing logic to UI development
Matt Lilley from SecuritEase
CHR 2010
14:00 Programming models for the Barrelfish multi-kernel operating system.
Tim Harris (Microsoft Research, Cambridge)
EC2-2010
Inference Architectures for Satisfiability Modulo Theories
Natarajan Shankar
SVARM
Verification of Security Protocols
Véronique Cortier (LORIA INRIA-Lorraine, France)
VERIFY
Methods for Loop Invariant Generation
Sumit Gulwani
WING
15:30 EMS panel on solver competitions and community infrastructure
Joe Hurd, Galois, Inc.; Daniel Le Berre, Universite dArtois; Ian Horrocks, University of Oxford; Viktor Kuncak, EPFL; Leonardo de Moura, Microsoft Research
EMSQMS 2010 and SVRAM 2010

Wednesday, July 21st

09:00 Challenges in Using the Message Passing Interface in Multicore and Heterogeneous Systems.
Bill Gropp (UIUC)
EC2-2010
Formal Verification of System Software
Bernhard Beckert
SVARM
Real Analysis for Complex Systems
André Platzer (Carnegie Mellon University, USA)
VERIFY
Constraint-based modeling in systems biology
Alexander Bockmayr
WCB10
Abstract Interpretation Meets Mathematical Optimization
Helmut Seidl
WING
14:00 GPU programming: bugs, pitfalls and the importance of correctness in biomedical and scientific applications.
Miriam Leeser (Northeastern)
EC2-2010