Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. It supports a wide range of program structures, data representations, and proof structures. Our approach supports reasoning about both safety and liveness properties. We implement our approach in a state-of-the-art verifier for the Rust language, which itself offers a strong foundation for memory safety. We demonstrate the practicality of our approach on a number of substantial case studies.

翻译：精化将抽象系统模型转化为具体的可执行程序，使得在抽象模型上确立的属性能够延续到具体实现中。精化已成功应用于多个实质性验证系统的开发。然而，现有精化技术存在限制其实际可用性的局限性。一些技术自动生成可执行代码，这通常会导致实现性能次优。另一些技术采用自底向上的程序验证来推理高效实现，但对代码结构、精化证明结构以及所使用的验证逻辑和工具提出了严格要求。本文提出了一种消除这些局限性的新型精化技术。该技术支持广泛的程序结构、数据表示和证明结构，并支持安全性与活性属性的推理。我们在Rust语言（该语言本身为内存安全提供了坚实基础）的最先进的验证器中实现了该方法。我们通过大量实质性案例研究证明了该方法的实用性。