Brazilian Symposium on Formal Methods (SBMF)

Keynotes and Tutorials

Technical Session 1:

• Neda Saeedloei and Feliks Kluzniak. An Efficient Customized Clock Allocation Algorithm for a Class of Timed Automata

• Mohamed Abdelghany and Sofiene Tahar. Formalization of Functional Block Diagrams using HOL Theorem Proving

Technical Session 2:

• Maycon Amaro, Samuel Feitosa and Rodrigo Ribeiro. A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching

• Luciano Silva and Marcel Oliveira. Automatic Generation of Verified Concurrent Hardware using VHDL

• Maksym Bortin. Synthesis of Implementations for Divide-and-conquer Specifications

Technical Session 3:

• Joabe Jesus and Augusto Cesar Sampaio. Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover

• Geoff Hamilton and Benjamin Aziz. Excommunication: Transforming Pi-Calculus Specifications to Remove Internal Communication

• Matthias Güdemann and Klaus Riedl. Level-Up - From Bits to Words