Detail publikace
2LS: Memory Safety and Non-termination (Competition Contribution)
MALÍK Viktor, MARTIČEK Štefan, SCHRAMMEL Peter, SRIVAS Mandayam, VOJNAR Tomáš a WAHLANG Johanan. 2LS: Memory Safety and Non-termination (Competition Contribution). In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2. Lecture Notes in Computer Science, roč. 10806. Thessaloniki: Springer International Publishing, 2018, s. 417-421. ISBN 978-3-319-89962-6. Dostupné z: https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24
Název česky
2LS: analýza bezpečnosti práce s pamětí a neukončitelnosti (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)
Martiček Štefan, Ing. (FIT VUT)
Schrammel Peter, Dr. (US)
Srivas Mandayam (CMI)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Wahlang Johanan (CMI)
Martiček Štefan, Ing. (FIT VUT)
Schrammel Peter, Dr. (US)
Srivas Mandayam (CMI)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Wahlang Johanan (CMI)
URL
Klíčová slova
verifikace programů, ukončitelnost, neukončitelnost, analýza tvaru haldy, syntéza invariantů
Abstrakt
2LS je nástroj pro analýzu programů v jazyce C postavený na platformě CPROVER. 2LS slouží k dokazování správnosti a hledání chyb v programech. Analýza využívá techniky založené na šablonách k nalezení invariantů programu a řadících funkcí a dále techniky rozbalování smyček k nalezení důkazů a protipříkladů pomocí k-indukce. Novými funkcemi pro letošní verzi jsou vylepšená analýza datových struktur alokovaných na haldě pomocí nové abstraktní domény a dále dvě techniky analýzy neukončitelnosti programů.
Rok
2018
Strany
417-421
Sborník
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2
Řada
Lecture Notes in Computer Science
Svazek
10806
Konference
European Joint Conferences on Theory and Practice of Software, Thessaloniki, GR
ISBN
978-3-319-89962-6
Vydavatel
Springer International Publishing
Místo
Thessaloniki, GR
DOI
UT WoS
000445822600024
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11892, author = "Viktor Mal\'{i}k and \v{S}tefan Marti\v{c}ek and Peter Schrammel and Mandayam Srivas and Tom\'{a}\v{s} Vojnar and Johanan Wahlang", title = "2LS: Memory Safety and Non-termination (Competition Contribution)", pages = "417--421", booktitle = "Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2", series = "Lecture Notes in Computer Science", volume = 10806, year = 2018, location = "Thessaloniki, GR", publisher = "Springer International Publishing", ISBN = "978-3-319-89962-6", doi = "10.1007/978-3-319-89963-3\_24", language = "english", url = "https://www.fit.vut.cz/research/publication/11892" }