Symbiotic 5: Boosted Instrumentation (Competition Contribution)

CHALUPA, Marek, Martina VITOVSKÁ a Jan STREJČEK. Symbiotic 5: Boosted Instrumentation (Competition Contribution). In Dirk Beyer and Marieke Huisman. Tools and Algorithms for the Construction and Analysis of Systems, 24th International Conference, Proceedings, Part II. Berlin: Springer, 2018, s. 442-446. ISBN 978-3-319-89963-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-89963-3_29.

Základní údaje

Originální název

Symbiotic 5: Boosted Instrumentation (Competition Contribution)

Autoři

CHALUPA, Marek (203 Česká republika, domácí), Martina VITOVSKÁ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Berlin, Tools and Algorithms for the Construction and Analysis of Systems, 24th International Conference, Proceedings, Part II, od s. 442-446, 5 s. 2018

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/18:00100910

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-89963-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-89963-3_29

UT WoS

000445822600029

Klíčová slova anglicky

Symbiotic; program analysis; program verification; SV-COMP 2018

Štítky

formal verification, formela-conference, program analysis, Symbiotic

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

The fifth version of Symbiotic significantly improves instrumentation capabilities that the tool uses to participate in the category MemSafety. It leverages an extended pointer analysis re-designed for instrumenting programs with memory safety errors, and staged instrumentation reducing the number of inserted function calls that track or check the memory state. Apart from various bugfixes, we have ported Symbiotic (including the external symbolic executor Klee) to llvm 3.9 and improved the generation of violation witnesses by providing values of some variables.

---

Návaznosti

GBP202/12/G061, projekt VaV	Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI) Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/0854/2017, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII. Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1038/2017, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18 Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/33/IP1/2018, interní kód MU	Název: Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky Investor: Masarykova univerzita, Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky