Detail publikace

2LS: Arrays and Loop Unwinding (Competition Contribution)

MALÍK, V.; NEČAS, F.; SCHRAMMEL, P.; VOJNAR, T. 2LS: Arrays and Loop Unwinding (Competition Contribution). In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2. Lecture Notes in Computer Science. Paris: Springer International Publishing, 2023. p. 529-534. ISBN: 978-3-031-30819-2.
Název česky
2LS: Analýza polí a rozbalování smyček (příspěvek do soutěže)
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Malík Viktor, Ing., Ph.D. (UITS)
Nečas František, Ing.
SCHRAMMEL, P.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

analýza programů, formální verifikace, odvozování invariantů, invarianty smyček, abstraktní interpretace, k-indukce, rozbalování smyček, abstraktní doména pro pole, analýza obsahu polí

Abstrakt

2LS je nástroj pro analýzu programů napsaných v jazyce C postavený na infrastruktuře CPROVER, který dokáže ověřovat platnost tvrzení v programu (assertions), bezpečnost práce s pamětí a ukončitelnost programu. Jednou z hlavních nevýhod 2LS byla doteď jeho neschopnost verifikovat programy pracující s polemi. Tento článek představuje novou abstraktní doménu pro 2LS určenou pro analýzu obsahu polí. K tomu navíc článek představuje vylepšený přístup k rozbalování smyček programu, který je klíčovou komponentou verifikačního algoritmu v 2LS. Tento přístup nově umožňuje nalezení důkazů korektnosti a protipříkladů v programech pracujících s dynamicky alokovanou pamětí.

Rok
2023
Strany
529–534
Sborník
Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2
Řada
Lecture Notes in Computer Science
Svazek
13994
ISBN
978-3-031-30819-2
Vydavatel
Springer International Publishing
Místo
Paris
DOI
10.1007/978-3-031-30820-8_31
EID Scopus
2-s2.0-85161470501
BibTeX 
@inproceedings{BUT187453,
  author="MALÍK, V. and NEČAS, F. and SCHRAMMEL, P. and VOJNAR, T.",
  title="2LS: Arrays and Loop Unwinding (Competition Contribution)",
  booktitle="Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2",
  year="2023",
  series="Lecture Notes in Computer Science",
  volume="13994",
  pages="529--534",
  publisher="Springer International Publishing",
  address="Paris",
  doi="10.1007/978-3-031-30820-8\{_}31",
  isbn="978-3-031-30819-2",
  url="https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_31.pdf?pdf=inline%20link"
}
Nahoru