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.