Combining Symbolic Execution with Predicate Abstraction and
CEGAR

D 2024

Combining Symbolic Execution with Predicate Abstraction and CEGAR

JONÁŠ, Martin; Jan STREJČEK a Alberto GRIGGIO

Základní údaje

Originální název

Combining Symbolic Execution with Predicate Abstraction and CEGAR

Autoři

JONÁŠ, Martin; Jan STREJČEK a Alberto GRIGGIO

Vydání

Wien, Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024, od s. 272-280, 9 s. 2024

Nakladatel

TU Wien Academic Press

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Rakousko

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/24:00139765

Organizační jednotka

Fakulta informatiky

ISBN

978-3-85448-065-5

DOI

https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_33

EID Scopus

2-s2.0-105007734023

Klíčová slova anglicky

program verification; symbolic execution; predicate abstraction; CEGAR

Štítky

core_B, firank_B, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 30. 7. 2025 14:27, Mgr. Michal Petr

Anotace

V originále

The paper presents a simple, yet effective program verification technique that combines symbolic execution with implicit predicate abstraction and CEGAR. The technique can prove correctness of many programs that are beyond the reach of the standard symbolic execution because their symbolic execution tree is prohibitively large or even infinite. The technique has been implemented in the software model checker KRATOS. Our experimental evaluation shows that it also decides correctness of some programs that were decided neither by the standard symbolic execution nor by IC3 with predicate abstraction (all implemented in KRATOS).

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

Citovat

JONÁŠ, Martin; Jan STREJČEK a Alberto GRIGGIO. Combining Symbolic Execution with Predicate Abstraction and CEGAR. Online. In Nina Narodytska, Philipp Rümmer. Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024. Wien: TU Wien Academic Press, 2024, s. 272-280. ISBN 978-3-85448-065-5. Dostupné z: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_33.

@inproceedings{2486571,
   author = {Jonáš, Martin and Strejček, Jan and Griggio, Alberto},
   address = {Wien},
   booktitle = {Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024},
   doi = {https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_33},
   editor = {Nina Narodytska, Philipp Rümmer},
   keywords = {program verification; symbolic execution; predicate abstraction; CEGAR},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Wien},
   isbn = {978-3-85448-065-5},
   pages = {272-280},
   publisher = {TU Wien Academic Press},
   title = {Combining Symbolic Execution with Predicate Abstraction and CEGAR},
   url = {https://repositum.tuwien.at/handle/20.500.12708/200800},
   year = {2024}
}

TY  - CONF
ID  - 2486571
AU  - Jonáš, Martin - Strejček, Jan - Griggio, Alberto
PY  - 2024
TI  - Combining Symbolic Execution with Predicate Abstraction and CEGAR
PB  - TU Wien Academic Press
CY  - Wien
SN  - 9783854480655
KW  - program verification
KW  - symbolic execution
KW  - predicate abstraction
KW  - CEGAR
UR  - https://repositum.tuwien.at/handle/20.500.12708/200800
N2  - The paper presents a simple, yet effective program verification technique that combines symbolic execution with implicit predicate abstraction and CEGAR. The technique can prove correctness of many programs that are beyond the reach of the standard symbolic execution because their symbolic execution tree is prohibitively large or even infinite. The technique has been implemented in the software model checker KRATOS. Our experimental evaluation shows that it also decides correctness of some programs that were decided neither by the standard symbolic execution nor by IC3 with predicate abstraction (all implemented in KRATOS).
ER  -

JONÁŠ, Martin; Jan STREJČEK a Alberto GRIGGIO. Combining Symbolic Execution with Predicate Abstraction and CEGAR. Online. In Nina Narodytska, Philipp Rümmer. \textit{Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024}. Wien: TU Wien Academic Press, 2024, s.~272-280. ISBN~978-3-85448-065-5. Dostupné z: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5\_{}33.

Přehled o publikaci