• free counters

SBMF - Brazilian Symposium on Formal Methods


Monday, September - 24

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

Tuesday, September - 25

Invited Talk (SBMF: Int Keynote 2 - John Rushby)
09h00 - 10h30 1 - The Versatile Synchronous Observer
John Rushby (SRI International)
Technical Session 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 and Augusto Sampaio
2 - BETA: A B Based Testing Approach
Ernesto C. B. de Matos and Anamaria M. Moreira
3 - Verification Rules for Exception Handling in Eiffel
Emil Sekerinski and Tian Zhang
Technical Session 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 and 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 and Sérgio Campos
3 - Identifying hardware failures systematically
Andre Didier and Alexandre Mota

Wednesday, September - 26

Technical Session 5 (SBMF: ST 5)
11h00 - 12h30 1 -Refinement, Compositionality, and Model-Driven Engineering
Jim Davies, Jeremy Gibbons, David Milward and James Welch
2 - Composition of Model Transformations: A Categorical Framework
Christoph Schulz, Michael Löwe and Harald König
3 - From SCR to SCADE (short paper)
Marcelo Andrade, Alexandre Mota and Márcio Cornélio
4 - Experience in Modeling a Microcontroller Instruction Set Using B (short paper)
Valério Gutemberg Medeiros Jr and David Déharbe
Technical Session 6 (SBMF: ST 6) – Short Papers
14h30 - 16h00 1 -Behavioral Transformation Contracts
Christiano Braga
2 - A Formal Analysis of Concurrent Assembly Code based on CSP
Gustavo Carvalho, Rafael Cabral and Alexandre Mota
3 - Hard-wiring CSP Parallelism: Implementing Multi-Synchronisation and Interleaving
Ivan Soares Medeiros Jr, Marcel V. M. Oliveira and Jim Woodcock
4 -A Probabilistic Model Checking Approach to Investigate Vehicular Networks
Bruno Ferreira, Fernando Braz and 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 and Jorge Sousa Pinto
SBMF Closing Session (16:00 - 16:10)