Correctness (computer science)

Formal sciences
Theoretical computer science
Programming language theory
Formal verification

About
Privacy
Disclaimer

Graph Chatbot

Related lectures (23)

Page 2 of 3

Automated Reasoning: Formal Verification with LISA

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

Rigorous System Design

Explores the challenges of designing reactive systems, emphasizing correctness and productivity in system design.

Trustworthy Systems Research

Discusses the need for proven trustworthiness in computer systems and the rigorous approach to achieving true trustworthiness in critical systems.

Correctness of Compilers: Part 2

Explores the correctness of compilers, emphasizing expression evaluation, bytecode compilation, and stack operations.

An Introduction to Iris: Higher-Order Concurrent Separation Logic

Introduces Iris, a logical framework for reasoning about safety and correctness of concurrent higher-order imperative programs, emphasizing its unique characteristics and applications.

Verifying Programs with Stainless

Explores the verification of programs using Stainless, focusing on functional correctness, proof assistants, and automation of reasoning tasks.

From Tests to Proof

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

Hoare Logic: Strongest Postcondition and Weakest Precondition

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

Data Abstraction: Modules and Specifications in Coq

Discusses data abstraction in programming, focusing on modules and specifications in Coq.

Calcul and Algorithms: Quadratic Equation Example

Covers control structures, quadratic equation algorithm design, and correctness verification.