|9:00 AM||Registration||Opening Session||Registration|
|9:30 AM||FMSchool – Tutorial #1||Invited Speaker #1||Invited Speaker #2|
|10:30 AM||Coffee Break||Coffee Break||Coffee Break|
|11:00 AM||FMSchool – Tutorial #1||Technical Session #1||Technical Session #2|
|12:30 PM||Lunch Time|
|2:00 PM||FMSchool – Tutorial #2||Panel Discussion||Technical Session #3|
|3:30 PM||Coffee Break||Coffee Break||Coffee Break|
|4:00 PM||Visiting the University||FM Committee Meeting||Invited Speaker #3|
|5:00 PM||Closing Session|
|8:00 PM||Conference Dinner|
FMSchool – Tutorial #1
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
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.
Keynote Speaker #1
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
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
SBMF – Technical Session #2
SBMF – Technical Session #3
Chair: Tiago Massoni
Applying Formal Methods in Industry