Play allFormal methods and verification
67 videos • 63 hr 49 min
Part of Computer science. Ordered by how many people recommended each video and for how long; 7 are classics.
1 2 3 "Finding bugs without running or even looking at code" by Jay Parlar
Strange Loop Conference
Recommended by 5 •
Classic4 5 "A Little Taste of Dependent Types" by David Christiansen
Strange Loop Conference
Recommended by 4 •
Classic6 7 Creator of OCaml: Functional Programming, Formal Verification, Programming Languages | Xavier Leroy
Ryan Peterman
Recommended by 2 •
Recent pick8 9 10 What if Current Foundations of Mathematics are Inconsistent? | Vladimir Voevodsky
Institute for Advanced Study
Recommended by 3 •
11 "Tackling Concurrency Bugs with TLA+" by Hillel Wayne
Strange Loop Conference
Recommended by 3 •
Classic12 In search of software perfection - 2016 Milner Award lecture by Dr Xavier Leroy.
The Royal Society
Recommended by 2 •
Hidden gem13 14 15 16 17 18 How to Find Bugs in Systems That Don't Exist - Hillel Wayne | SSW 2026
Software Should Work
Recommended by 2 •
Hidden gem19 20 Constraint Solvers for the Working PL Researcher - Nadia Polikarpova at PLMW@ICFP
UCSD Programming Systems
Recommended by 1 •
21 Ruslan Shevchenko at #ScalaUA - From Akka to Labelled Transition Systems
ScalaUA Conference
Recommended by 1 •
22 23 24 Scott Fleischman: Agda from Nothing: Order in the Types - λC Winter Retreat 2017
LambdaConf
Recommended by 1 •
25 MuniHac 2024 - So, Oct. 13 - Niki Vazou: Liquid Haskell: Verification with Refinement Types
TNG Technology Consulting GmbH
Recommended by 1 •
26 The Best New Programming Language is a Proof Assistant by Harry Goldstein | DC Systems 006
Antithesis
Recommended by 1 •
27 28 Lightning Talk: Turing Completeness Is Overrated: and here's why - Ben Deane - CppNow 2022
CppNow
Recommended by 1 •
29 RustBelt: Logical Foundations for the Future of Safe Systems Programming
Talks with Harley
Recommended by 1 •
30 Jubi Taneja presents "Improving Compiler Construction Using Formal Methods"
Berkeley Programming Systems
Recommended by 1 •
31 [Tutorial Fest @ POPL'23] Using a Proof Assistant to Teach PL Theory, Without the Overhead
ACM SIGPLAN
Recommended by 1 •
32 DEF CON 30 - Adam Zabrocki, Alex Tereshkin - Exploitation in the era of Formal Verification
DEFCONConference
Recommended by 1 •
33 34 Nuno Lopez 2022-10-08 11:00 GEP Pavillon Workshop on Dependable and Secure Software Systems
ETH WSCR
Recommended by 1 •
35 Ron Pressler - Why Writing Correct Software Is Hard and Why Math (Alone) Won’t Help Us - Curry On
Curry On!
Recommended by 1 •
36 37 2017 03 09 - Joachim Breitner - Why use theorem provers when we have compilers
Simon Meier
Recommended by 1 •
38 39 40 41 42 43 44 45 46 47 48 PLSE Seminar Series: Amal Ahmed, "Compositional Compiler Verification for a Multi-Language World"
UW PLSE
Recommended by 1 •
49 50 51 A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss | Code BEAM V
Code Sync
Recommended by 1 •
52 BOB 2017 - Philipp Kant: Performance and Safety: an Example of using Liquid Haskell in the Real Worl
BOBKonf
Recommended by 1 •
53 Gus Smith's Generals Talk: Generating Compiler Backends from Formal Models of Hardware
Gus Smith
Recommended by 1 •
54 Let’s Use An Automated Theorem Prover To Verify Video Games; I Swear This Is More Fun Than It Sounds
linux.conf.au
Recommended by 1 •
55 56 57 Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch
TLA+ - The Temporal Logic of Actions
Recommended by 1 •
58 Dharma Shukla: TLA+ at Microsoft to build planetary-scale systems - Keynote TLA+ Community Event
TLA+ - The Temporal Logic of Actions
Recommended by 1 •
59 60 TLA+ in Engineering Systems – Quinceañera - David Langworthy
TLA+ - The Temporal Logic of Actions
Recommended by 1 •
61 62 Byron Cook: Formal Reasoning about the Security of Amazon Web Services
Federated Logic Conference FLoC 2018
Recommended by 2 •
Hidden gem63 Five Stages of Accepting Constructive Mathematics - Andrej Bauer
Institute for Advanced Study
Recommended by 1 •
64 seL4 Is Free – What Does This Mean For You?
Linux.conf.au 2015 -- Auckland, New Zealand
Recommended by 1 •
65 NVIDIA — Securing the Future of Safety and Security of Embedded Software (Captioned)
AdaCore
Recommended by 1 •
66 67 Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification
Simons Institute for the Theory of Computing
Top upload •
