Automated Reasoning with SAT/QBF/SMT

Description

- 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.

Period	03 May 2016
Event title	Course on Automated Reasoning
Event type	Other
Location	RomaniaShow on map