Discussion meeting
This is a summary of the group meeting on 30 September 2020
Xie: Array Fold Logic (CAV 16′)
SUMMARY:
Main contribution: devised the syntax and semantic of array fold logic and proved the decidability of this logic. The core part of array fold logic is
fold_a v f, where v is a vector and f is a function depend on different guards, when the guard is met there are updates to the counters, iterator and state or break.
This formula will eventually produce an output vector v’.
As for the decidability proof, the main idea of the proof of complexity is using reversal bounded CFG to bound the value range of variables, length of array and array elements. Therefore the variables and arrays can be simulated by an NTM, thus proving the membership. As for hardness, we can induce the emptiness problem of intersection of DFAs to sat of AFL formula.
The decision procedure, utilize the existent reachability decision procedure of symbolic counter machines for the decision algorithm of AFL formulas.
DISCUSSION:
Q1: Currently the variables and constants are of integer type, what happens if we change it into a float or double type?
Q2: Whether can we utilize this logic for bitvectors, such as the comparation, separation and combination of bitvectors?
Q3: The paper stated that the logic cannot express sortedness, what if we store the element to a variable?
A3: The syntax of update only allows the update of counters and state variable, not the free explicit input variable and we cannot store the value of element to these variables.
Q4: What properties are considered in the experiment?
Shizhen: Benchmarking Software Model Checkers on Automotive Code (NFM 20′)
本文聚焦于SV-COMP参赛工具在自动生成代码上性质验证的表现以及其与工业界中实用工具的比较。实验所用测试程序是通过应用模型自动生成，待验证的性质为invariants及bounded-response properties，被测试的工具包括11个参与SV-COMP2018竞赛的工具、根据测试代码特性优化的CBMC+k-induction以及工业界使用的 BTC Embedded Validator。实验结果为BTC可以对90%+的性质做验证，CBMC+k-induction可以对60%+的性质做验证，而SV-COMP的工具只能验证20%的性质。因此作者提出对目前的开源验证工具做针对数据集的优化手段是有必要的。
问：这篇论文中提到SV-COMP竞赛中针对工具的validation检查，这部分具体是怎么进行的呢？
这部分是通过要求每个工具在验证后给出witness，然后挑选性质验证工具（论文中提到的是CPAChecker和Ultimate）对witness进行验证，我理解这一部分或许可以通过自动机相乘来实现。
问：在该论文中CBMC+k-induction在两个数据集都可以验证较多性质，这是否表明该工具可以更好适用于自动生成代码的性质验证？
论文中提到的CBMC+k-induction是文章作者为了说明在原有的工具中做一些小优化会在实际应用时具有很明显的性能提升，但在这里引入的k-induction是针对benchmark做的优化，本身并不具有普适性。