Advancing software model-checking by SMT interpolation beyond decidable arithmetic theories : an approach to verify safety properties in embedded and hybrid system models
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Electronic Thesis;
E-Book
Title:
Advancing software model-checking by SMT interpolation beyond decidable arithmetic theories : an approach to verify safety properties in embedded and hybrid system models
Contributor:
Mahdi, Ahmed
[Author]
imprint:
Carl von Ossietzky Universität Oldenburg: /oops/ - Oldenburger Online-Publikations-Server, 2017
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Verifying reachability of control-oriented software systems is an industrial quest which is becoming more complex to answer when programs involve arithmetic and probabilistic hybrid models. Whenever code segments of a program are unreachable, they are called dead codes. Detecting dead code is required in various standards for embedded system development. Most previous work can’t handle programs inducing non-linear arithmetic, as they are confined to linear programs. This restriction was overcome by combining several techniques that attack state space explosion and solve large arithmetic constraints system. Additionally, a variant of this technique would verify probabilistic reachability by computing the maximum probability of reaching bad states in a probabilistic model. Finally, a model-slicing approach is introduced to verify assumption-commitment properties in computational models which induce consistent transition system semantics.