LastMile - Narrowing the Usability Gap of Software Verification

Formal software verification technology has advanced rapidly in recentyears, and we are finally seeing applications of research results inthis area that help practical software development. Nevertheless,despite an undeniable progress, the gap between the state of the artof software verification and mainstream programming practices remainswide, especially for techniques that target the analysis of complexbehavioral properties. Support for language features that arecommonly used in real-world software, such as object-orientedabstraction mechanisms and concurrency models of differentgranularity, is rarely fully available even in the latest softwareverification tools. More commonly, each technique or tool supportsonly a set of specific features, which makes using it on complexrealistic programs impractical.The overall objective of project LastMile is narrowing this gap at the``last mile'' of software verification technology: between the latestresearch results and their practical usability on realistic software.Work in the project targets three main contributions, corresponding tothe work of three PhD students coordinated by the applicant: - LastMile's core contribution is a language-based framework to combine existing verification techniques and tools. The framework flexibly connects different programming and specification languages to different verification tools used as back ends. By decoupling the analyzed programs from the implementation details of the formal verification techniques, the framework accommodates, largely independent of each other, changes and extensions to the input language (for example, adding new features) or to the verification techniques. - Supporting within the framework the full verification of realistic object-oriented software written using idiomatic design patterns is another contribution of the project. This contribution combines various methodologies that have been developed over the years to capture and reason about different features of realistic object-oriented programs. By building atop the framework, this contribution also makes the research results available in practice and usable on the latest versions of common object-oriented languages such as Java. - With the wide availability of multicore processors, concurrent programming has become a necessity in many application domains. Still, writing correct concurrent programs is notoriously hard, and hence the help of formal software verification would be invaluable. Unfortunately, the verification of concurrent programs is an area where the gap between research and practice is especially pronounced. Project LastMile aims at bridging this gap by supporting the encoding of different concurrency synchronization models in a common language within the framework. This contribution will support the verification of concurrency features in combination with other features in a consistent way, so that realistic programs can be analyzed from different angles without having to give up any significant features. LastMile's results have the potential to positively affect progress offormal software verification by facilitating the integration of different techniques and by improving their applicability. They can also bring the evolution of programming languages closer to the latestprogress in analysis and verification techniques, which otherwise may take years, or even decades, to become available to practitioners. LastMile's ultimate impact depends not only on its scientificcontributions but also on whether these become available to other researchers and practitioners to implement and combine their software verification techniques. To this end, a part-time R&D engineer will participate in the project to ensure that development of the frameworkis carried out with state-of-the-art practices and that the various contributions are all merged consistently into it. The project's results will be disseminated by publication in major formal methods, verification, software engineering, and programming languages conferences and journals. The framework, tools, and infrastructure implemented as part of LastMile's work will target widely used programming languages and will be distributed publiclyunder suitable open source licenses.