YASSi: Yet Another Symbolic Simulator Large (Tool Demo)

Authors Sebastian Pointner
Pablo Gonzalez-de-Aledo
Robert Wille
Editors Gabriele Kotsis
A Min Tjoa
Ismail Khali
Lukas Fischer
Bernhard A. Moser
Atif Mashkoor
Johannes Sametinger
Anna Fensel
Jorge Martínez Gil
Title YASSi: Yet Another Symbolic Simulator Large (Tool Demo)
Booktitle DEXA 2020: Database and Expert Systems Applications
Type in proceedings
Publisher Springer
Series Communications in Computer and Information Science
Volume 1285
ISBN 978-3-030-59027-7
DOI 10.1007/978-3-030-59028-4_3
Month September
Year 2020
Pages 25-31
SCCH ID# 20050
Abstract

Safety critical systems have finally made their way into our daily life. While recent industrial and academic research could already improve the design cycle for such systems, ensuring the functionality of such systems still remains an open question. Such systems which are composed of hardware as well as software components have to be checked since any wrong behavior of the system could end up in harming human life. To this end, program analysis techniques can be applied in order to ensure that the program works as intended and that no unwanted behavior is executed. However, approaches like static or dynamic program analysis which are widely applied for this purpose still lead a large number of fault positive results. To overcome such limitations an alternative approach called symbolic execution has been proposed. In this work, we present a tool called YASSi which implements this approach. Applying YASSi allows to symbolically execute programs written in the C/C++ language. By this, YASSi can be applied for several applications needed for the checking program for safety critical properties like (1) assertion checking, (2) reachability analysis, or (3) stimuli generation for digital circuits.