Monday (September 21, 2015)
Keynote (09:00 - 10:30)
Applications of Formal Methods to Data Wrangling and Education
Sumit Gulwani, Microsoft Research, Redmond, WA, USA
11:00 - 12:30
Technical Session 1: Model Checking
Chair: Christiano Braga
Improving a Design Methodology of Synthesizable VHDL by Using Model Checking
Luis Gustavo Perpetuo Costa Marques, Max Hering de Queiroz and Jean-Marie Farines
Hard-wiring CSP Hiding: Implementing Channel Abstraction to Generate Verified Concurrent Hardware
Francisco Macario and Marcel Vinicius Medeiros Oliveira
Instantiation Reduction in Iterative Parameterised Three-Valued Model Checking
Nils Timm and Stefan Gruner
15:00 - 16:30
Technical Session 2: Languages and Semantics
Chair: Augusto Sampaio
Mobile CSP
Jim Woodcock, Andy Wellings and Ana Cavalcanti
Evaluating the Assignment of Behavioral Goals to Coalitions of Agents
Christophe Chareton, Julien Brunel and David Chemouil.
Towards Reasoning in Dynamic Logics with Rewriting Logic: the Petri-PDL Case
Christiano Braga and Bruno Lopes
Tuesday (September 22, 2015)
11:00 - 12:30
Technical Session 3: Refinement and Verification
Chair: Jim Woodcock
Refinement strategies for Safety-Critical Java
Alvaro Miyazawa and Ana Cavalcanti
Verifying Transformations of Java programs using Alloy
Tarciana Silva, Alexandre Mota and Augusto Sampaio
A Mechanized Textbook Proof of a Type Unification Algorithm
Rodrigo Ribeiro and Carlos Camarão
15:00 - 16:30
Technical Session 4: Testing and Evaluation
Chair: Ana Cavalcanti
Automatic generation of test cases and test purposes from natural language
Sidney C. Nogueira, Hugo L. S. Araujo, Renata B. S. Araujo, Juliano Iyoda and Augusto Sampaio
Time Performance Formal Evaluation of Complex Systems
Valdivino Alexandre de Santiago Júnior and Sofiene Tahar
Test Case Generation from Natural Language Requirements using CPN Simulation
Bruno Cesar F. Silva, Augusto Sampaio and Gustavo Carvalho
Keynote (17:00 - 18:30)
To test or not to test, that is formal question
Adenilso Simão, ICMC/USP, São Carlos, SP, Brazil
