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.
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.
The topics we are interested include the following:
static analysis and model checking
interactive theorem proving
formal security and reliability analysis
programming languages and tools
distributed and real-time systems
- See the full workshop website, here.