TriCera Benchmarks: SMT-LIB Encodings of SV-COMP 2022 Benchmarks by TriCera

This repository contains the SMT-LIB v2.6 encodings of a subset of SV-COMP 2022 benchmarks from the <em>reach-safety</em> and the <em>memsafety</em> categories, encoded by TriCera and heap2array [1, 2]. The source benchmarks from SV-Comp 2022 (`.c` and `.i` files together with their accompanying `.yml` files) are not provided due to licensing reasons; the files are freely available for download at https://zenodo.org/record/5831003/export/hx - `benchmarks/heap` contains all heap benchmarks (encoded by TriCera using the theory of heaps, used in [1] and [2]).<br> - `benchmarks/heap2array` contains all heap2array encoded benchmarks (encoded from heap benchmarks using heap2array, used in [1] and [2]).<br> - `benchmarks/nonHeapBms` contains all non-heap benchmarks (encoded by TriCera, used in [2]). [1] (to appear) Zafer Esen and Philipp Rümmer, "An SMT-LIB Theory of Heaps", SMT 2022<br> [2] (to appear) Zafer Esen and Philipp Rümmer, "TriCera: Verifying C Programs Using the Theory of Heaps", FMCAD 2022本仓库收录了由TriCera与heap2array [1, 2] 编码生成的、取自SV-COMP 2022基准集**可达安全性（reach-safety）**与**内存安全性（memsafety）**类别的子集的SMT-LIB v2.6格式编码文件。 因授权许可限制，本仓库未提供SV-COMP 2022的原始基准集（含`.c`、`.i`文件及配套的`.yml`文件）；该类文件可通过链接 https://zenodo.org/record/5831003/export/hx 免费获取。 - `benchmarks/heap` 目录包含所有堆相关基准集的编码文件（由TriCera基于堆理论编码所得，已在文献[1]、[2]中使用）。 - `benchmarks/heap2array` 目录包含所有经heap2array转换的基准集编码文件（由heap2array从堆基准集转换而来，已在文献[1]、[2]中使用）。 - `benchmarks/nonHeapBms` 目录包含所有非堆相关基准集的编码文件（由TriCera编码所得，已在文献[2]中使用）。 [1]（待发表）Zafer Esen、Philipp Rümmer，《堆的SMT-LIB理论》，SMT 2022 [2]（待发表）Zafer Esen、Philipp Rümmer，《TriCera：基于堆理论验证C语言程序》，FMCAD 2022