Formal Verification and Program Synthesis

About
Privacy
Disclaimer

Graph Chatbot

Related lectures (29)

Page 3 of 3

Concurrency Semantics and Verification

Explores concurrency semantics, recursive functions, loops, interleaving modeling, and interpreter verification.

Memory Models: Visibility and Semantics

Explains the Java Memory Model and thread start semantics for concurrent programs.

Concurrency and transactional memory in Dafny

Covers Dafny for formal verification, modeling concurrency, safety rules, liveness, and transactional memory concepts.

Formally Verified Chisel Designs

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

Readers-writer Lock

Introduces the readers-writer lock for handling concurrency in scenarios with frequent reads and occasional updates.

Stainless Verification System Tutorial

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

Introduction to Formal Verification

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

Concurrency Basics: Threads and Synchronization

Covers the basics of concurrency, focusing on threads and synchronization, including thread joining and challenges of non-deterministic execution.

Locking

Explores the concept of locking for mutual exclusion in OS, covering race conditions, parallelism, atomic instructions, deadlock prevention, and best practices.