Detail výsledku
2LS: Static Analyser and Verifier, version 0.10
Malík Viktor, Ing., Ph.D., UITS (FIT)
Schrammel Peter
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Mukherjee Rajdeep
Martiček Štefan, Ing., UITS (FIT)
Nečas František, Ing., FIT (FIT)
Hruška Martin, Ing., Ph.D., UITS (FIT)
Brain Martin
Buecheli Samuel
David Cristina
Kumar Madhukar
Watcher Björn
2LS ("tools") is a verification tool for C programs. It is built upon the CPROVER framework, which supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. It allows verifying array bounds (buffer overflows), pointer safety, exceptions, user-specified assertions, and termination properties. The analysis is performed by template-based predicate synthesis and abstraction refinements techniques.
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
Volně šířitelný software poskytovaný pod licencí 4-clause BSD (pro přesné znění licence viz. https://github.com/diffblue/2ls/blob/master/LICENSE).
Pokročilá analýza a verifikace pro pokročilý software, GAČR, Standardní projekty, GA23-06506S, zahájení: 2023-01-01, ukončení: 2025-12-31, ukončen
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Verifikace a validace spolehlivosti a bezpečnosti automatizovaných systémů, EU, Horizon 2020, 8A20009, zahájení: 2020-05-01, ukončení: 2023-07-31, ukončen