Task 4a: System APIs and Protocols TLS: nqsbTLS TCP: Huginn-TCP POSIX filesystem test oracle: SibylFS POSIX filesystem logic
Task 3: Systems Programming Languages Sequential C (de facto/ISO/CHERI): Cerberus Concurrent C: C/C++11 and new models C runtime typechecking: libcrunch ELF linking: linksem Verified ML implementation: CakeML JavaScript
Task 2: Architectural Multiprocessor Semantics Sail ISA models: ARM, Power, MIPS, CHERI L3 ISA models: ARM, MIPS, x86, CHERI, RISC-V ARM and Power Concurrency CHERI ISA
Task 1: Semantic tools Lem , L3 ISA DSL , Sail ISA DSL
Task 4b: Concurrency Reasoning