Verifying Array Manipulating Programs with Full-Program Induction

Verifying Array Manipulating Programs by Tiling

Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers array access patterns in loops using simple heuristics, and then uses this information to compositionally prove universally quantified assertions about arrays. Specifically, we identify tiles of array accesses patterns in a loop, and use the tiling information to reduce the problem of checking a quantified assertion at the end of a loop to an inductive argum…

Deciding Memory Safety for Single-Pass Heap-Manipulating Programs

We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety--- determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidab…

声明式智能合约的安全性验证

Safety Verification of Declarative Smart Contracts

本文提出自动化安全验证工具DCV，针对DeCon语言编写的声明式智能合约，通过数学归纳法证明安全属性并自动推断归纳不变量，在20个基准合约上验证有效且速度优于基线工具。

基于电路的程序验证：将时序电路用作验证C程序的中间表示

Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs

本文提出CPV框架，将C程序转时序电路并调用硬件模型检查器，在16000+任务基准上验证，其性能与成熟软件验证器相当且可解决其他工具无法处理的任务。