Patrocínio



























Apoio








  • free counters


SBMF- Simpósio Brasileiro de Métodos Formais


Programação

Segunda, 24 de Setembro

SBMF Abertura (11:00 - 11:15)
Sessão Técnica 1 (SBMF: ST 1)
11h15 - 12h45 1 - CInvestigating Time Properties of Interrupt-Driven Programs
Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu e Shengchao Qin
2 - Specification Patterns for Properties over Reachable States of Graph Grammars
Simone Costa, Luciana Foss e Leila Ribeiro
3 - A Sound reduction of persistent sets for deadlock detection in MPI applications
Subodh Sharma, Ganesh Gopalakrishnan e Greg Bronevetsky
Sessão Técnica 2 (SBMF: ST 2)
14h30 - 16h00 1 - Model Checking Propositional Deontic Temporal Logic via a mu-calculus Characterization
Araceli Acosta, Cecilia Kilmurray, Pablo Castro e Nazareno Aguirre
2 - Alternating-time Temporal Logic in the Calculus of (Co)Inductive Constructions
Dante Zanarini, Carlos Luna e Luis Sierra
3 - Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflow
Germán Regis, Nicolás Ricci, Nazareno Aguirre e Tom Maibaum
Palestra Internacional (SBMF: Pal Int 1 - Wolfram Schulte)
16h30 - 18h00 1 - Thirteen Years of Automated Code Analysis at Microsoft
Wolfram Schulte (Microsoft Research)

Terça, 25 de setembro

Palestra Internacional (SBMF: Pal Int 2 - John Rushby)
09h00 - 10h30 1 - The Versatile Synchronous Observer
John Rushby (SRI International)
Sessão Técnica 3 (SBMF: ST 3)
11h00 - 12h30 1 - A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications
Gustavo Carvalho, Diogo Falcão, Alexandre Mota e Augusto Sampaio
2 - BETA: A B Based Testing Approach
Ernesto C. B. de Matos e Anamaria M. Moreira
3 - Verification Rules for Exception Handling in Eiffel
Emil Sekerinski e Tian Zhang
Sessão Técnica 4 (SBMF: ST 4)
14h30 - 16h00 1 - An approach using the B method to formal verification of PLC programs in an Industrial Setting
Haniel Barbosa e David Deharbe
2 - Palytoxin Inhibits the Sodium-Potassium Pump – An Investigation of an Electrophysiological Model Using Probabilistic Model Checking
Fernando Braz, Jader Cruz, Alessandra C. Faria-Campos e Sérgio Campos
3 - Identifying hardware failures systematically
Andre Didier e Alexandre Mota

Quarta, 26 de Setembro

Sessão Técnica 5 (SBMF: ST 5)
11h00 - 12h30 1 -Refinement, Compositionality, and Model-Driven Engineering
Jim Davies, Jeremy Gibbons, David Milward e James Welch
2 - Composition of Model Transformations: A Categorical Framework
Christoph Schulz, Michael Löwe e Harald König
3 - From SCR to SCADE (Artigo Curto)
Marcelo Andrade, Alexandre Mota e Márcio Cornélio
4 - Experience in Modeling a Microcontroller Instruction Set Using B (Artigo Curto)
Valério Gutemberg Medeiros Jr e David Déharbe
Sessão Técnica 6 (SBMF: ST 6) – Artigos Curtos
14h30 - 16h00 1 -Behavioral Transformation Contracts
Christiano Braga
2 - A Formal Analysis of Concurrent Assembly Code based on CSP
Gustavo Carvalho, Rafael Cabral e Alexandre Mota
3 - Hard-wiring CSP Parallelism: Implementing Multi-Synchronisation and Interleaving
Ivan Soares Medeiros Jr, Marcel V. M. Oliveira e Jim Woodcock
4 -A Probabilistic Model Checking Approach to Investigate Vehicular Networks
Bruno Ferreira, Fernando Braz e Sérgio Campos
5 - A Case Study on Model Checking and Deductive Verification Techniques of Safety-Critical Software
Rovedy Silva, José M Parente De Oliveira e Jorge Sousa Pinto
SBMF Encerramento (16:00 - 16:10)