PhD Oral Exam - Elif Deniz, Electrical and Computer Engineering

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

Abstract

Partial Differential Equations (PDEs) are central for the mathematical modeling of many physical and engineering problems such as heat transfer, the flow of fluids and the radiation of electromagnetic waves. Solving these equations is essential for gaining precise insights into the behavior of such systems. Traditionally, the analysis of PDEs has been performed using paper-and-pencil based proofs or computer-based numerical methods. However, these analysis techniques compromise the soundness and accuracy of their results, especially in safety-critical systems, due to the risk of human errors and inherent incompleteness of numerical algorithms. To address these limitations, we propose to use formal methods, in particular higher-order logic (HOL) theorem proving, for analyzing PDEs. The main motivation of this choice is the highly expressive and sound nature of HOL, which can be used to effectively model most systems that can be expressed in a closed mathematical form.

In this thesis, we introduce a comprehensive framework for the formal analysis of mathematical models of physical systems described by PDEs using the interactive proof assistant HOL Light. In particular, we have developed formal libraries for the heat, Laplace, telegrapher's and wave equations. Each library includes the formalization of these PDEs, encompassing their formal definitions and the formal verification of some classical properties as well as their analytical solutions. These libraries constitute distinct contributions, each providing substantial value for various applications. To demonstrate the practical utility and effectiveness of our proposed framework, we conduct the formal analysis of several physical systems such as thermal protection, transmission lines, and potential flows.