Lecture

Separation is all you need: Foundations for Modular Verification

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture by the instructor covers the foundations for modular verification of realistic concurrent programs using Separation Logic. It discusses the challenges of concurrency, the importance of achieving thread-locality by keeping threads separated, and the application of Separation Logic to achieve this goal. The lecture also explores the weak spots of Separation Logic, the success story of Separation Logic in verification tools, and the complexities of shared mutable state in concurrent programs. It delves into the intricacies of reference counting, ghost permissions, and the formal verification of microkernel IPC. The lecture concludes with a discussion on the Rust programming language, its type system, and the challenges of ensuring safety in Rust programs.

Official source

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages

Related concepts (32)

Rust (programming language)

Rust is a multi-paradigm, general-purpose programming language that emphasizes performance, type safety, and concurrency. It enforces memory safety—ensuring that all references point to valid memory—without requiring the use of a garbage collector or reference counting present in other memory-safe languages. To simultaneously enforce memory safety and prevent data races, its "borrow checker" tracks the object lifetime of all references in a program during compilation.

System programming language

A system programming language is a programming language used for system programming; such languages are designed for writing system software, which usually requires different development approaches when compared with application software. Edsger Dijkstra refers to these languages as machine oriented high order languages, or mohol. General-purpose programming languages tend to focus on generic features to allow programs written in the language to use the same code on different platforms.

Type system

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Zig (programming language)

Zig is an imperative, general-purpose, statically typed, compiled system programming language designed by Andrew Kelley. It is intended to be a replacement for the C programming language, with the goals of being even smaller and simpler to program in while also offering modern features, new optimizations and a variety of safety mechanisms while not as demanding of runtime safety as seen in other languages. It is distinct from languages like Go, Rust and Carbon, which have similar goals but also target the C++ space.

Programming language

A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming language is usually split into the two components of syntax (form) and semantics (meaning), which are usually defined by a formal language. Some languages are defined by a specification document (for example, the C programming language is specified by an ISO Standard) while other languages (such as Perl) have a dominant implementation that is treated as a reference.

Related lectures (64)

Programming Language Security

Explores programming language security, covering type safety, memory safety, threat safety, Rust's ownership model, sandboxing, and compartmentalization.

Taming Null References

Explores the challenges of null references in programming languages and proposes solutions to mitigate their drawbacks while ensuring compatibility with existing codebases.

Formally Correct Intermittent Systems

Focuses on designing formally correct intermittent systems in batteryless systems powered intermittently, addressing challenges and strategies for ensuring correctness.

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.

Verified Functional Programming: Nicolas Voirol public PhD thesis defense