Product Details

2LS: Static Analyser and Verifier, version 0.10

Created: 2023

Czech title
2LS: Nástroj pro statickou analýzu a verifikaci, verze 0.10
Type
software
License
required - free
Authors
Brain Martin (City University London)
Buecheli Samuel (UOx)
David Cristina (UBRIS)
Hruška Martin, Ing. (DITS FIT BUT)
Kroening Daniel (UOx)
Kumar Madhukar (IITD)
Malík Viktor, Ing. (DITS FIT BUT)
Martiček Štefan, Ing. (DITS FIT BUT)
Mukherjee Rajdeep (AmazonCom)
Nečas František, Ing. (FIT BUT)
Schrammel Peter, Dr. (US)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Watcher Björn (UOx)
Keywords

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

Description

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.

Location
Licence

Free software under the 4-clause BSD license (see https://github.com/diffblue/2ls/blob/master/LICENSE for details).

Projects
Back to top