Program
| Tuesday, 26th August | |
| 8:00 - 8:30 | Registration / M1 |
| 8:30 - 9:00 | LSFA / BDD / M1 |
| 9:00 - 9:30 | LSFA / BDD / M1 |
| 9:30 - 10:00 | LSFA / BDD / M1 |
| 10:00 - 10:30 | Coffee Break |
| 10:30 - 11:00 | LSFA / BDD / M2 |
| 11:00 - 11:30 | LSFA / BDD / M2 |
| 11:30 - 12:00 | LSFA / BDD / M2 |
| 12:00 - 12:30 | LSFA / BDD / M2 |
| 14:00 - 14:30 | LSFA / BDD / M1 |
| 14:30 - 15:00 | LSFA / BDD / M1 |
| 15:00 - 15:30 | LSFA / BDD / M1 |
| 15:30 - 16:00 | LSFA / BDD / M1 |
| 16:00 - 16:30 | Coffee Break |
| 16:30 - 17:00 | LSFA / BDD / M2 |
| 17:00 - 17:30 | LSFA / BDD / M2 |
| 17:30 - 18:00 | LSFA / BDD / M2 |
| 18:00 - 18:30 | LSFA / BDD / M2 |
Wednesday, 27th August |
|
| 8:00 - 8:30 | Registration |
| Invited Talk Chair: Ana Melo |
|
| 8:30 - 10:00 | Stateflow diagrams in Circus. Ana Cavalcanti (University of York, UK). |
| 10:00 - 10:30 | Coffee Break |
| Technical Papers Track (Refinement, Verification and Code Generation) Chair: Jim Woodcock |
|
| 10:30 - 11:00 | Combining decision procedures by (model-)equality
propagation. David Deharbe (UFRN, BR), Diego Caminha B. de Oliveira (Universiti de Nancy-INRIA-LORIA, Nancy-France), Pascal Fontaine (Universiti de Nancy - INRIA - LORIA Nancy - France) M3 |
| 11:00 - 11:30 | Checking Z Data Refinements Using Traces Refinement A. Didier, A. Farias, A. Mota (Cin - UFPE - PE - BR) M3 |
| 11:30 - 12:00 | Specification and Runtime Verification of Java Card Programs. Umberto Souza da Costa, Anamaria Martins Moreira, Martin A. Musicante (UFRN-BR), Placido A. Souza Neto (CEFET/RN-BR) M3 |
| 12:00 - 12:30 | M3 |
| Invited Talk Chair: Ana Cavalcanti |
|
| 14:00 - 15:00 | Talk: Research in Formal Methods Ana Cristina Vieira de Melo (USP, SP-BR) M3 |
| Student Papers Track Chair: Juliano Iyoda / Invited Debaters: Alexandre Mota, Ana Cavalcanti, Anamaria Martins Moreira |
|
| 15:00 - 15:30 | An Automatic Translation Approach for Component, Based Real-Time Systems Verification. André L. N. Muniz, Aline M. S. Andrade, George Lima (LaSiD-UFBA-BR) On the Development of Integrated Modular Avionics Systems Assisted by Model Checking. Fabiano C. Carvalho(Mectron-SP-BR), Josi M. Parente de Oliveira, Gustavo T. Zaniboni (ITA-SP-BR) |
| 15:30 - 16:00 | Student Papers Discussion |
| 16:00 - 16:30 | Coffee Break |
| Student Papers Track | |
| 16:30 - 17:00 | Towards a Formal Development of an Artificial
Pacemaker. A. O. Gomes, M. V. M. Oliveira (UFRN-Natal-RN-Brazil) |
| Demonstration and Poster Track Chair: Adolfo Duran |
|
| 17:00 - 17:30 | Specification and Runtime Verification of Java Card Programs. Umberto Souza da Costa, Anamaria Martins Moreira, Martin A. Musicante (UFRN - BR), Placido A. Souza Neto (CEFET/RN - BR) JZed-Gen: Towards Pragmatical Generation of Software from Z Specifications Alvaro Miyazawa, Paulo Salem da Silva, Ana C. V. de Melo (USP - SP - BR) |
| 17:30 - 18:00 | Poster call: The Correctness of the AKS Primality Test in
Coq. Flavio L. C. de Moura, Ricardo Tadeu (UnB - DF - BR) |
| 18:00 - 18:30 | Openning |
Thursday, 28th August |
|
| 8:00 - 8:30 | Registration |
| Invited Talk - Chair: Patrícia Machado | |
| 8:30 - 10:00 | Symbolic model-based test selection. Thierry Jeron (IRISA / INRIA, FR). |
| 10:00 - 10:30 | Coffee Break |
| Technical Papers Track (Verification and Validation) Chair: David Deharbe |
|
| 10:30 - 11:00 | Mechanized wire-wire verification of Handel-C synthesis. Juan Ignacio Perna, JimWoodcock (University of York, York-U.K.) |
| 11:00 - 11:30 | Transforming Programs into Recursive Functions. Magnus O. Myreen, Michael J. C. Gordon (University of Cambridge - U.K.) |
| 11:30 - 12:00 | Model Checking Merged Program Traces. Paulo Salem da Silva and Ana C. V. de Melo (USP - Sao Paulo - Brasil) |
| Invited Tutorial Chair: Marcelo D'Amorin |
|
| 14:00 - 16:00 | Patrice Godefroid (Microsoft Research, Redmond, US) Invited Tutorial |
| 16:00 - 16:30 | Coffee Break |
| Invited Talks - Chair: Patrícia Machado | |
| 16:30 - 18:00 | Formal Methods in Industry |
| 18:00 - 18:30 | Meeting CEMF |
Friday, 29th August |
|
| 8:00 - 8:30 | Registration |
| Invited Talk Chair: Augusto Sampaio |
|
| 8:30 - 9:30 | Applying the B Method to Take on the Grand Challenge of
Verified Compilation. David Deharbe (UFRN, BR) |
| 9:30 - 10:00 | Grand Challenge in Software Verification Jim Woodcock (University of York, UK) |
| 10:00 - 10:30 | Coffee Break |
| Technical Papers Track (Formal Methods Integration and Reasoning) Chair: Álvaro Moreira |
|
| 10:30 - 11:00 | Mechanical Reasoning about Families of UTP Theories. Frank Zeyda and Ana Cavalcanti (University of York, York-U.K.) M4 |
| 11:00 - 11:30 | Formal Verification of Graph Grammar using Mathematical Induction. Simone Andri da Costa (UFRGS, UFPel-RS-BR), Leila Ribeiro (UFPel - RS - BR) M4 |
| 11:30 - 12:00 | A Case Study in JML-Assisted Software Development. Fernando Barraza (ParqueSoft, Cali, Colombia), Nestor Catano, Daniel Garcia, Pablo Ortega, Camilo Rueda (Pontificia Universidad Javeriana-Cali-Colombia) M4 |
| 12:00 - 12:30 | M4 |
| Technical Papers Track (Specification and Modelling) Chair: Leonardo Freitas |
|
| 14:00 - 14:30 | Multiple Synchrony in MSC. Flavia Falcco, Juliano Iyoda and Augusto Sampaio (Cin-UFPE-PE-BR) M4 |
| 14:30 - 15:00 | A TLA+ Formal Specification and Verification
of a New Real-Time Communication Protocol. Paul Regnier, George Lima, Aline Andrade (LaSiD - UFBA - Brasil) M4 |
| Demonstration and Poster Track Chair: Adolfo Duran |
|
| 15:00 - 15:30 | Transforming Programs into Recursive Functions. Magnus O. Myreen, Michael J. C. Gordon (University of Cambridge-U.K.) Model Checking Merged Program Traces. Paulo Salem da Silva and Ana C. V. de Melo (USP-Sao Paulo-Brasil) M4 |
| 15:30 - 16:00 | A Case Study in JML-Assisted Software Development. Fernando Barraza (ParqueSoft, Cali, Colombia), Nestor Catano, Daniel Garcia, Pablo Ortega, Camilo Rueda (Pontificia Universidad Javeriana-Cali-Colombia) M4 |
| 16:00 - 16:30 | Coffee Break |
| 16:30 - 17:00 | Closing |
| Minicursos | |
| Terça-feira (26/08): 8:00-10:00 14:00-16:00 |
M1 Abordagens Baseadas em Modelos para o Projeto de Sistemas Interativos Dr. Marco Winckler (IRIT/FR) |
| Terça-feira (26/08): 10:30-12:30 16:30-18:30 |
M2 Model-Driven Architecture (MDA) e Geração de Código Dr. Franklin Ramalho (UFCG) |
| Quarta-feira (27/08): 10:30-12:30 14:00-15:00 |
M3 Teoria da Computação, o Barbeiro e o Mentiroso Dr. Edward Hermann Haeusler (PUC-Rio) |
| Sexta-feira (29/08): 10:30-12:30 14:00-16:00 |
M4 Fundamentos do Teste de Software Dr. Marcelo D′Amorim (UFPE) |
Tutorials (minicursos)
