hackertube.io

Analyzing Programs with Z3

Compose Conference · talk · Watch on YouTube

Logic & formal methodsFunctional programmingCompilers, interpreters & program analysis

What it is

Tikhon Jelvis's Compose Conference talk on using the Z3 SMT solver to analyze and verify programs, including checking invariants with bounded loops. He demonstrates verifying programs in a small language by compiling them to Z3.

Why Hacker News recommends it

HN lists it among the practical entry points for learning Z3 and formal verification.

  • 2 people recommended it
  • 2 different months
  • 0 strong recommendations
  • first 2016, last 2021

What HN commenters said

  1. “It's easier than it sounds!”

    Verifying programs in a tiny language by compiling to Z3

    tikhonj, 2016-08 · Recommendation · in “Z3 SMT solver interactive tutorial”

  2. “the best one I've found as an entry point was the approach they use in Cryptol”

    Entry point to formal verification approach used in Cryptol

    buckie, 2017-07 · Recommendation · in “Show HN: Dharma – Programmable Peer-To-Peer Loans Using Ethereum Smart Contracts”

Excerpts from Hacker News comments, linked to the originals. Summaries and labels were written by a language model from those comments.

Topics: z3, smt solver, formal verification, program analysis, haskell

Also recommended by the same people