Let’s verify this with Why3

François Bobot,Jean-Christophe Filliâtre,Claude Marché,Andrei Paskevich

International Journal on Software Tools for Technology Transfer (STTT)（2014）

引用 66|浏览52

暂无评分

摘要

We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.

查看译文

关键词

Formal specification,Deductive verification,Automated theorem proving,Case study

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要