Formal Methods at Scale 2019 Workshops Report

Formal methods for systems assurance have a rich history spanning half a century. Even in the early days of computing, there were efforts directed at mathematical specifications and proof of properties of programs. Motivated by emerging uses of computing software and hardware in critical systems, several U.S. agencies invested in research in formal methods. For decades, however, formal methods tools and ecosystems could operate only on problems and systems of modest scale. Computer science students often had only limited exposure to formal methods techniques and tools, partly on the basis that the techniques were long considered to be a theoretical possibility but not a practical reality that could affordably provide real benefits to larger system and software engineering projects. Recently there have been revolutionary advances in tools, practices, training, and ecosystems that have facilitated the application of formal methods at larger scales, in a manner that is affordable and usable by professional software and hardware engineers. Recognizing the opportunity afforded by these advances, two workshops were convened in fall 2019 on the topic of formal methods at scale. This report provides a summary of those workshops, including their principal conclusions and relevant reports on experience in practice. The workshops included participants from the U.S. Government, industry, and academia, gathering to discuss recent advances that address the challenges of both scalability and adoptability into practice, including evidence from early adopters, with a focus on understanding prospects for the future and how they might be better enabled. Following the workshop, select formal methods practitioners from the community offered abstracts communicating use cases and related discussions of formal methods at scale. This report concludes with a discussion of key findings and emerging capabilities that can speed the adoption of formal methods.

[
  "100:65"
]

[
  "en-US"
]

[
  "000:000"
]

[
  "publications"
]