9.00 9.30 |
Welcome | |||
9.30 10.30 |
Session chair: Furio Honsell Gordon Plotkin (Invited Lecture) |
|||
10.30 11.00 |
Coffee | |||
11.00 12.30 |
CC
Program Analysis 1 Session chair: Tom Reps
Alias Analysis by means of a Model Checker
Points-to and Side-effect Analyses for Programs Built with Precompiled
Libraries
A Novel Probabilistic Data-Flow Framework
|
FOSSACS
Concurrency and Mobility Session chair: Luca Cardelli
Secrecy Types for Asymmetric Communication
High-Level Petri Nets as Type Theories in the Join Calculus
The Complexity of Model Checking Mobile Ambients
|
TACAS
Opening: Tiziana Margaria and Wang Yi
Symbolic Verification
Language Containment Checking with Nondeterministic BDDs
Satisfiability Checking Using Boolean Expression Diagrams
A Library for Composite Symbolic Representations
|
WADT |
12.30 15.00 |
Lunch | |||
15.00 17.00 |
CC
Program Transformation Session chair: Uwe Assmann
Imperative Program Transformation by Rewriting
Compiler Transformation of Pointers to Explicit Array
Accesses in DSP Applications
User-extensible Simplification — Type-based Optimizer Generators
A Practical, Robust Method for Generating Variable Range Tables
|
FOSSACS
Type Theory Session chair: Pawel Urzyczy
Type inference with recursive type equations
Axioms for Recursion in Call-by-Value
Type Isomorphisms and Proof Reuse in Dependent Type Theory
The Rho Cube
|
TACAS
Infinite State Systems: Deduction and Abstraction Session chair: Rance Cleaveland
Synthesis of Linear Ranking Functions
Automatic Deductive Verification with Invisible Invariants
Incremental Verification by Abstraction
A Technique for Invariant Generation
|
WADT |
17.00 17.30 |
Coffee | |||
17.30 19.00 |
CC
Program Analysis 2 Session chair: Reinhard Wilhelm
Efficient Symbolic Analysis for Optimizing Compilers
Interprocedural Shape Analysis for Recursive Programs
Design-Driven Compilation
|
FOSSACS
Formal Verification Session chair: Carolyn Talcott
Verified Bytecode Verifiers
Higher-Order Abstract Syntax with Induction in Isabelle/HOL:
Marrella and the Verification of an Embedded System (DEMO)
|
TACAS
Applications of Model Checking Techniques Session chair: John Hatcliff
Model Checking Syllabi and Student Careers
Verification of Vortex Workflows
Parameterized Verification of Multithreaded Software Libraries
|
WADT |
20.00 | Reception |