The Gradual Verifier
The Gradual Verifier
复制标题
渐进验证者
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
N. Shankar
中科院分区：
文献类型：
--
作者：
Stephan Arlt;Cindy Rubio;P. Rümmer;Martin Schäf;N. Shankar
静态验证传统上产生是/否的答案。它要么提供一段代码满足某个属性的证明，要么提供一个反例，表明该属性可以被违反。因此，静态验证的进展很难衡量。与测试不同，覆盖度量可以用于跟踪进度，静态验证不提供任何中间结果，直到可以计算正确性证明。由于静态验证器不可避免的不完整性，这尤其是个问题。
为了克服这一点，我们提出了一个渐进的验证方法，重力。对于一段给定的Java代码，Gravy将语句划分为不可访问的语句，或者是不可能、不可避免或可能的异常终止语句。进一步的分析可以集中在后一种情况。也就是说，即使某些语句仍然可能异常终止，Gravy仍然计算部分结果。这使我们能够衡量静态验证的进展。我们提出了一个实现的Gravy和评估它在几个开源项目。
Static verification traditionally produces yes/no answers. It either provides a proof that a piece of code meets a property, or a counterexample showing that the property can be violated. Hence, the progress of static verification is hard to measure. Unlike in testing, where coverage metrics can be used to track progress, static verification does not provide any intermediate result until the proof of correctness can be computed. This is in particular problematic because of the inevitable incompleteness of static verifiers.
To overcome this, we propose a gradual verification approach, GraVy. For a given piece of Java code, GraVy partitions the statements into those that are unreachable, or from which exceptional termination is impossible, inevitable, or possible. Further analysis can then focus on the latter case. That is, even though some statements still may terminate exceptionally, GraVy still computes a partial result. This allows us to measure the progress of static verification.We present an implementation of GraVy and evaluate it on several open source projects.