Technical Program

Invited Talks

Accepted Papers

  • Wojciech Mostowski and Erik Poll.
    Midlet Navigation Graphs in JML

  • Giselle Reis and Elaine Pimentel.
    [WTD] Using Linear Logic with Subexponentials to Implement Logic Interpreters

  • Alejandro Tamalet and Ken Madlener.
    Reasoning about Assignments in Recursive Data Structures

  • Paulo Salem da Silva and Ana Cristina Vieira de Melo.
    A Formal Environment Model for Multi-Agent Systems

  • Moritz Kleine and J. W. Sanders.
    Simulating Truly Concurrent CSP

  • Sebastian Bauer, Rolf Hennicker and Michel Bidoit.
    A Modal Interface Theory with Data Constraints

  • Eduardo Mazza, Marie-Laure Potet and Daniel Le Mvİtayer.
    A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence

  • Frank Zeyda and Ana Cavalcanti.
    Automatic Refinement of Circus Programs

  • Thomas Martin Gawlitza, Helmut Seidl and Kumar Neeraj Verma.
    Normalization of Linear Horn-Clauses

  • Michael Leuschel and Jens Bendisposto.
    Directed Model Checking for B: An Evaluation and New Techniques

  • Sabina Akhtar, Stephan Merz and Martin Quinson.
    A High-Level Language for Modeling Algorithms and Their Properties

  • Zhiming Liu, Charles Morisset and Shuling Wang.
    A Graph-based Implementation for Mechanized Refinement Calculus of OO Programs

  • Abderrahman matoussi, Frvİdvİric Gervais and Rvİgine Laleau.
    Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned

  • Tiago Massoni, Rohit Gheyi and Paulo Borba.
    Synchronizing Model and Program Refactoring

  • Marcello Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, Jan Rutten and Alexandra Silva.
    Algebra meets coalgebra \\ A decision procedure for bisimilarity of generalized regular expressions

  • Pedro Crispim, Antv=nia Lopes and Vasco T. Vasconcelos.
    Runtime Verification for Generic Classes with CONGU2

  • Artur Gomes and Marcel Vinicius Medeiros Oliveira.
    Formal Development of a Cardiac Pacemaker: from Specification to Code

  • Daniel Calegari, Carlos Luna, Nora Szasz and Alvaro Tasistro.
    A Type-Theoretic Framework for Certified Model Transformations

  • Thiago C. de Sousa and Paulo Svİrgio Muniz Silva.
    [WTD] A UML-based Method for Event-B Refinement

  • Saeed Khalafinejad.
    [WTD] Generation of Database Schemas from Z Specifications