PhD Application Talk: Proof Automation of Conditions of C-kernel Programs Correctness Based on PVS

The framework described in this thesis uses PVS as a core of proof automation process. PVS is a mechanized environment for formal specification and verification, as well as it enable to create, analyze, manage and document theories and proofs. PVS consists of a specification language, which is based on classical, typed higher-order logic, a number of predefined theories, a type checker and interactive theorem prover.
I developed and implemented a converter of correctness conditions into PVS theories. The converter is on Lisp language and a connecting part between the generator of correctness conditions and PVS. At first, verification conditions of C-kernel programs are translated to the PVS input format. Revelation of metavariables types and addition of special PVS theories, which are based on C-kernel semantics and necessary for subsequent proof, occur in the process of converting. After that verification conditions are simplified and finally combined into PVS theories. Assertion language has some constructions which weren't determined in the PVS language such as types definitions, metavariables and abstract functions. Therefore axiomatics was given for them. Also axiomatics of problem-oriented concepts was given for arrays and lists. This approach was successfully applied for verification of programs from test suite which included sorting programs and search in the unidirectional list.