Basic Information
The Seminar Deals With Advanced Algorithms For Formal Verification. Topics Include# Reduction of Verification Problems to Constrained Horn Clauses (chcs), Algorithms For Deciding Satisfiability of Chcs, Hyper-properties, Their Applications in Formal Verification And Algorithms For Solving Them._ Learning Outcomes# Students Will Learn About State-of-the-art Research in The Domain of Formal Methods. Students Will Be Familiar With# - How to Represent Software Verification Problems As Constrained Horn Clauses (chcs). - Different Aspects in The Problem of Chc-sat Modulo Theories of First Order Logic._ - Solving Chc-sat With Partial Algorithms Which Are Based On Model Checking Algorithms For Finite Systems._ - Hyper-properties and Hyper-logics and Their Usage in Verification. - Reduction Techniques of Hyper-properties._ - The Use of Quantifiers in Hyper-properties, The Complexity And Algorithms to Solve Them.
Faculty: Computer Science
|Undergraduate Studies
|Graduate Studies
Pre-required courses
(234292 - Logic For Cs and 236342 - Introduction to Software Verification)