2LS: Static Analyser and Verifier, version 0.10

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

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Kroening Daniel
Malík Viktor, Ing., Ph.D. (UITS)
Schrammel Peter
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Mukherjee Rajdeep
Martiček Štefan, Ing.
Nečas František, Ing.
Hruška Martin, Ing., Ph.D. (VZ Automata@FIT)
Brain Martin
Buecheli Samuel
David Cristina
Kumar Madhukar
Watcher Björn

formal verification, program analysis, template-based invariant synthesis, loop invariants, program safety, memory safety, termination analysis, abstract interpretation, k-induction, bounded model checking, abstract domain, heap shape domain, template polyhedra domain, single static assignment, SMT solving

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).

Cyber-security Excellence Hub in Estonia and South Moravia, EU, HORIZON EUROPE, 101087529, 2023-2026, řešení
Pokročilá analýza a verifikace pro pokročilý software, GAČR, Standardní projekty, GA23-06506S, 2023-2025, řešení
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, 2023-2026, řešení
Verifikace a validace spolehlivosti a bezpečnosti automatizovaných systémů, EU, Horizon 2020, 8A20009, 2020-2023, řešení

Ústav inteligentních systémů (UITS)