2LS: Static Analyser and Verifier, version 0.10

2LS: Nástroj pro statickou analýzu a verifikaci, verze 0.10

software

vyžadována - zdarma

Brain Martin (City University London)
Buecheli Samuel (UOx)
David Cristina (UBRIS)
Hruška Martin, Ing. (UITS FIT VUT)
Kroening Daniel (UOx)
Kumar Madhukar (IITD)
Malík Viktor, Ing. (UITS FIT VUT)
Martiček Štefan, Ing. (UITS FIT VUT)
Mukherjee Rajdeep (AmazonCom)
Nečas František, Bc. (FIT VUT)
Schrammel Peter, Dr. (US)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Watcher Björn (UOx)

2LS je nástroj pro verifikaci programů napsaných v jazyce C. Je postavený na infrastruktuře CPROVER, která podporuje C89, C99 a většinu C11 a rozšíření definovaných překladačemi GCC a Visual Studio. 2LS umožňuje verifikaci hranic polí (přetečení paměti), bezpečnosti práce s pamětí, výjimek, uživatelem definovaných tvrzení v programu a ukončitelnosti programu. Analýza v 2LS je založená na automatickém odvozovaní vlastností programu pomocí šablon a technikách zjemňování abstrakce.

https://github.com/diffblue/2ls/releases/tag/2ls-0.10

Volně šířitelný software poskytovaný pod licencí 4-clause BSD (pro přesné znění licence viz. https://github.com/diffblue/2ls/blob/master/LICENSE).

Centrum excelence v kyber-bezpečnosti v Estonsku a na Jižní Moravě (101087529)
Pokročilá analýza a verifikace pro pokročilý software GA142303001 (GA23-06506S)
Reliable, Secure, and Intelligent Computer Systems (FIT-S-23-8151)
Verifikace a validace spolehlivosti a bezpečnosti automatizovaných systémů (8A20009)