Formal methods (FM) have a rich history spanning a half-century. Mathematical proof of properties of programs have been sought since the early days of computing. Despite these aspirations, FM has not taken hold due to barriers of scale, usability, engineering realism, and mission incentives. Indeed, for decades, FM tools and ecosystems could only operate on problems and systems of modest scale. There has nonetheless been strong impetus to continue the advance of FM driven by emerging uses of computing hardware and software in critical systems such as space and aircraft flight control, communication security, and cryptography. Recently, however, FM has advanced to the point that techniques are breaking through the barriers and being adopted in a broader range of engineering organizations where reliability and assurance are highly critical, particularly in cloud infrastructure, operating system kernels, and other applications. This is timely, because assurance needs are ramping up due to the growing sophistication of modern cyber threats, as well as the increase in complexity and interconnection of systems. Indeed, many of the modern applications of FM address scale and interconnection challenges through emphasis on composition, integration with modern tooling, and better accessibility for mainstream software developers, including invisible FM, where FM-originated techniques are built in to languages and tools in ways that yield the benefits while nonetheless “hiding the math” from developers.
This special issue of IEEE Security & Privacy aims at understanding how the FM community, working in partnership with sponsors and users, is achieving broader use of this critical technology and at increasing levels of scale. Still further, this special issue seeks to present this discussion in a form accessible to a general audience of researchers and practitioners thereby increasing the understanding of the community around FM. In the long history of FM, we have experienced both major steps forward and also some crises of expectations. Some have suggested that we might be at a new inflection point--and so it is important to consider the landscape. Topics include, but are not limited to:
Submissions due: 30 November 2021
Publication: May/June 2022
For author information and guidelines on submission criteria, please visit the Author Information page. Please submit papers through the ScholarOne system, and be sure to select the special-issue name. Manuscripts should not be published or currently submitted for publication elsewhere. Please submit only full papers intended for review, not abstracts, to the ScholarOne portal.
Contact the guest editors at sp3-22@computer.org.
