Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations. While some formally verified abstract interpreters have been written in the past, writing and understanding them requires expertise in the use of proof assistants, and requires a non-trivial amount of interactive proofs. This paper presents a formally verified abstract interpreter fully programmed and proved correct in the F* verified programming environment. Thanks to F* refinement types and SMT prover capabilities we demonstrate a substantial saving in proof effort compared to previous works based on interactive proof assistants. Almost all the code of our implementation, proofs included, written in a functional style, are presented directly in the paper.
翻译:抽象口译员是复杂的软件:即使抽象解释理论和配套算法得到很好的理解,其实施也会受到错误的影响,这可能对其计算是否正确产生疑问;虽然一些经过正式核实的抽象口译员过去曾写过,但撰写和理解这些解释员需要使用证明助理的专门知识,需要非三重的交互式证明,本文提供了经过正式核实的抽象口译员,在经过核实的F*编程环境中,经过充分编程并证明是正确的。由于F*精细类型和SMT证明能力,我们证明与以前基于互动证据助理的工程相比,在取证工作方面节省了大量费用。几乎所有执行守则,包括以功能风格书写的证据,都直接在文件中提出。