Mohua Banerjee, IIT Kanpur
Modal logic and algebra
In this course we discuss logic on models which are finite words (coloured linear orders), finite trees and generalizations. A set of models is called a “language”, and definability of languages by formulae will also be covered. First order logic, monadic second order logic and temporal logics can all be used to specify requirements that the models must satisfy. We discuss the motivation for using these different formalisms.
Formal verification employs logic to model the actual and intended behavior of computation systems, and uses logical inference to prove or refute the desired properties of these behaviors. Techniques for formal verification range from interactive proof checking to automated techniques based on theorem proving, satisfiability solving, and model checking. We review the basic foundations of logic and then examine the techology for interactive and automated verification as implemented in the PVS interactive theorem prover, the SAL model checker, and the Yices SMT solver. The use of these verification systems will be be illustrated through a range of examples.
- Logical foundations
- Basic interactive proofs with PVS
- Advanced features of PVS
- Model checking with SAL
- Satisfiability checking with Yices