Symbiotic

SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Symbiotic. 2012.

Základní údaje

• Originální název: Symbiotic
• Autoři: SLABÝ, Jiří (203 Česká republika, garant, domácí), Jan STREJČEK (203 Česká republika, domácí) a Marek TRTÍK (203 Česká republika, domácí).
• Vydání: 2012.

Další údaje

• Originální 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í
• WWW: Odkaz na stránku software
• 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: [e-mail]; telefon: [phone]; adresa: Jan Strejček, Fakulta informatiky Masarykovy univerzity, Botanická 68a, 602 00 Brno.
• Příznaky: Mezinárodní význam

Anotace

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