Schedule

	11/26	11/27	11/28
	TUESDAY	WEDNESDAY	THURSDAY
8:00 AM	ETMF	SBMF	SBMF
8:30 AM		Registration
9:00 AM	Registration	Opening Session	Registration
9:30 AM	FMSchool – Tutorial #1	Invited Speaker #1	Invited Speaker #2
10:00 AM
10:30 AM	Coffee Break	Coffee Break	Coffee Break
11:00 AM	FMSchool – Tutorial #1	Technical Session #1	Technical Session #2
11:30 AM
12:00 PM
12:30 PM	Lunch Time
1:00 PM
1:30 PM
2:00 PM	FMSchool – Tutorial #2	Panel Discussion	Technical Session #3
2:30 PM
3:00 PM
3:30 PM	Coffee Break	Coffee Break	Coffee Break
4:00 PM	Visiting the University	FM Committee Meeting	Invited Speaker #3
4:30 PM
5:00 PM			Closing Session
8:00 PM			Conference Dinner
10:00 PM

Location

All lectures and meetings will be held at CCSL Auditorium (IME-USP)

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)

 

Keynote Speaker #3

Philip Wadler

Joint work with Robert Bruce Findler and others.

Well-typed programs can’t be blamed

We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen’s contracts to a system similar to Siek and Taha’s gradual types and Flanagan’s hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.

Short Bio: Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK. He is an ACM Fellow, a Fellow of the Royal Society of Edinburgh, and editor-in-chief of Proceedings of the ACM for Programming Languages. He is past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 66 with more than 24,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O’Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.