Hoare Logic: Postconditions and Preconditions

About
Privacy
Disclaimer

Graph Chatbot

Related lectures (32)

Page 1 of 4

Hoare Logic: Strongest Postcondition and Weakest Precondition

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

Hoare Logic: Foundations and Applications

Covers Hoare Logic, its foundations, applications, and significance in program verification.

Encoder and Decoder for Prefix-Free Codes

Covers the implementation and verification of encoder and decoder for prefix-free codes, including classes and types, lemmas on trees, and the main theorem.

Verifying Programs with Stainless: Part 2

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

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Converting Imperative Programs to Formulas

Explores converting imperative programs to formulas, including verification conditions, formula construction, and control flow structures.

Untitled

Verifying Compiler: Spec# Approach

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

Formally Verified Chisel Designs

Explores formally verifying Chisel designs using SMT solvers and covers examples like delayed assertions and proofs by induction.

Introduction to Stainless: First Steps with Stainless

Introduces the Stainless verification tool with examples of verifying commutativity properties and arithmetic operations.