Go to the content

21 a 25/09/15BELO HORIZONTE - MG

Full screen

SBMF 2015


Online proceedings available

The proceedings of the SBMF 2015 were published by Springer as volume 9526 of the series Lecture Notes in Computer Science (LNCS).


The Brazilian Symposium on Formal Methods (SBMF) is a Brazilian symposium dedicated to the study and the application of Formal Methods in the development of software systems.

This symposium also has established itself in the national scientific calendar as an important scientific-technical event in the software area. Its first edition took place in 1998, going for its 18th edition in 2015.

The SBMF event is devoted to the dissemination of the development and use of formal methods for the construction and verification of computer systems, aiming to promote opportunities for researchers with interests in formal methods to discuss recent advances in the area.

SBMF 2015 will include the following specific activities, in addition to the general activities of CBSoft:

  • Lectures
  • Technical Sessions



Abstract Submission Deadline: July 6, 2015 (June 27, 2015)
Paper Submission Deadline: July 10, 2015 (July 3, 2015)
Authors notification: August 18, 2015
Camera-ready copy: September 2, 2015



Alvaro Miyazawa and Ana Cavalcanti
Refinement strategies for Safety-Critical Java

Bruno Cesar F. Silva, Augusto Sampaio and Gustavo Carvalho
Test Case Generation from Natural Language Requirements using CPN Simulation

Christiano Braga and Bruno Lopes
Towards Reasoning in Dynamic Logics with Rewriting Logic: the Petri-PDL Case

Christophe Chareton, Julien Brunel and David Chemouil
Evaluating the Assignment of Behavioral Goals to Coalitions of Agents

Francisco Macario and Marcel Vinicius Medeiros Oliveira
Hard-wiring CSP Hiding: Implementing Channel Abstraction to Generate Verified Concurrent Hardware

Jim Woodcock, Ana Cavalcanti and Andy Wellings
Mobile CSP

Luis Gustavo Perpetuo Costa Marques, Max Hering de Queiroz and Jean-Marie Farines
Improving a Design Methodology of Synthesizable VHDL by Using Model Checking

Nils Timm and Stefan Gruner
Instantiation Reduction in Iterative Parameterised Three-Valued Model Checking

Rodrigo Ribeiro and Carlos Camarão
A Mechanized Textbook Proof of a Type Unification Algorithm

Sidney C. Nogueira, Hugo L. S. Araujo, Renata B. S. Araujo, Juliano Iyoda and Augusto Sampaio
Automatic generation of test cases and test purposes from natural language

Tarciana Silva, Alexandre Mota and Augusto Sampaio
Sound Transformations of Java programs using Alloy

Valdivino Alexandre de Santiago Júnior and Sofiene Tahar
Time Performance Formal Evaluation of Complex Systems