Detail publikace

2LS: Arrays and Loop Unwinding (Competition Contribution)

MALÍK Viktor, NEČAS František, SCHRAMMEL Peter a VOJNAR Tomáš. 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, roč. 13994. Paris: Springer International Publishing, 2023, s. 529-534. ISBN 978-3-031-30819-2. Dostupné z: https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_31.pdf?pdf=inline%20link
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
angličtina
Autoři
Malík Viktor, Ing. (UITS FIT VUT)
Nečas František, Ing. (FIT VUT)
Schrammel Peter, Dr. (US)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'23, Paris, FR
ISBN
978-3-031-30819-2
Vydavatel
Springer International Publishing
Místo
Paris, FR
DOI
10.1007/978-3-031-30820-8_31
EID Scopus
2-s2.0-85161470501
BibTeX 
@INPROCEEDINGS{FITPUB13064,
   author = "Viktor Mal\'{i}k and Franti\v{s}ek Ne\v{c}as and Peter Schrammel and Tom\'{a}\v{s} Vojnar",
   title = "2LS: Arrays and Loop Unwinding (Competition Contribution)",
   pages = "529--534",
   booktitle = "Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2",
   series = "Lecture Notes in Computer Science",
   volume = 13994,
   year = 2023,
   location = "Paris, FR",
   publisher = "Springer International Publishing",
   ISBN = "978-3-031-30819-2",
   doi = "10.1007/978-3-031-30820-8\_31",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13064"
}
Nahoru