- Lecture 1: General Introduction to Formal Verification
Despite of extensive testing efforts, we cannot be sure that a hardware or software system is correct. As accurately pointed out by E. Dijkstra, "testing shows the presence, not the absence of bugs". In general not all possible test cases can be considered. Here, formal verification can help by using techniques of automated reasoning to prove the correctness of the system under consideration. In the first lecture, we will give an overview on the field of formal verification and introduce some of the most basic approaches like model checking.
- Lecture 2: Formal Verification with SAT
In the context of formal verification, one core technology is SAT solving. SAT, the decision problem of propositional logic, is the archetypical problem for the complexity class NP.
In the second lecture, we will introduce the basic principles of
state-of-the-art SAT solving and we will show concrete SAT encodings for verification problems.
- Lecture 3: Formal Verification with Formalisms Beyond SAT
In the third lecture, we will review formalisms which are more expressive than SAT, i.e., which allow more compact and user-friendly encodings of verification problems.
In particular, quantified Boolean formulas (QBF), the extension of
propositional logic with quantifiers and Satisfiality Modulo Theories (SMT) will be introduced and their application in formal verification will be demonstrated.
Sprache der Kurzfassung:
Eingeladener Vortrag an Universität
Details zum Vortragsort:
Sapientia Hungarian University of Transylvania, Cluj-Tg.Mures-M.Ciuc