Interactive Theorem Proving

Traditional analysis techniques cannot ascertain an accurate analysis for the safety- and mission-critical applications of smart grids due to their inability to exhaustively specify and verify the systems. To overcome these issues, we propose the theorem proving based methodology for an accurate analysis of smart grid problems which can be modeled using stability, microeconomics and algorithm design theories. We choose the HOL Light theorem prover to develop the proposed formalizations due to the availability of foundational theories, such as set, differential, real and complex, in the HOL Light library. In this chapter, we present a brief overview of the HOL Light theorem prover and commonly used formalizations from the HOL Light library to facilitate the understanding of the proposed formalizations which are presented, in the rest of the book.