🦞🌯 Lobster Roll

Uses new tool, UC-KLEE, that builds on prior one I submitted here: https://lobste.rs/s/fzzbm0/klee_unassisted_automatic_generation

You can jump straight to the paper [here](https://www.wireguard.io/papers/wireguard-formal-verification.pdf) but the main page also has git instructions for reproduction.

Hi, I'd like to move my career towards formal methods and software verification. Almost every job posting understandably requires either an advanced degree or extensive prior work. I'm curious to hear from anyone who's landed a job in this area with minimal previous experience in this specializ...

By @ahelwer.

Abstract interpretation is a method static analyzers use to prove absence of bugs. [Astree Analyzer](http://www.astree.ens.fr) is one of the best. This paper describes the basic concepts of how it works.

Abstract: "In the first part of this thesis, we present a case study on successfully verifying the Linux USB BP keyboard driver. Our verification approach is (a) sound, (b) takes into account dynamic memory allocation, complex API rules and concurrency, and (c) is applied on a real kernel driver wh...

Abstract: "Program verification systems based on automated theorem provers rely on user-provided axioms in order to verify domain-specific properties of code. However, formulating axioms correctly (that is, formalizing properties of an intended mathematical interpretation) is nontrivial in practice,...

Abstract: "We study an automated verification method for functional correctness of parallel programs running on GPUs. Our method is based on Kojima and Igarashi’s Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop ...