Teaching

Advanced Topics in Formal Verification - 236624

Course, The Technion, Computer Science Department, 2019

Topics

  • SAT and SMT
  • Bounded Model Checking
  • Finding Inductive Invariants with Interpolation and IC3/PDR
  • Verification using Constrained Horn Clauses
  • Hyper-properties and Security Verification

Introduction to Software Verification - 236342

Course, The Technion, Computer Science Department, 2020

Topics

  • Floyd proof rules
  • Temporal Logic
  • Model Checking for CTL and LTL
  • BDDs and Symbolic Model Checking
  • SAT and Bounded Model Checking