D 2020

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

CHALUPA, Marek, Tomáš JAŠEK, Lukáš TOMOVIČ, Martin HRUŠKA, Veronika ŠOKOVÁ et. al.

Základní údaje

Originální název

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

Autoři

CHALUPA, Marek (203 Česká republika, garant, domácí), Tomáš JAŠEK (703 Slovensko, domácí), Lukáš TOMOVIČ (703 Slovensko, domácí), Martin HRUŠKA, Veronika ŠOKOVÁ, Paulína AYAZIOVÁ (703 Slovensko, domácí), Jan STREJČEK (203 Česká republika, domácí) a Tomáš VOJNAR (203 Česká republika)

Vydání

Německo, Tools and Algorithms for the Construction and Analysis of Systems, od s. 413-417, 5 s. 2020

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"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00114113

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-45236-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-45237-7_31

Klíčová slova anglicky

Symbiotic;Predator;Program Slicing;Termination Analysis;Shape Analysis;Symbolic Execution

Štítky

formela-conference, program analysis, program slicing, Symbiotic, verification

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2021 12:25, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA18-02177S, projekt VaV
Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů
MUNI/A/1050/2019, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
Zobrazeno: 28. 10. 2024 17:56