Treffer: Logika: the Sireum verification framework.

This article gives an overview of Logika – a highly automated and interactive verification framework, that is designed for scalability and usability across a wide spectrum of users from beginners to experts in formal methods. To support the intuition of developers, it emphasizes programming constructs and idioms in both its contract-based specifications and integrated proof language. To integrate with developer workflows, verification feedback is provided directly within the industrial strength IntelliJ & VSCode-based Sireum Integrated Verification Environment (IVE & CodeIVE) and is expressed directly in terms of code features instead of lower-level SMT constraints or theorem prover languages. To support tailoring to different domains and properties, Logika includes multiple extensibility mechanisms to customize property specifications, verification rules, and proof tactics. To scale to large systems, Logika provides carefully engineered incremental verification, and it leverages modern hardware for (massive) parallelization on server-based platforms. To illustrate the wide range of Logika use cases for effective formal methods, we describe how Logika is being used to teach large classes of undergraduate students as well as to support industrial defense-related research projects. We present Logika performance experiments on both infrastructure and application code used on industry projects within the HAMR model-driven development tool chain for the AADL SAE International and the upcoming SysML v2 standard architecture specification languages. [ABSTRACT FROM AUTHOR]

Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)