Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution)

CHALUPA, Marek, Martin JONÁŠ, Jiří SLABÝ, Jan STREJČEK a Martina VITOVSKÁ. Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution). In Marsha Chechik and Jean-Francois Raskin. Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Berlin, Heidelberg: Springer, 2016, s. 946-949. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_67.

Základní údaje

Originální název

Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution)

Autoři

CHALUPA, Marek (203 Česká republika, domácí), Martin JONÁŠ (203 Česká republika, domácí), Jiří SLABÝ (203 Česká republika, domácí), Jan STREJČEK (203 Česká republika, garant, domácí) a Martina VITOVSKÁ (203 Česká republika, domácí)

Vydání

Berlin, Heidelberg, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, od s. 946-949, 4 s. 2016

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088244

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-49673-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_67

UT WoS

000406428000067

Klíčová slova anglicky

instrumentation; symbolic execution; program slicing

Štítky

bug-detection, formela-conference, program analysis, Symbiotic

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

Symbiotic 3 is a new generation of a bug-detection tool for C programs. The tool sticks to the combination of program instrumentation, slicing, and symbolic execution. Large parts of the tool are rewritten, in particular the managing and instrumentation scripts and slicer (including points-to analysis). Further, the symbolic executor Klee has been modified to produce error-witnesses. The changes are commented in the description of the tool workflow.

Česky

Symbiotic 3 je novou generací nástroje pro detekci chyb v programech v C. Nástroj nadále využívá kombinaci programové instrumentace, prořezávání a symbolické exekuce. Velké části nástroje byly přepsány, zejména řídící a instrumentační skripty a prořezávač (včetně points-to analýzy). Také jsme modifikovali symbolický exekutor Klee, aby poskytoval svědky chyb. Změny jsou komentovány v popisu běhu nástroje.

---

Návaznosti

GA15-17564S, projekt VaV	Název: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů Investor: Grantová agentura ČR, Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
MUNI/A/0935/2015, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0945/2015, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V. Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty