Formal Methods: Foundations and Applications

1. Front Matter

   Pages I-X

   PDF

2. The Pragmatic Dimension of Formal Methods: Towards Building a Sound Synthesiser

   • Alexandre Mota

   Pages 1-4

3. Formal Design of Cloud Computing Systems in Maude

   • José Meseguer

   Pages 5-19

4. Source Code Analysis with a Temporal Extension of First-Order Logic

   • David Come, Julien Brunel, David Doose

   Pages 20-38

5. A Type-Directed Algorithm to Generate Well-Typed Featherweight Java Programs

   • Samuel S. Feitosa, Rodrigo Geraldo Ribeiro, Andre Rauber Du Bois

   Pages 39-55

6. Programming Language Foundations in Agda

   • Philip Wadler

   Pages 56-73

7. Formal Verification of n-bit ALU Using Theorem Proving

   • Sumayya Shiraz, Osman Hasan

   Pages 74-89

8. The Scallina Grammar

   • Youssef El Bakouny, Dani Mezher

   Pages 90-108

9. VDM at Large: Modelling the EMV^® \(2^{nd}\) Generation Kernel

   • Leo Freitas

   Pages 109-125

10. Constraint Reusing and k-Induction for Three-Valued Bounded Model Checking

    • Nils Timm, Stefan Gruner, Matthias Harvey

    Pages 126-143

11. TeSSLa: Temporal Stream-Based Specification Language

    • Lukas Convent, Sebastian Hungerecker, Martin Leucker, Torben Scheffel, Malte Schmitz, Daniel Thoma

    Pages 144-162Open Access

12. Automatic Test Case Generation for Concurrent Features from Natural Language Descriptions

    • Rafaela Almeida, Sidney Nogueira, Augusto Sampaio

    Pages 163-179

13. A Methodology for Protocol Verification Applied to EMV® 1

    • Leo Freitas, Paolo Modesti, Martin Emms

    Pages 180-197

14. Analysing RoboChart with Probabilities

    • M. S. Conserva Filho, R. Marinho, A. Mota, J. Woodcock

    Pages 198-214

15. Timed Scenarios: Consistency, Equivalence and Optimization

    • Neda Saeedloei, Feliks Kluźniak

    Pages 215-233

16. Safe and Constructive Design with UML Components

    • Flávia Falcão, Lucas Lima, Augusto Sampaio

    Pages 234-251

17. Formal Modelling of Environment Restrictions from Natural-Language Requirements

    • Tainã Santos, Gustavo Carvalho, Augusto Sampaio

    Pages 252-270

18. Back Matter

    Pages 271-271

    PDF

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.

• formal logic
• formal methods
• functional programming
• model checking
• program compilers
• programming languages
• semantics
• software engineering
• software evaluation
• specifications
• verification
• algorithm analysis and problem complexity

• Federal University of Campina Grande, Campina Grande, Brazil

  Tiago Massoni

• University of Leicester, Leicester, UK

  Mohammad Reza Mousavi

Policies and ethics