Aug. 10, 2020 · show notes

ABOUT THIS EPISODE

Show Notes and Links

Flo and Julian managed to get Marius Melzer into the recording studio and talk with him about his passion: Formal Verification. In this episode, we make a broader sweep compared to our earlier spotlight on Ada/SPARK and touch on many projects that are on-going in the formal verification community.

We discuss how to get going with formal verification and also touch on the theoretical underpinnings.

We forgot to mention it in the episode, but please also check out Marius’ other project: palava.tv!

Additional sound effects from https://www.zapsplat.com.

Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly.
Send feedback to podcast@ukvly.org or via Twitter.

Resources

Erlang
Elixir
Haskell
Haskell Programming from First Principles
Lambda Days
Coq
seL4
DeepSpec
Project Everest
Idris
Ada/SPARK
Isabelle
Lean
Frama-C
LiquidHaskell
F*

Technology

English

United States

Use API to fetch this episode in JSON

IN THIS EPISODE

marius melzer

Edit these tags

SHOW NOTES 🔗

00:00:00Intro

00:07:51What is Formal Methods?

00:13:09What happened since seL4?

00:15:44The French Tax System

00:17:55DeepSpec

00:20:36Project Everest

00:23:04What goes into a formally verified program?

00:34:10Theorem Provers

00:37:30Type Systems

00:54:03Proves in existing languages

00:56:58Where do I start?

01:02:30Outro

TRANSCRIPT 🔗

Are you the producer of this podcast? Add a podcast transcript

Need Audio-to-Text? Transcribe with Listen411 in Just 60 Seconds

SEARCH PAST EPISODES

Search past episodes of Syslog.

Embed this search bar to your website

OTHER EPISODES IN THIS PODCAST

Genode Labs - with Norman Feske

Feb. 6, 2020

Show Notes and Links Flo and Julian talk with Norman Feske, one of the founders of Genode Labs, about how to turn an idea into a company. We touch on operating system research, the Genode OS Framework, and Sculpt OS. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #u…