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