Logo Logo
Switch Language to German

Apel, Sven; Beyer, Dirk; Mordan, Vitaly; Mutilin, Vadim and Stahlbauer, Andreas (2016): On-the-Fly Decomposition of Specifications in Software Model Checking. 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering FSE 2016, Seattle, WA, USA, November 13 - 18, 2016. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery. pp. 349-361

Full text not available from 'Open Access LMU'.


Major breakthroughs have increased the efficiency and effectiveness of software model checking considerably, such that this technology is now applicable to industrial-scale software. However, verifying the full formal specification of a software system is still considered too complex, and in practice, sets of properties are verified one by one in isolation. We propose an approach that takes the full formal specification as input and first tries to verify all properties simultaneously in one run of the verifier. Our verification algorithm monitors itself and detects situations for which the full set of properties is too complex. In such cases, we perform an automatic decomposition of the full set of properties into smaller sets, and continue the verification seamlessly. To avoid state-space explosion for large sets of properties, we introduce on-the-fly property weaving : properties get weaved into the program's transition system on the fly, during the analysis;which properties to weave and verify is determined dynamically during the verification process. We perform an extensive evaluation based on verification tasks that were derived from 4 336 Linux kernel modules, and a set of properties that define the correct usage of the Linux API. Checking several properties simultaneously can lead to a significant performance gain, due to the fact that abstract models share many parts among different properties.

Actions (login required)

View Item View Item