Overview

This workshop provides a platform for the exchange of ideas between systems research and formal methods. Recent years have seen tremendous increase in reasoning power of formal verification techniques. Today formal methods are routinely applied during the design of processors. Device drivers are model checked. Microkernels and hypervisors have been fully formally verified.

With this workshop we want to stipulate further research in rigorous system design in this direction. We particular welcome contributions that ’’cross the border’’, which either apply established, adapted or new formal techniques to computer systems or use precise formal modelling within systems research. Systems papers, which show the need for formal reasoning, would be equally interesting.

Format

We plan to have one workshop-internal tutorial respectively invited talk on a practically successful technique in rigorous systems engineering. Another important goal of the workshop is to expose systems researchers to the new generation of formal verification tools, which scale to realistic systems and have been proven to produce better systems faster. Thus we will also have a second workshop-internal tutorial on new formal techniques applicable to systems research.
Beside the two invited talks we will ask for three types of submissions: original papers, short papers, and presentation-only papers. For the first set of papers we will have formal archived proceedings with an open access electronic publisher.

Topics

The topics we are interested include the following:
 static analysis and model checking
 interactive theorem proving
 formal security and reliability analysis
 automated testing
 decision procedures
 symbolic execution
 model-driven development
 software synthesis
 programming languages and tools
 domain-specific languages
 distributed and real-time systems
 experience reports

Further Information

• See the full workshop website, here.

Réalisation Axome - Création de sites Internet