Symbiotic 7: Integration of Predator and More (Competition Contribution)

Informace o publikaci

Autoři	CHALUPA Marek JAŠEK Tomáš TOMOVIČ Lukáš HRUŠKA Martin ŠOKOVÁ Veronika AYAZIOVÁ Paulína STREJČEK Jan VOJNAR Tomáš
Rok publikování	2020
Druh	Článek ve sborníku
Konference	Tools and Algorithms for the Construction and Analysis of Systems
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	https://doi.org/10.1007/978-3-030-45237-7_31
Doi	http://dx.doi.org/10.1007/978-3-030-45237-7_31
Klíčová slova	Symbiotic;Predator;Program Slicing;Termination Analysis;Shape Analysis;Symbolic Execution
Popis	Symbiotic 7 brings improvements in all parts of the tool. In particular, we integrated the advanced shape analysis implemented in Predator to our instrumentation process for memory safety checking. Further, we extended our slicer to correctly handle non-terminating programs. This new slicing is applied in termination analysis, where we also added instrumentation for detection of simple cycles in the program state space. The witness generation process changed as well.
Související projekty:	Abstrakce a jiné techniky v semi-symbolické verifikaci programů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX

Studijní programy