Detail aplikovaného výsledku

2LS: Static Analyser and Verifier, version 0.10

KROENING, D.; MALÍK, V.; SCHRAMMEL, P.; VOJNAR, T.; MUKHERJEE, R.; MARTIČEK, Š.; NEČAS, F.; HRUŠKA, M.; BRAIN, M.; BUECHELI, S.; DAVID, C.; KUMAR, M.; WATCHER, B.

Originální název

2LS: Static Analyser and Verifier, version 0.10

Anglický název

2LS: Static Analyser and Verifier, version 0.10

Druh

Software

Abstrakt

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.

Abstrakt aglicky

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.

Klíčová slova

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

Klíčová slova anglicky

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

Umístění

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

Licenční poplatek

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

www

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