Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Formal verification

Related lectures (30)

Automated Testing: Fuzzing and Sanitization

Explores fuzzing, bug oracles, code reviews, and automated testing techniques, emphasizing the importance of sanitization in detecting faults.

Verifying Programs with Stainless: Part 2

Focuses on using Stainless for program verification, demonstrating the process of verifying programs and ensuring correctness.

Static Analysis for Amy: Techniques and Implementations

Explores static analysis techniques like AST-based analysis and taint analysis applied to the Amy language.

Automated Reasoning: Formal Verification with LISA

Explores formal verification using the LISA proof assistant and the OCBSL Equivalence Checker.

Timing and Performance Analysis: Model Checking

Covers timing and performance analysis using model checking and multiple objective scheduling.

Verifying Compiler: Spec# Approach

Explores the Spec# programming system, focusing on a verifying compiler for C# 2.0.

Stochastic Hybrid Systems

Explores time-determinator model checking, U-Pool scheduling, worst-case execution time analysis, and statistical model checking for cyber-physical systems.

Correctness of Compilers: Part 1

Explores compiler correctness, examples of verified compilers, formal verification, and the challenges of certifying compilers.

Introduction to Formal Verification

Introduces formal verification, emphasizing rigorous proof of system correctness and the use of mathematical models.

Hoare Logic: Strongest Postcondition and Weakest Precondition

Covers Hoare logic, strongest postcondition, and weakest precondition for simplifying proofs in imperative programming.

Finite Element Analysis: Advanced Mechanisms in Engineering

Provides an overview of advanced mechanisms analysis using Finite Element Method and Finite Element Analysis in engineering applications.

Compiler verification: Challenges and Benefits

Explores the challenges and benefits of compiler verification, emphasizing the importance of verifying compilers for critical software.

Introduction to Quantifier Elimination for Presburger Arithmetic

Introduces formal verification methodology and Presburger arithmetic for program verification and automated reasoning.

Martingale-based Methods for Stochastic Systems

Explores martingales in stochastic systems, focusing on formal analysis, termination analysis, and stability verification.

Software security - Security testing

Covers software security testing approaches and coverage metrics.

From Tests to Proof

Explores software engineering concepts, emphasizing the significance of tests and clear specifications in ensuring software correctness.

Memory Model

Explores the formalization of memory models and their crucial role in program optimization.

Hoare Logic: Strongest Postcondition and Weakest Precondition

Introduces Hoare logic for simplifying program behavior proofs through annotations.

Kernel Integrity and Real-Time Systems

Explores kernel integrity, system security, and real-time system verification, emphasizing the importance of proving critical properties for building secure and timely systems.

Software Correctness: Testing and Verification Log in to Mediaspace to watch this video

Explores software correctness through testing, verification, property-based fuzzing, and dynamic information flow control.