*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 |