Grant: Discovery Grants Program - Individual

We have all experienced errors or bugs in software products. An error causing some text processing software to malfunction can be very annoying but it is normally not critical with serious consequences. On the other hand, if an error in a system affects a safety critical system such as the autopilot of an airplane or the control unit of a nuclear plant, failure is not acceptable. Software engineers usually develop good testing strategies allowing them to detect most errors hidden in programs, but testing can never guarantee that the program is free of errors. Formal methods are the study and application of mathematically-based techniques addressing this problem. They are used for the specification, development, and verification of software and hardware components. This is normally done by providing a condition that should be satisfied before executing a particular piece of code, another condition that will hold after executing the code and a proof of this fact. The verification process is usually complicated and very time consuming so that quite often (semi)automatic theorem provers are used in order to automate at least parts of the task. The importance of Formal Methods is indicated by the fact that a certification of a computer system following the Common Criteria for Information Technology Security Evaluation standard (ISO/IEC 15408) starting at level EAL5 requires the use of (semi)formal tools. Most approaches to formal methods are based on languages and calculi derived from first-order logic, i.e., they use the standard logical operations and quantifiers. On the other hand, recent experiments have shown that certain theorem provers work very successfully with algebraic theories, i.e., in situations where axioms and theorems are equations and proofs are calculations similar to those in regular algebra. This research will use the equational theory of binary relations in program specification, development, and verification by focusing on three major aspects. Firstly, the research will expand the mathematical theory and the calculus of binary relations into areas currently not yet developed such a parallel programming. Secondly, a library containing all aspects of the theory of relations and their implementation will be developed for the interactive programming language and theorem prover Coq. Since Coq is also a programming language we will be able to handle theory, proofs and implementation in one system. The library will be a base for all practical applications of the theory, i.e., any concrete development of verified software. Last but not least, these aspects and tools will be applied in order to develop correct software ranging from conceptual examples to real world applications.