Program

Monday, 28 July

12:00 - 13:00Registration
13:00 - 14:00Session Chair: Jose Meseguer and Grigore Rosu
  • Invited Talk: Marrying Words and Trees, Rajeev Alur
14:00 - 14:30Break
14:30 - 16:00Session Chair: Grigore Rosu
  • Verification of Java Programs with Generics,Kurt Stenzel, Holger Grandy, Wolfgang Reif
  • Separation Logic Contracts for a Java-like Language with Fork/Join,Christian Haack, Clement Hurlin
  • Evolving Specification Engineering, Dusko Pavlovic, Peter Pepper, Douglas Smith
16:30First bus leaves for Allerton
16:40Final bus leaves for Allerton
18:30 - 20:30Banquet at Allerton

Tuesday, 29 July

08:00 - 09:00Breakfast
09:00 - 10:00Session Chair: Martin Wirsing
  • Invited Talk: Simulation Using Orchestration, Jayadev Misra
10:00 - 10:30Break
10:30 - 12:00Session Chair: Rolf Hennicker
  • Explaining Verification Conditions,Ewen Denney, Bernd Fischer
  • Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving,Stefan Maus, Michal Moskal, Wolfram Schulte
  • A Hybrid Approach for Safe Memory Management in C, Syrine Tlili, Zhenrong Yang, Hai Zhou Ling, Mourad Debbabi
12:00 - 13:30Lunch
13:30 - 15:00Session Chair: Doug Smith
  • An Algebra for Features and Feature Composition,Sven Apel, Christian Lengauer, Bernhard Moeller, Christian Kaestner
  • Extending Timed Process Algebra with Discrete Stochastic Time,Jasen Markovski, Erik de Vink
  • Domain Axioms for a Family of Near-Semirings, Georg Struth, Jules Desharnais
15:00 - 15:30Break
15:30 - 17:00Session Chair: Narciso Marti-Oliet
  • Abstract Interpretation Plugins for Type Systems,Tobias Gedell, Daniel Hedin
  • Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines,Roberto Bruni, Leonardo Gaetano Mezzina
  • A Formal Analysis of Complex Type Flaw Attacks on Security Protocols, Han Gao, Chiara Bodei, Pierpaolo Degano
17:00 - AMAST Business Meeting

Wednesday, 30 July

08:00 - 09:00Breakfast
09:00 - 10:00Session Chair: Mike Johnson
  • Invited Talk: Liberate Computer User from Programming, Teodor Rus
10:00 - 10:30Break
10:30 - 12:00Session Chair: Roberto Bruni
  • Constant complements, reversibility and universal view updates,Michael Johnson, Robert Rosebrugh
  • Generating specialized rules and programs for demand-driven analysis,K. Tuncay Tekle, Katia Hristova, Yanhong A. Liu
  • The verification of the on-chip COMA cache coherence protocol, Duong Vu, Li Zhang, Chris Jesshope
12:00 - 13:30Lunch
13:30 - 15:00Session Chair: Andrzej Tarlecki
  • Coinductive Properties of Causal Maps,Jiho Kimr
  • Service Specification and Matchmaking using Description Logic: An Approach Based on Institutions,M. Birna van Riemsdijk, Rolf Hennicker, Martin Wirsing, Andreas Schroeder
  • Towards a Model-theoretic Semantics for Contract-based Software Components, Rolf Hennicker, Michel Bidoit
15:00 - 15:30Break
15:30 - 17:10Session Chair: Jose Fiadeiro
  • A declarative debugger for Maude,Rafael Caballero, Narciso Marti-Oliet, Adrian Riesco, Alberto Verdejo
  • Towards Validating a Platoon of Cristal Vehicles using CSP||B,Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, Jeanine Souquieres
  • Towards Formal Verification of ToolBus Scripts, Wan Fokkink, Paul Klint, Bert Lisser, Yaroslav S. Usenko
  • Implementing a categorical information system, Michael Johnson, Robert Rosebrugh
  • System Demonstration of Spiral, Program Generator for High-Performance Libraries for Linear Transforms, Yevgen Voronenko, Franz Franchetti, Frederic de Mesmay, Markus Pueschel

Thursday, 31 July

08:00 - 09:00Breakfast
09:00 - 10:30Session Chair: Jan Rutten
  • Non expansive Epsilon-Bisimulations,Simone Tini
  • Calculating Invariants as Coreflexive Bisimulation,Luis Barbosa, Jose Oliveira, Alexandra Silva
  • Towards an Efficient Implementation of Tree Automata Completion, Emilie Balland, Yohan Boichut, Pierre-Etienne Moreau, Thomas Genet
10:30 - 11:00Break
11:00 - 12:00Session Chair: Jose Meseguer
  • Petri nets are dioids,Paolo Baldan, Fabio Gadducci
  • Long-Run Cost Analysis by Approximation of Linear Operators over Dioids,David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin
12:00 - 13:30Lunch