Program Analysis for System Security and Reliability

Spring 2018
Prof. Dr. Martin Vechev

EDoz Link
EDoz link
Lecture Time and Place
Exercise Time and Place

The course introduces program analysis techniques (discrete and probabilistic) and shows how to apply these to build more secure and reliable systems across several application domains and scenarios, including: blockchain, computer networks and deep learning.


  1. Understand how classic program analysis and synthesis techniques work, including discrete and probabilistic methods.
  2. Understand how to apply the methods to generate attacks and create defenses against applications in blockchain, computer networks and deep learning.
  3. Understand the state-of-the-art in the area as well as future trends.

Part I: Analysis and Synthesis for Computer Networks
  • Analysis: Declarative analysis, Batfish
  • Synthesis: CEGIS, SyNET
  • Probabilistic: PSI, Bayonet

Part II: Security of Blockchain Applications
  • Introduction to space and tools
  • Symbolic Analysis, Abstract interpretation
  • Securify

Part III: Security and Robustness of Deep Learning
  • Basics: affine transforms, activation functions
  • Attacks: gradient based method to adversarial generation
  • Defenses: affine domains, AI2

Part IV: Probabilistic Security
  • Enforcement: PSI + Spire
  • Statistical De-obfuscation: CRFs + Analysis
  • Probabilistic de-obfuscation: JSNice, DeGuard, DeBIN

Lectures (Tentative Schedule):

No. DateContentSlides Exercises Solutions

Readings (Optional):