Proof Checker for Extended Linear Time Temporal Logic Proofs About Small Concurrent Programs

Abstract

Program verification is a time-consuming task and prone to errors when done manually. Verification tools are therefore essential when dealing with verification in larger scales. As of now, most verification tools use model checking when verifying program properties. Model checkers search for contradictions to properties regarding those programs, and if none are found then the property is considered valid. However, most model checkers are made for sequential programs, and with most modern environments using concurrency, the demands on the verification tools increase accordingly. With the success of model checking, formal proofs regarding concurrent programs have gotten little attention the past years. Conducting formal proofs can be tedious and error prone when done manually, but can also be very useful in terms certainty and gaining a more intuitive understanding of the problems. This thesis focuses on the development of a tool for formal proof checking of small concurrent programs. The tool was developed using the functional programming language Agda. A logic was implemented, along with a representation of a small programming language and a proof construction system. The final result of the project is a proof checking tool able to verify liveness proofs regarding arbitrary programs of the specified language. The proofs are conducted using predefined logic rules. If the proof can be implemented in the proof checker, the proof is considered valid. Agda turned out to be a useful tool for conducting formal proofs. The method of formal proofs for concurrent programs is still not preferable due to the complexity of the proofs, but with the development of more sophisticated automated theorem provers, the method may become increasingly viable in the future.