Wasser, Nathan ; Tabar, Asmae Heydari ; Hähnle, Reiner (2021)
Automated model extraction: From non-deterministic C code to active objects.
In: Science of Computer Programming, 204
doi: 10.1016/j.scico.2020.102597
Article, Bibliographie
Abstract
The C programming language is well-known to have a large amount of underspecified behavior that often results in non-determinism even of sequential programs. In many application areas, not necessarily safety-critical ones, this is highly undesirable. A number of approaches and tools that statically analyze such behavior have been suggested, but they suffer from a high number of false positives and negatives. We present a novel model-based approach to analyzing non-determinism that works by automatic extraction of a faithful model of a given C program in a concurrent active object language. The extracted model renders any non-deterministic behavior of the C program in terms of explicit concurrency. This opens the door to global, semantic analyses. We give a fully formal account of the model extraction process and present an experimental evaluation of its implementation in the model extraction tool C2ABS.
| Item Type: | Article |
|---|---|
| Erschienen: | 2021 |
| Creators: | Wasser, Nathan ; Tabar, Asmae Heydari ; Hähnle, Reiner |
| Type of entry: | Bibliographie |
| Title: | Automated model extraction: From non-deterministic C code to active objects |
| Language: | English |
| Date: | 1 April 2021 |
| Publisher: | Elsevier |
| Journal or Publication Title: | Science of Computer Programming |
| Volume of the journal: | 204 |
| DOI: | 10.1016/j.scico.2020.102597 |
| Abstract: | The C programming language is well-known to have a large amount of underspecified behavior that often results in non-determinism even of sequential programs. In many application areas, not necessarily safety-critical ones, this is highly undesirable. A number of approaches and tools that statically analyze such behavior have been suggested, but they suffer from a high number of false positives and negatives. We present a novel model-based approach to analyzing non-determinism that works by automatic extraction of a faithful model of a given C program in a concurrent active object language. The extracted model renders any non-deterministic behavior of the C program in terms of explicit concurrency. This opens the door to global, semantic analyses. We give a fully formal account of the model extraction process and present an experimental evaluation of its implementation in the model extraction tool C2ABS. |
| Additional Information: | Art.No.: 102597 |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 19 Jul 2022 08:35 |
| Last Modified: | 20 Jul 2022 07:38 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum