%0 Conference Proceedings
%T Modeling Non-deterministic C Code with Active Objects
%+ Department of Computer Science
%+ Department of Computer Science and Engineering [Göteborg] (CSE)
%A Wasser, Nathan
%A Heydari Tabar, Asmae
%A Hahnle, Reiner
%Z Part 6: Program Analysis
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th International Conference on Fundamentals of Software Engineering (FSEN)
%C Tehran, Iran
%Y Hossein Hojjat
%Y Mieke Massink
%I Springer International Publishing
%3 Fundamentals of Software Engineering
%V LNCS-11761
%P 213-227
%8 2019-05-01
%D 2019
%R 10.1007/978-3-030-31517-7_15
%K Model extraction
%K Model validation
%K Parallelization
%Z Computer Science [cs]Conference papers
%X Cheap and ubiquitous availability of multi-processor hardware provides a strong incentive to parallelize existing software. We aim to annotate existing sequential applications written in C with OpenMP directives that can be processed by compilers on high performance parallel computers. We adopt a model-based approach, where from sequential C-code a software model is extracted in a largely automatic fashion. The target is the modeling language ABS (Abstract Behavioral Specification), an active objects-language with formal semantics. ABS has been designed to be statically analyzable. We focus on the first stages of model-based parallelization: model extraction and validation. We define a behavior-preserving, fully automatic translation of a large fragment of sequential C that explicitly renders all possible execution sequences, then use automated test case generation to produce validation test cases.
%G English
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-03769132/document
%2 https://inria.hal.science/hal-03769132/file/490001_1_En_15_Chapter.pdf
%L hal-03769132
%U https://inria.hal.science/hal-03769132
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-WG2-2
%~ IFIP-FSEN
%~ IFIP-LNCS-11761