Toward a tool to verify complex data structure invariants

Coq theorem prover;formal verification;separation logic;Computer Science

Roe, Kenneth DSmith, Scott F. ;

Johns Hopkins University

关键词: Coq theorem prover;    formal verification;    separation logic;    Computer Science;   

Others  :  https://jscholarship.library.jhu.edu/bitstream/handle/1774.2/59170/ROE-DISSERTATION-2018.pdf?sequence=1&isAllowed=y

瑞士|英语

来源: JOHNS HOPKINS DSpace Repository

【 摘 要 】

Formal methods provide the potential to create effective tools for finding bugs in software.However, the effectiveness of existing tools is limited: many existing static analysis tools provide limited abstractions, and interactive theorem proving techniques while providing deeper verifications are often too tedious to be practical.The goal of our research is to make interactive theorem proving techniques more practical to use.We started by developing the PEDANTIC framework in Coq which is based on Separation logic to document and reason about program invariants. Initial experience with PEDANTIC in Coq showed such reasoning to be quite tedious: proving invariants correct was slow and cumbersome.So, we next developed two tools aimed at improving prover productivity.First we developed CoqPIE, an interactive IDE aimed at streamlining common proof development tasks such as replaying theorems when there are changes.Next we developed an advanced rewriting library which gives Coq more powerfulexpression simplification algorithms.To stress test PEDANTIC and these new tools, we culminated with a verification of data structure invariants of the DPLL satisfiability solver algorithm, a complex 200-line C program.While the DPLL proof is not fully complete, key pieces of the proof are done and many important tactics and other building blocks were developed. Overall, the research presented gives a greater understanding of many proof development productivity issues and how to address these issues in practice.