Sound static program analysis (SSPA) can tackle real-world programs and effectively prove, for instance, that they do not expose some runtime errors and security vulnerabilities. Over the past half-century, many theories, all amenable to abstract interpretation, have been proposed and applied in practice: program analysis, program verification through SMT solvers, type systems, and model checking are just the most notable examples. SSPA has had a great impact on the analysis of safety-critical embedded software (where a single bug might cause catastrophic effects on the physical world) but has achieved so far limited interest in desktop applications (where bugs do not have relevant consequences). An exception is the revival of SSPA in Web applications, where a security vulnerability (such as a SQL injection) within them might have a relevant business impact. More recent developments, such as the Internet of Things, in the past decade, have bridged the realm of embedded software with Web applications.

Modern software architectures, such as microservices and serverless computing, incorporate multiple programming languages and technologies, requiring a substantial effort to formalize and implement sound semantics. However, such applications are limited in size and communicate through simple and clear interfaces (e.g., REST APIs). In addition, current trends underline a wider and wider adoption of scripting languages, such as Python, in different contexts. Applying SSPA in this context might provide deep and structured feedback to usually non-professional developers. Finally, the recent machine learning revolution has drastically changed how software is developed (from providing intelligent code completions and generating code snippets to fully developing software via model training). This poses novel challenges to SSPA regarding soundness, precision, and scalability. Unfortunately, all those opportunities have not seen a resurgence so far in applying SSPA to industrial software. The main players in the market apply shallow and syntactic analyses, exposing our society to serious flaws.

The main goal of this Dagstuhl Seminar is to bring together the sound static program analysis and the software engineering communities to stimulate the extension of existing theories to these new trends and to disseminate the practitioner community about what has been done so far in this field and what could be the further developments in the future. In particular, discussing how SSPA can be integrated into software engineering practices, such as DevOps and the overall software development lifecycle, seems essential for the successful application of SSPA to modern software development practices.

The objectives of the seminar are to:

• Bring together the scientific and industrial communities of static analysis and software engineering to discuss and investigate how sound tools (based on formal methods) can achieve a relevant impact on modern software engineering practices.
• Explore topics and calls for funding opportunities to develop projects applying sound static analysis in modern software engineering practices.
• Discuss challenges to formal methods arising from modern software architectures.

Creative Commons BY 4.0

Pietro Ferrara, Liana Hadarean, Jorge Navas, and Caterina Urban