2LS ("tools") is a verification tool for C programs, built upon the CPROVER framework. It allows one to verify user-specified assertions, memory safety properties (e.g. buffer overflows), numerical overflows, division by zero, memory leaks, and termination properties. The analysis is performed by translating the verification task into a second-order logic formula over bitvector, array, and floating-point arithmetic theories. The formula is solved by a modular combination of algorithms involving unfolding and template-based invariant synthesis with the help of incremental SAT solving. Advantages of 2LS include its very fast incremental bounded model checking algorithm and its flexible framework for experimenting with novel analysis and abstraction ideas for invariant inference. Drawbacks are its lack of support for certain program features (e.g. multi-threading).

翻译：2LS（“tools”）是一款基于CPROVER框架构建的C程序验证工具。该工具支持验证用户指定的断言、内存安全属性（如缓冲区溢出）、数值溢出、除零错误、内存泄漏以及终止性属性。其分析过程通过将验证任务转化为基于位向量、数组和浮点算术理论的二阶逻辑公式来实现。该公式通过算法模块化组合求解，涉及展开、基于模板的不变量合成，并借助增量SAT求解技术。2LS的优势包括其极快的增量有界模型检验算法，以及用于实验新型不变量推断分析与抽象思想的灵活框架。其局限性在于对某些程序特性（如多线程）的支持不足。