PL/Verification @ MPI-SWS

PL/Verification research at MPI-SWS focuses on the principles of programming languages, on their design and implementation, and on foundational techniques and practical tools for the analysis, testing, and verification of programs against their correctness specifications. Recent research has focused on techniques for verifying compilers and other critical software, verification and testing tools for concurrent systems, and the design of modular programming languages.

Projects

• ALStypes: Asynchronous liquid separation types
• Backpack: Retrofitting Haskell with interfaces
• C11comp: Reasoning about C11 program transformations
• Cave: A tool for proving linearizability of concurrent libraries
• Ceal: A C-based language for self-adjusting computation
• FSL: A program logic for C11 concurrency with support for memory fences
• GPS: A program logic for C11 concurrency
• IRIS: A concurrent program logic based on monoids and invariants
• llvmcs: Formalizing the concurrency semantics of LLVM
• Mtac: A monad for typed tactic programming in Coq
• OGRA: The Owicki-Gries method for the RA memory model
• Paco: A Coq library for parameterized coinduction
• Pilsner: A compositionally verified compiler for a higher-order imperative language
• RCMC: Model checking for C/C++ concurrency
• RSL: A (simple) program logic for C11 concurrency
• RustBelt: Logical foundations for the future of safe systems programming
• SCfix: Repairing sequential consistency in C/C++11
• SRA: Strong release-acquire consistency
• Trns: Explaining relaxed memory models with program transformations
• Transactions: On the semantics of weakly consistent transactions
• validC: Validating optimizations of concurrent C/C++ programs

Imprint | Data Protection