Wednesday the 10th of November
| 08:00-08:30 | Registration |
| 08:30-09:00 | Opening of the Conference |
|
9:00-10:00
|
Keynote by Constance Heitmeyer
A Model-Based Approach to Testing Software for Critical Behavior and Properties
|
|
10:00-10:30
|
Coffee Break
|
|
10:30-12:00
|
Full Papers Session 1
|
Michael Leuschel and Jens Bendisposto
Directed Model Checking for B: An Evaluation and New Techniques
|
Wojciech Mostowski and Erik Poll.
Midlet Navigation Graphs in JML
|
Pedro Crispim, Antónia Lopes and Vasco T. Vasconcelos
Runtime Verification for Generic Classes with CONGU2
|
|
12:00-14:00
|
Lunch
|
|
14:00-15:30
|
Full Papers Session 2
|
Sabina Akhtar, Stephan Merz and Martin Quinson
A High-Level Language for Modeling Algorithms and Their Properties
|
Paulo Salem da Silva and Ana Cristina Vieira de Melo
A Formal Environment Model for Multi-Agent Systems
|
Sebastian Bauer, Rolf Hennicker and Michel Bidoit
A Modal Interface Theory with Data Constraints
|
|
15:30-16:00
|
Coffee Break
|
|
16:00-17:00
|
Full Papers Session 3
|
Tiago Massoni, Rohit Gheyi and Paulo Borba
Synchronizing Model and Program Refactoring
|
Daniel Calegari, Carlos Luna, Nora Szasz and Alvaro Tasistro
A Type-Theoretic Framework for Certified Model Transformations
|
|
17:30-19:30
|
SBMF Panel I - Integration Industry-Academia
|
|
20:00-23:00
|
Conference Dinner
|
Thursday the 11th of November
|
9:00-10:00
|
Keynote by Bill Roscoe
SVA: Using CSP to Analyse Shared Variable Programs
|
|
10:00-10:30 |
Coffee Break
|
|
10:30-12:00
|
Full Papers Session 4
|
Moritz Kleine and J. W. Sanders
Simulating Truly Concurrent CSP
|
Håkan L. S. Younes, Edmund Clarke and Paolo Zuliani
Statistical Verification of Probabilistic Properties with Unbounded Until
|
Alejandro Tamalet and Ken Madlener
Reasoning about Assignments in Recursive Data Structures
|
|
12:00-14:00
|
Lunch
|
|
14:00-15:30
|
Full Papers Session 5
|
Abderrahman matoussi, Frédéric Gervais and Régine Laleau
Specification of a Localization Component
|
Eduardo Mazza, Marie-Laure Potet and Daniel Le Métayer
A Formal Framework for Specifying and Analyzing Logs
|
Artur Gomes and Marcel Vinicius Medeiros Oliveira
Formal Development of a Cardiac Pacemaker
|
|
15:30-16:00
|
Coffee Break
|
|
16:00-17:00
|
Full Papers Session 6
|
Marcello Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, Jan Rutten and Alexandra Silva
A decision procedure for bisimilarity of generalized regular expressions
|
Thomas Martin Gawlitza, Helmut Seidl and Kumar Neeraj Verma
Normalization of Linear Horn-Clauses
|
|
17:30-19:00
|
PC Meeting
|
Friday the 12th of November
|
9:00-10:00
|
Keynote by David Naumann
Dynamic Boundaries: Global Invariants for Local Reasoning
|
|
10:00-10:30
|
Coffee Break
|
|
10:30-12:00
|
Discussion About Formal Method Curriculum
|
|
12:00-14:00
|
Lunch
|
|
14:00-15:30
|
WTD
|
Thiago C. de Sousa and Paulo Sérgio Muniz Silva
A UML-based Method for Event-B Refinement
|
Saeed Khalafinejad and Seyed-Hassan Mirian-Hosseinabadi
Generation of Database Schemas from Z Specifications
|
Giselle Reis and Elaine Pimentel
Using Linear Logic with Subexponentials to Implement Logic Interpreters
|
|
15:30-16:00
|
Coffee Break
|
|
16:00-17:00
|
Full Papers Session 7
|
Zhiming Liu, Charles Morisset and Shuling Wang
A Graph-based Implementation for Mechanized Refinement Calculus of OO Programs
|
Frank Zeyda and Ana Cavalcanti
Automatic Refinement of Circus Programs
|
|
17:00 -17:30
|
Closing SBMF
|
|
18:30 - 20:30
|
SBMF Happy Hour
(associated with DIMAP's 25 Years Celebration)
|
|