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