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

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

Citovat

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.

@inproceedings{1649136,
   author = {Chalupa, Marek and Jašek, Tomáš and Tomovič, Lukáš and Hruška, Martin and Šoková, Veronika and Ayaziová, Paulína and Strejček, Jan and Vojnar, Tomáš},
   address = {Německo},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
   doi = {http://dx.doi.org/10.1007/978-3-030-45237-7_31},
   editor = {Armin Biere, David Parker},
   keywords = {Symbiotic;Predator;Program Slicing;Termination Analysis;Shape Analysis;Symbolic Execution},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Německo},
   isbn = {978-3-030-45236-0},
   pages = {413-417},
   publisher = {Springer},
   title = {Symbiotic 7: Integration of Predator and More (Competition Contribution)},
   url = {https://doi.org/10.1007/978-3-030-45237-7_31},
   year = {2020}
}

TY  - JOUR
ID  - 1649136
AU  - Chalupa, Marek - Jašek, Tomáš - Tomovič, Lukáš - Hruška, Martin - Šoková, Veronika - Ayaziová, Paulína - Strejček, Jan - Vojnar, Tomáš
PY  - 2020
TI  - Symbiotic 7: Integration of Predator and More (Competition Contribution)
PB  - Springer
CY  - Německo
SN  - 9783030452360
KW  - Symbiotic;Predator;Program Slicing;Termination Analysis;Shape Analysis;Symbolic Execution
UR  - https://doi.org/10.1007/978-3-030-45237-7_31
L2  - https://doi.org/10.1007/978-3-030-45237-7_31
N2  - 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.
ER  -

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. \textit{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.

Podrobný výpis o publikaci