R 2012

Symbiotic

SLABÝ, Jiří; Jan STREJČEK a Marek TRTÍK

Základní údaje

Originální název

Symbiotic

Autoři

SLABÝ, Jiří; Jan STREJČEK a Marek TRTÍK

Vydání

2012

Další údaje

Jazyk

angličtina

Typ výsledku

Software

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Odkazy

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/12:00062340

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

symbolic execution; slicing; bug-finding

Technické parametry

Symbiotic je statický analyzátor kódu, tedy nástroj pro hledání chyb v kódu aniž by tento kód přímo spouštěl. Pracuje nad programovacím jazyku C a sestává ze tří technik: instrumentace, slicing a symbolická exekuce. Instrumentace zavádí do kódu vlastnosti, které chceme kontrolovat, slicing odebírá kód nemající vliv na dané vlastnosti a konečně symbolická exekuce je přesný nástroj pro ověření těchto vlastností. Slicing v tomto případě napomáhá exekuci, protože vyřazuje nepotřebný kód, který by bylo jinak nutné (zbytečně) analyzovat. Licence: GPLv2 a klee Release License. Odpovědná osoba pro jednání: Jan Strejček, email: strejcek@fi.muni.cz; telefon: 549496941; adresa: Jan Strejček, Fakulta informatiky Masarykovy univerzity, Botanická 68a, 602 00 Brno.

Příznaky

Mezinárodní význam
Změněno: 23. 4. 2013 05:58, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We introduce a tool implementing a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs.

Návaznosti

LA09016, projekt VaV
Název: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Akronym: ERCIM)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Účast ČR v European Research Consortium for Informatics and Mathematics
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty