Formal Methods: Foundations and Applications: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26–30, 2018, Proceedings

Description

This book constitutes the refereed proceedings of the 21st Brazilian Symposium on Formal Methods, SBMF 2018, which took place in Salvador, Brazil, in November 2018. The 16 regular papers presented in this book were carefully reviewed and selected from 30 submissions. The papers are organized in topical sections such as: techniques and methodologies; specification and modeling languages; theoretical foundations; verification and validation; experience reports regarding teaching formal methods; and applications.Chapter “TeSSLa: Temporal Stream-Based Specification Language” is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Front Matter ....Pages I-X The Pragmatic Dimension of Formal Methods: Towards Building a Sound Synthesiser (Alexandre Mota)....Pages 1-4 Formal Design of Cloud Computing Systems in Maude (José Meseguer)....Pages 5-19 Source Code Analysis with a Temporal Extension of First-Order Logic (David Come, Julien Brunel, David Doose)....Pages 20-38 A Type-Directed Algorithm to Generate Well-Typed Featherweight Java Programs (Samuel S. Feitosa, Rodrigo Geraldo Ribeiro, Andre Rauber Du Bois)....Pages 39-55 Programming Language Foundations in Agda (Philip Wadler)....Pages 56-73 Formal Verification of n-bit ALU Using Theorem Proving (Sumayya Shiraz, Osman Hasan)....Pages 74-89 The Scallina Grammar (Youssef El Bakouny, Dani Mezher)....Pages 90-108 VDM at Large: Modelling the EMV®\(2^{nd}\) Generation Kernel (Leo Freitas)....Pages 109-125 Constraint Reusing and k-Induction for Three-Valued Bounded Model Checking (Nils Timm, Stefan Gruner, Matthias Harvey)....Pages 126-143 TeSSLa: Temporal Stream-Based Specification Language (Lukas Convent, Sebastian Hungerecker, Martin Leucker, Torben Scheffel, Malte Schmitz, Daniel Thoma)....Pages 144-162 Automatic Test Case Generation for Concurrent Features from Natural Language Descriptions (Rafaela Almeida, Sidney Nogueira, Augusto Sampaio)....Pages 163-179 A Methodology for Protocol Verification Applied to EMV® 1 (Leo Freitas, Paolo Modesti, Martin Emms)....Pages 180-197 Analysing RoboChart with Probabilities (M. S. Conserva Filho, R. Marinho, A. Mota, J. Woodcock)....Pages 198-214 Timed Scenarios: Consistency, Equivalence and Optimization (Neda Saeedloei, Feliks Kluźniak)....Pages 215-233 Safe and Constructive Design with UML Components (Flávia Falcão, Lucas Lima, Augusto Sampaio)....Pages 234-251 Formal Modelling of Environment Restrictions from Natural-Language Requirements (Tainã Santos, Gustavo Carvalho, Augusto Sampaio)....Pages 252-270 Back Matter ....Pages 271-271