Automatic Modularization of Large Programs for Bounded Model Checking
| Autor: | Carsten Sinz, Marko Kleine Büning |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Model checking
050101 languages & linguistics business.industry Programming language Computer science Semantics (computer science) 05 social sciences 02 engineering and technology computer.software_genre Software Bounded function Scalability Modular programming 0202 electrical engineering electronic engineering information engineering Code (cryptography) 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences business computer TRACE (psycholinguistics) |
| Zdroj: | Formal Methods and Software Engineering ISBN: 9783030324087 ICFEM |
| DOI: | 10.1007/978-3-030-32409-4_12 |
| Popis: | The verification of real-world applications is a continuous challenge which yielded numerous different methods and approaches. However, scalability of precise analysis methods on large programs is still limited. We thus propose a formal definition of modules that allows a partitioning of the program into smaller code fragments suitable for verification by bounded model checking. We consider programs written in C/C++ and use LLVM as an intermediate representation. A formal trace semantics for LLVM program runs is defined that also takes modularization into account. Using different abstractions and a selection of fragments of a program for each module, we describe four different modularization approaches. We define desirable properties of modularizations, and show how a bounded model checking approach can be adapted for modularization. Two modularization approaches are implemented within the tool QPR-Verify, which is based on the bounded model checker LLBMC. We evaluate our approach on a medium-sized embedded system software encompassing approximately 160 KLoC. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|