• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
Master 2020/2021

Automated Methods for Program Verification

Type: Elective course (Data Science)
Area of studies: Applied Mathematics and Informatics
When: 1 year, 1, 2 module
Mode of studies: offline
Open to: students of all HSE University campuses
Instructors: Max Kanovich
Master’s programme: Data Science
Language: English
ECTS credits: 4

Course Syllabus

Abstract

The course acts as introduction to some of the most successful logic based concepts, tools and techniques used today in CS and IT, which are behind a major breakthrough in the practical applications in verification of systems and software. These methods are proven to be of great theoretical and practical potential in CS and IT. The topics of this course fall under the umbrella of what is called verification (a) Verification means to verify that a system satisfies some property. (b) The system can be a physical or software system. (c) The property is expressed using specifications within a certain logical language. The course has been designed in accordance with the most recent trends in the program verification. The challenge has been twofold: (1) to select the material and design the course so that to make it meet the actual needs of the CS applications, and (2) to do that so that to allow the students to learn and digest all necessary ideas to efficiently prove that the programs behave in the correct way.
Learning Objectives

Learning Objectives

  • To introduce students to techniques behind most impressive verification tools, which are based on <i> Hoare logics and <i> SAT solving.</i></i>
  • To cover <i> symbolic model checking and <i> symbolic execution.</i></i>
Expected Learning Outcomes

Expected Learning Outcomes

  • Software verification using SAT solvers.
  • Learn syntax and semantics of predicate logic with ensuring its orientation to the actual needs of computer science and information technology.
  • Understanding the importance of distinguishing syntax and semantics.
  • Formal description of predicate logic syntax.
  • Formal definition of interpretation of predicate logic domain (universe and interpretation of symbols).
  • Informal description of predicate logic formulas semantics, including connectives and quantifiers.
  • Learn semantics of predicate logic with ensuring its orientation to the actual needs of computer science and information technology.
  • Learn bound and free variables.
  • Learn formal semantics of predicate logic.
  • Learn validity, satisifiability, etc.
  • Introduced to reasoning about predicate logic formulas.
  • Understand the aim of the course.
  • Get a big picture on the materials to be covered by the course.
  • Specify programs formally using Hoare triples.
  • Manually run symbolic execution rules for loop-free programs.
  • Use symbolic execution rules to prove loop-free programs semi-automatically.
  • Understand an algorithm for generating loop invariants automatically.
  • Understand the definition of loop invariants.
  • Understanding SAT solvers.
  • Understanding the DPLL algorithm.
  • Apply Conflict-Driven Clause Learning as an efficient tool for SAT solving in practice.
  • Learning the basic of software verification using SAT solvers.
  • Understand how to translate programs into SAT.
Course Contents

Course Contents

  • Introduction to the course and basic concepts of verification
    <ul><li>Discuss the aim of the course and the basics concepts of verification.</li></ul>
  • Basic concepts of propositional logic
    <ul><li>Discuss propositional connectives.</li></ul>
  • Predicate logic as a language for CS
    <ul><li>Discuss several subtle examples of encoding problems into predicate logic.</li> <li>Discuss the importance of distinguishing syntax and semantics.</li> <li>Formally describe the syntax of predicate logic.</li> <li>Formally define the domain of interpretation of predicate logic (universe and interpretation of symbols).</li> <li>Informally describe the semantics of predicate logic formulas, including connectives and quantifiers.</li></ul>
  • Semantics of Predicate Logic
    <ul><li>Recap on the formal syntax of predicate logic.</li> <li>Bound and free variables.</li> <li>Formal semantics of predicate logic.</li> <li>Validity, satisifiability, etc.</li> <li>Brief introduction to reasoning about predicate logic formulas.</li></ul>
  • Hoare Triples <i>{P(x, y, z)} c {Q(x, y, z)}</i>
    <ul><li>Introduction to Hoare logic as the foundation of many successful techniques for formal verification of software.</li> <li>Provide intuition about program correctness through examples of program specifications in Hoare logic.</li> <li>Formally define the syntax and semantics of Hoare triples.</li> <li>Distinguish between the notion of partial and total correctness. </li><li>The importance of auxiliary variables.</li> <li>Use Hoare Triples to specify simple program in the While programming language.</li></ul>
  • Hoare Logic: Inference Rules
    <ul><li>Formally define inference rules of Hoare logic for reasoning about partial program correctness.</li> <li>Explain the connection between forwards and backwards axiom for assignment and weakest preconditions for assignment.</li> <li>Explain how reasoning about predicate logic formulas is used for verifying programs using Hoare Logic.</li> <li>Apply the Hoare Logic inference rules to prove (or disprove) correctness of loop free programs.</li> <li>Use loop invariants to prove correctness of programs with loops.</li> <li>Discuss the difference between inference rules for partial and total correctness.</li> <li>Discuss extensions of Hoare Logic to support other programming language features, such as pointers.</li></ul>
  • Symbolic Execution
    <ul><li>Classic (single-path) symbolic execution.</li> <li>Current applications and developments.</li></ul>
  • Hoare Logic and Symbolic Execution
    <ul><li>Recap: Syntax and semantics of while programs.</li> <li>Recap: Hoare triples.</li> <li>Proving Hoare triples of programs using forward symbolic execution.</li></ul>
  • Automatic Inference of Loop Invariants
    <ul><li>An algorithm for generating loop invariants automatically.</li></ul>
  • SAT Solvers
    <ul><li>What is SAT.</li> <li>Complexity issues and simple case of Horn Clauses.</li> <li>Normal forms for general case.</li> <li>Tseitin transformation.</li> <li>Understand the DPLL algorithm: <ul> <li>unit propagation,</li> <li>pure literal elimination.</li></ul></li> <li>Conflict-Driven Clause Learning as an efficient tool for solving the Boolean satisfiability problem in practice.</li></ul>
  • SAT Solvers, Symbolic model checking
    From code to propositional logic:<ul> <li>single static assignment;</li> <li>loop unfolding;</li> <li>basic of software verification using SAT solvers.</li></ul>
  • Software verification using SAT solvers
    <ul><li>How to translate programs in propositional formulas.</li> <li>How to translate assignments into propositional formulas.</li> <li>How to translate conditional statements into propositional formulas.</li> <li>The importance of using negation of assertions for verification.</li> <li>The use of assumptions for verification.</li></ul>
Assessment Elements

Assessment Elements

  • non-blocking Mid-term tests
  • non-blocking Final exam
Interim Assessment

Interim Assessment

  • Interim assessment (2 module)
    0.7 * Final exam + 0.3 * Mid-term tests
Bibliography

Bibliography

Recommended Core Bibliography

  • Koç, Ç. K. (ed.). Open problems in mathematics and computational science. – Springer, 2014.

Recommended Additional Bibliography

  • Peterson, L. L., Davie, B. S. Computer networks: a systems approach. – Elsevier, 2007. – 835 pp.