STRESS 2024

International School on Tool-based Rigorous Engineering of Software Systems

The International School on Tool-based Rigorous Engineering of Software Systems (STRESS) series aims to provide top-quality lectures and innovative pedagogical material that provide young researchers with:

• Instructions in existing and emerging formal methods and software engineering techniques that are tool-supported and process-oriented
• Insights into how software is developed in the real world, including emphasis on domains such as safety/mission-critical software and embedded systems where the development effort associated with tool-based formal methods promises greatest returns
• Case-studies and example domains in which formal methods have been successfully transitioned into actual development along with insights in how to bridge the gap between research tools and actual development processes
  
• Additional pedagogical resources and personal contacts that they can explore for the purpose of increasing the impact of their research.

Developer-friendly Integrated Coding and Verification with Slang and Logika

Stefan Hallerstede – Aarhus University
John Hatcliff – Kansas State University

Developing verified code for embedded systems is challenging. To be effective, code should be both (a) clean and include abstractions amenable to verification as well as (b) efficient and predicatable with respect to execution speed and resource utilization.

This series of tutorials presents the Slang programming language (a safety-critical subset of Scala) and its accompanying verification framework called Logika. Slang is designed to support software contract-based verification but can also be transpiled to C and Rust to obtain effective embedded system implementations. The Logika verifier is supported by a sophisticated integrated development environment within the IntelliJ IDE that provides a number of useful visualizations of contract verification status, automatically discovered program facts, and developer-friendly displays of how program constraints are converted to SMT queries. Slang/Logika are also unique in that they support an integrated language for manual program proofs to complement automated SMT-based verification. Logika also provides a programmer-friendly interface to the  SMT-based proof support. As a consequence, the tool can also be used without prior education in theorem proving.

Development of Slang and Logika has been funded via several industry partnerships with US defense companies. We will conclude with an overview of industry-research applications of Slang and Logika and its ongoing integration with Rust verification. This overview will include walkthroughs of model-driven development of medical devices and applications within US aerospace companies.

STRESS will take place from October 22, 2024 to October 25, 2024.