Conference Program

WEDNESDAY, August 29th

08:45: Opening session

9:00-10:00: Invited talk by Martin Abadi

Software Security: A Formal Perspective

10:00: Coffee break

10:30-12:30: Verification   

Matthieu Carlier, Catherine Dubois and Arnaud Gotlieb
A certified constraint solver over finite domains

Hossein Hojjat, Filip Konecny, Florent Garnier, Radu Iosif, Viktor Kuncak

and Philipp Ruemmer

A Verification Toolkit for Numerical Transition Systems (tool paper)

 

Sam Owre, Indranil Saha and Natarajan Shankar
Automatic Dimensional Analysis of Cyber-Physical Systems

 

Mathieu Giorgino and Martin Strecker
Correctness of pointer manipulating algorithms illustrated by a verified BDD construction

 

Maurice H. Ter Beek, Franco Mazzanti and Aldi Sulova

VMC: A Tool for Product Variability Analysis (tool paper)

 

12:30: Lunch

 

14:00-16:00: Learning and control

Fides Aarts, Faranak Heidarian, Harco Kuppens, Petur Olsen
Automata Learning Through Counterexample-Guided Abstraction Refinement

Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong and Étienne André

Automatic Compositional Verification of Timed Systems (tool paper)

 

Ammar Osaiweran, Tom Fransen, Jan Friso Groote and Bart van Rijnsoever
Experience Report on Designing and Developing Control Components using Formal Methods

 

Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat
IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems (tool paper)

 

Nicolas D'Ippolito, Victor Braberman, Nir Piterman and Sebastian Uchitel

The Modal Transition System Control Problem

16:00: Coffee break

 

16:30-18:30: Analysis and Debugging

Andreas Bauer and Ylies Falcone

Decentralised LTL monitoring without central observer

 

Evren Ermis, Martin Schäf and Thomas Wies

Error Invariants

Virginia Aponte, Pierre Courtieu, Yannick Moy and Marc Sango
Maximal and Compositional Pattern-Based Loop Invariants

Howard Barringer, Yliès Falcone, Klaus Havelund, Giles Reger and David Rydeheard

Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors

19:00-21:00 Welcome Reception

 

THURSDAY, August 30th

09:00-10:00: Invited talk by Asaf Degani

Formal Methods in the Wild: Trains, Planes, & Automobiles

10:00: Coffee break

10:30-12:30: Modeling and Model Checking  

James Heather and Steve Schneider
A Formal Framework for Modelling Coercion Resistance and Receipt Freeness

Yael Meller, Orna Grumberg and Karen Yorav

Applying Software Model Checking Techniques For Behavioral UML Models

 

Fu Song and Tayssir Touili

Efficient Malware Detection Using Model-Checking

 

Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong and Yan Liu

Improved BDD-based Discrete Analysis of Timed Systems

12:30-12:40: Verification Competition Presentation,  

Marieke Huisman, U Twente, Vladimir Klebanov, Karlsruhe Institute of Technology, Rosemary Monahan , NUI Maynooth

12:40 Lunch

14:00-16:00: Proofs and Synthesis   

Grigore Rosu and Andrei Stefanescu
From Hoare Logic to Matching Logic

María Alpuente, Demis Ballis, Francisco Frechina and Daniel Romero

Julienne: a Trace Slicer for Conditional Rewrite Theories

 

Srinivas Nedunuri, William R Cook and Douglas Smith

Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms

 

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts and Hernán Vanzetto

TLA+ Proofs (tool paper)

 

Daniel Plagge and Michael Leuschel

Validating B, Z and TLA+ using ProB and Kodkod

16:00: Coffee break

16:30-18:30: Distribution and Refinement

Mikael Asplund, Atif Manzoor, Melanie Bouroche, Siobhan Clarke and Vinny Cahill

A Formal Approach to Autonomous Vehicle Coordination

 

German Sibay, Sebastian Uchitel, Victor Braberman and Jeff Kramer

Distribution of Modal Transition Systems

 

Mirko Spasic and Filip Maric

Formalization of Incremental Simplex Algorithm by Stepwise Refinement

 

Julien Dormoy, Olga Kouchnarenko and Arnaud Lanoix

When Structural Refinement of Components Keeps Temporal Properties over Reconfigurations

21:00-23:15: Conference Dinner

 

FRIDAY, August 31st

09:00-10:00: Invited talk by Alan Wassyng

Who Are We, and What Are We Doing Here?

 

10:00: Coffee break

10:30-12:30: Testing  

Maria Christakis, Peter Müller and Valentin Wüstholz
Collaborative Verification and Testing with Explicit Assumptions

 

Yasuhiko Minamide and Shunsuke Mori

Reachability Analysis of the HTML5 Parser Specification and its Application to Compatibility Testing

 

Guowei Yang, Sarfraz Khurshid and Miryung Kim

Specification-based Test Repair Using a Lightweight Formal Method

 

Rob Hierons, Mercedes Merayo and Manuel Nuñez

Using Time to Add Order to Distributed Testing

12:30-12:40: FM 2013 Preparation, Cliff Jones  

12:40 Lunch

14:00-16:00: Applications   

Hengjun Zhao, Naijun Zhan, Deepak Kapur and Kim G. Larsen

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example

 

David Lazar, Andrei Arusoaie, Traian Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu and Grigore Rosu

Executing Formal Semantics with the K Tool (tool paper)

 

Soufiene Benkirane, Rachel Norman, Erin Scott and Carron Shankland

Measles Epidemics and PEPA: an exploration of historic disease dynamics using process algebra

 

Taylor T Johnson, Jeremy Green, Sayan Mitra, Rachel Dudley and Richard Scott Erwin

Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems

16:00: Coffee break

16:30: Closing session