Formal Verification Courses and Certifications

Hausdorff Center for Mathematics

Modularity in PVS

Explore modularity concepts in PVS theorem proving, enhancing code organization and reusability for complex formal verification projects.

• YouTube
• 35 minutes
• On-Demand
• Free Video

Code Sync

When Testing Just Doesn't Cut It - Formal Verification in Mission-Critical Software

Explore formal verification techniques for mission-critical software, using a financial application example to demonstrate mathematical proofs beyond standard unit testing.

• YouTube
• 43 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Formal Runtime Error Detection in Automotive Software Development

Explore formal runtime error detection in automotive software development using inferred contracts and abstract interpretation for improved precision and scalability in module-level analysis.

• YouTube
• 22 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs

Explore formalization of parallel critical pairs in Isabelle, simplifying definitions and generalizing criteria for confluence and commutation in term rewrite systems.

• YouTube
• 31 minutes
• On-Demand
• Free Video

ACM SIGPLAN

UTC Time, Formally Verified - Presentation at CPP 2024

Explore formal verification of UTC time conversions using Coq and MathComp, including leap seconds implementation and refinement techniques for software verification projects.

• YouTube
• 31 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture

Explore the formalization of Giles Gardam's disproof of Kaplansky's Unit Conjecture using Lean 4, combining deductive proving and verified computation.

• YouTube
• 30 minutes
• On-Demand
• Free Video

ACM SIGPLAN

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams

Explore PfComp, a verified compiler for stateless firewall policies using binary decision diagrams. Learn about its Coq-assisted proof, OCaml extraction, and performance benefits.

• YouTube
• 31 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Memory Simulations, Security and Optimization in a Verified Compiler

Explore memory simulations, security features, and optimizations in verified compilers. Gain insights into pointer allocations, stack canaries, and tail recursion elimination in CompCert.

• YouTube
• 28 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Massive Proofs for the Masses

Explore massive proofs and their applications in computer science with Byron Cook's insightful presentation on cutting-edge verification techniques.

• YouTube
• 21 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation

Explore modular specification and verification of NOVA microhypervisor using concurrent separation logic. Discover challenges in formally verifying concurrent systems for enhanced virtualization and isolation.

• YouTube
• 24 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Modularizing CPU Semantics for Virtualization

Explore modularization of CPU semantics for efficient virtualization, focusing on simplifying VMM implementation and verification while addressing challenges in hardware-assisted virtualization.

• YouTube
• 25 minutes
• On-Demand
• Free Video

ACM SIGPLAN

CLOVER: Closed-Loop Verifiable Code Generation - Dafny'24

Explore CLOVER, a paradigm for ensuring correctness in AI-generated code through consistency checking among code, docstrings, and formal annotations using verification tools and language models.

• YouTube
• 20 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Verifying a Concurrent File System with Sequential Reasoning

Explore a verified, concurrent file system using GoTxn and Dafny. Learn about crash safety, concurrency, and combining interactive and automated proofs for robust systems software.

• YouTube
• 1 hour 7 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Trustworthy Formal Natural Language Specifications

Explore a novel approach to translating natural language specifications into formal claims within proof assistants, enhancing software verification and bridging the gap between informal and formal specifications.

• YouTube
• 30 minutes
• On-Demand
• Free Video

ACM SIGPLAN

Formal Verification of a Mechanical Ventilator Using UPPAAL

Explore formal verification of mechanical ventilators using UPPAAL, enhancing system reliability and correctness through advanced modeling techniques.

• YouTube
• 32 minutes
• On-Demand
• Free Video