Abbrevation
EFM
City
Porto
Country
Portugal
Deadline Paper
Start Date
End Date
Abstract

A plethora of difficulties in software practice and momentous software faults continuously deliver reasons to believe that formal methods (FMs) will, in one or another way, have to play a key role in mastering these difficulties and in achieving the desired compound guarantees (e&#046;g&#046; dependability, security, performance) of future software&#8211;intensive systems&#046;<br>However, dependable software industry has not yet successfully adopted FMs as a vital part of their software engineering (SE) processes&#046; Many practitioners believe in the high potential of FMs and would use FMs to their maximum benefit, whether directly or through powerful tools&#046;<br>Sadly, the beneficial use of FMs still seems hindered by several obstacles&#046; But the lack of recent knowledge about these obstacles and the lack of recent knowledge about FM effectiveness and productivity raises a high demand for strong empirical research and goal&#8211;directed collaboration between academia and industry&#046; Interestingly, the low adoption of FMs in SE differs drastically from other engineering disciplines&#046;<br>We aim to strengthen the community<br>of researchers aiming at the compelling empirical validation of any aspects of FMs and<br>of practitioners supporting such validation as well as the sustainable transfer of FMs into dependable software practice&#046;<br>TOPICS OF INTEREST<br>For this single&#8211;day workshop, we kindly request<br>short research summaries, focused literature surveys<br>short experiences, opinions/positions, agendas, visions,<br>short or regular technical contributions<br>related (but not limited) to the following topics:<br>experiences in or surveys (e&#046;g&#046; systematic mappings and reviews, interview studies) of<br>FM transfers and applications (e&#046;g&#046; case studies),<br>challenges, limitations/barriers, and benefits of FMs,<br>evaluations of<br>tools, languages, frameworks, or platforms widely used in dependable software practice regarding their support of FMs,<br>the integration of FMs into programming techniques, SE methods, and SE processes,<br>new (automated) abstraction techniques,<br>comparisons of<br>projects applying FMs in practice with similar practical projects applying non&#8211;FM approaches,<br>FMs with similar approaches in traditional engineering,<br>benchmarks and metrics (beyond tool performance) for<br>the evaluation and comparison of FMs (e&#046;g&#046; fault&#8211;avoidance and fault&#8211;detection effectiveness),<br>usability and maturity assessment of FMs (e&#046;g&#046; abstraction effort, proof complexity, productivity),<br>research designs (e&#046;g&#046; for controlled field experiments) for the practical validation of FMs,<br>statements (see 2&#046;) on<br>FM integration and semantics unification,<br>future FM (empirical) research, education, and training&#046;<br>