For the past two years, I have been following with great interest a French conference on formal methods called "Forum Méthodes Formelles". It takes place every 6 months in Toulouse and is broadcasted live to Grenoble and Paris. Its unique characteristic is something we could call pair-presenting, where someone first presents a technique or tool (usually a scientist or tool developer) followed by someone else who presents an industrial use of the technique or tool (usually the industrial user herself). This is a format I have not found elsewhere, and which I find very effective at conveying the right ideas about what a tool/technique can achieve in practice, to a broad non-specialist audience (usually a good mix of academia and industry). This format is specially suited in my view to presenting formal methods, which are all too often considered a thing of specialists.
Since a few months, I am part of the program committee of this conference, so I'll report on this blog the conference topics that could be of interest to SPARK users. After considering in turn all major families of formal methods, the next topic is turning to the integration of formal methods with testing, whether to generate tests or combine proof and test (see program). The next conference will take place on June 16th, and you can already register (see links at the top of the page). Most presentations will be in French, except for the introductory talk by Klaus Havelund, a pillar of formal methods at NASA.
You can also access online videos & slides of all past conferences.