Schedule

 11/2611/2711/28
 TUESDAYWEDNESDAYTHURSDAY
8:00 AMETMFSBMFSBMF
8:30 AM Registration 
9:00 AMRegistrationOpening SessionRegistration
9:30 AMFMSchool – Tutorial #1Invited Speaker #1Invited Speaker #2
10:00 AM
10:30 AMCoffee BreakCoffee BreakCoffee Break
11:00 AMFMSchool – Tutorial #1Technical Session #1Technical Session #2
11:30 AM
12:00 PM 
12:30 PMLunch Time
1:00 PM
1:30 PM
2:00 PMFMSchool – Tutorial #2Panel DiscussionTechnical Session #3
2:30 PM
3:00 PM
3:30 PMCoffee BreakCoffee BreakCoffee Break
4:00 PMVisiting the UniversityFM Committee MeetingInvited Speaker #3
4:30 PM
5:00 PMClosing Session
8:00 PM  Conference Dinner
10:00 PM  

ETMF Keynotes

FMSchool – Tutorial #1

Gustavo Carvalho

UFPE – Centro de Informática

Reasoning with the Coq proof assistant:

Coq is an interactive theorem prover to assist the development of machine-checked proofs. Among its many applications, it can be used to certify properties of programming languages and to prove correctness of algorithms. In this short course, we are going to cover the Coq basics: inductive definitions, functional programming with Coq, and the tactics language.

FMSchool – Tutorial #2

Thierry Lecomte 

CLEARSY Systems Engineering

Formal techniques for safer systems:

Designing safety critical systems is a difficult task, given the number of dimensions to analyse, the heterogeneity and the interdependency of the devices composing these systems, and sometimes the replacement of history-based systems with a unique interoperable one. To address all these issues, formal methods have been experimented on real life systems to ensure safety demonstration / verification at system, software and data levels. The combination of existing formal proof techniques and innovative modelling approaches makes possible the discovery of specification errors (even for systems already deployed), the completion of safety cases with a higher level of confidence and the seamless development of safety critical functions.
This talk is going to present:

  • several applications of this kind, 
  • the various technical frameworks used, sometimes in combination (B, EventB, Atelier B, ProB, CLEARSY Safety Platform), 
  • the added value and the results obtained so far.

Several demos and videos will exhibit the key points of the presentation.


SBMF Keynotes

Keynote Speaker #1

Gustavo Carvalho

UFPE – Centro de Informática

Generating test cases from natural-language requirements:

High trustworthiness levels are usually required when developing critical systems, and model-based testing (MBT) techniques play an important role generating test cases from specification models. Despite the benefits of MBT, those who are not familiar with the models syntax and semantics may be reluctant to adopt these formalisms. Furthermore, most of these models are not available in the very project beginning; typically, only natural-language requirements are available. In this talk, we present our efforts to develop a strategy for test generation from natural-language requirements (NAT2TEST), supporting different formalisms (Software Cost Reduction, Coloured Petri Nets, Communicating Sequential Processes, and Gallina), techniques (SMT solving, simulation, model checking, and interactive theorem proving) and tools (T-VEC, CPN tools, FDR, and Coq).

Short Bio: Gustavo Carvalho is a graduate of Centro de Informática (CIn) at Universidade Federal de Pernambuco (UFPE): BSc (2006), MSc (2010), and PhD (2016), the latter with periods at the University of Bremen (Germany) and at the University of York (UK). Since 2017, he is a lecturer at CIn-UFPE (www.cin.ufpe.br/~ghpc). His main research interest is on software engineering, with emphasis on tests and formal methods. He has authored about 25 peer-reviewed publications, besides reviewing papers for international conferences (FM, SEFM, ICTAC, TASE) and journals (SCP, SoSyM, IST). In 2017, he was the general chair of the XX Brazilian Symposium on Formal Methods (SBMF).


Keynote Speaker #2

Andreas Zeller

CISPA Helmholtz Center for Information Security / Saarland University – Computer Sicience

Explaining Program Behavior with Mined Input Grammars:

Knowing he input language of a program is a necessity for executing and testing it, but can also be helpful in explaining its behavior. In this talk, I show how to automatically mine input grammars from programs by dynamically tracking where and how input characters are used within the program; test generators specialized for input processors allow for mining input grammars even without any input samples. The resulting grammars can be used for quickly generating large numbers of syntactically correct inputs for exhaustive testing. As they are well-structured and very readable, they can also be used for program understanding: If two versions of a program process slightly different inputs, this will be reflected in differences in the mined grammars. If, however, grammars are learned only from a subset of inputs – e.g. those that cause a program to fail – the resulting grammars will capture these features and specifically produce similar inputs that are likely to cause more failures. All these techniques will be illustrated with live demos.

Short Bio: Andreas Zeller is Faculty at the CISPA Helmholtz Center for Infomation Security, and professor for Software Engineering at Saarland University, both in Saarbrücken, Germany. In 2010, Zeller was inducted as Fellow of the ACM for his contributions to automated debugging and mining software archives, for which he also obtained the ACM SIGSOFT Outstanding Research Award in 2018. His current work focuses on specification mining and test case generation, funded by grants from DFG and the European Research Council (ERC).

Chair: Philip Wadler (School of Informatics, University of Edinburgh)

 

 

SBMF – Technical Session #1

Chair: 

  • A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP
    Lucas Albertins de Lima, Amaury Tavares, Sidney Nogueira

  • A Domain-Specific Language for Verifying Software Requirement Constraints
    Marzina Vidal, Tiago Massoni, Franklin Ramalho

  • Use Case Evolution Analysis based on Graph Transformation with NACs
    Leila Ribeiro, Lucio Mauro Duarte, Rodrigo Machado, Andrei Costa, Érika Fernandes Cota, Jonas Santos Bezerra

SBMF – Technical Session #2

Chair:

  • The CLEARSY Safety Platform: 5 Years of Research, Development and Deployment
    Thierry Lecomte, David Deharbe, Paulin Fournier, Marcel Oliveira

  • Modelling and testing timed data-flow reactive systems in Coq from controlled natural-language requirements
    Gustavo Carvalho, Igor Meira

  • Formalizing the Dependency Pair Criterion for Innermost Termination
    Ariane Alves Almeida, Mauricio Ayala-Rincó

SBMF – Technical Session #3

Chair:

  • Ready, set, Go! Sound and complete data-race detection in the context of message passing
    Daniel Schnetzer Fava, Martin Steffen

  • A Polymorphic RPC Calculus
    Kwanghoon Choi, James Cheney, Simon Fowler, Sam Lindley

  • Analyzing Occupancy-Driven Thermal Dynamics in Smart Buildings using Model Checking
    Khaza Anuarul Hoque, Nathalie Cauchi, Alessandro Abate

Panel Discussion

Chair: Tiago Massoni

Applying Formal Methods in Industry