CHALUPA, Marek, Tomáš JAŠEK, Lukáš TOMOVIČ, Martin HRUŠKA, Veronika ŠOKOVÁ, Paulína AYAZIOVÁ, Jan STREJČEK a Tomáš VOJNAR. Symbiotic 7: Integration of Predator and More (Competition Contribution). In Armin Biere, David Parker. Tools and Algorithms for the Construction and Analysis of Systems. Německo: Springer, 2020, s. 413-417. ISBN 978-3-030-45236-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-45237-7_31.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 12:25.
Anotace
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 VaVNá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 MUNá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
VytisknoutZobrazeno: 24. 4. 2024 18:46