For Teams Interested in Competing for the Formal Methods Special Recognition

Teams can compete for the special recognition granted by the Formal Methods Europe (FME) group for outstanding exploitation of formal methods regardless of the project they choose to develop.

Formal methods encompass a variety of rigorous techniques and tools such as formal verification techniques (model checking, static analysis, and so on), refinement development methods (VDM, the B method, and so on), and formal notations for requirements and specifications (finite-state automata, Petri nets, Z, and so on). There is no fixed list of formal methods teams can choose to use. As a general guideline, however, teams choosing formal methods should be able to make a rigorous case that the formal techniques, tools, and methods they used ensure some correctness, reliability, or quality guarantee of the resulting project. For example, if they use a model checker to detect deadlocks in a scheduler implementation, they could argue that the scheduling policies they implemented do not deadlock under the assumptions implicit in the formal model they constructed. Teams can choose whether to use formal methods throughout project development, or limit their use to specific development tasks or to some aspects of the application.

Within the SCORE 2016 Program Committee, Matteo Rossi acts as ambassador for the FME group, and as reference person for teams interested in competing for the Formal Methods special recognition. He is available to answer questions from teams regarding the application of formal methods in SCORE 2016 projects, such as whether a project lends itself to the use of formal methods and which parts of a project are most suitable for the application of formal methods.