🦞🌯 Lobster Roll

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.

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: "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: "We present a formal verification approach for detecting design issues related to user interaction, with a focus on user interface of medical devices. The approach makes a novel use of configuration diagrams proposed by Rushby to formally verify important human factors properties of user i...

The author first introduces foundations like C0 subset of C language and Hoare logic. Then, author then builds a library for doubly-linked lists over arbitrary data types and a string library with 11 functions which includes most-used functions. Note: I changed tittle to say C0 instead of C to e...

Abstract: "With the increasing power of computers, real-time algorithms tends to become more complex and therefore require better guarantees of safety. Among algorithms sustaining autonomous embedded systems, model predictive control (MPC) is now used to compute online trajectories, for example in t...

Abstract: "Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal la...

Abstract: "In this thesis, we present a novel framework for the formal specification and verification of computer algebra programs and its application to a non-trivial computer algebra package. The programs are written in the language MiniMaple which is a substantial subset of the language of the c...

Has no abstract. Look at table of contents. She covers a lot of ground.

Abstract: "The design methodology of an embedded system should start with a system-level partitioning dividing functions into hardware and software. However, since this partitioning decision is taken at a high level of abstraction, we propose regularly validating the selected partitioning during sof...

Abstract: "This article answers fundamental safety questions for ground robot navigation: Under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective as well as the physical capa...

Abstract: "—With the increasing importance of software in the aerospace field, as evidenced by its growing size and complexity, a rigorous and reliable software verification and validation process must be applied to ensure conformance with the strict requirements of this software. Although importan...

Abstract: "Iterated Register Coalescing (IRC) is a widely used heuristic for performing register allocation via graph coloring. Many implementations in existing compilers follow (more or less faithfully) the imperative algorithm published in 1996. Several mistakes have been found in some of these i...

Abstract: "In current practices of system-on-chip (SoC) design a trend can be observed to integrate more and more low-level software components into the system hardware at different levels of granularity. The implementation of important control functions and communication structures is frequently s...

Trimmed abstract: "We present the first mechanized formal semantics of the BGP specification RFC 4271 [14], and we show how to use this semantics to develop reliable tools and guidelines that help BGP administrators avoid router misconfiguration. In contrast to previous semantics, our semantics is f...

Abstract: "Flash memory has become virtually indispensable in most mobile devices. In order for mobile devices to operate successfully, it is essential that flash memory be controlled correctly through the device driver software. However, as is typical for embedded software, conventional testing met...

Abstract: "This thesis basically splits up into two parts. The first part introduces the abstract model of the Vamos kernel. The Vamos kernel provides the infrastructure for process and memory management, priority-based round-robin scheduling, communication with external devices, as well as inter-p...

Abstract: "Many real programs are written in multiple different programming languages, and supporting this pattern creates challenges for formal compiler verification. We describe our Coq verification of a compiler for a high-level language, such that the compiler correctness theorem allows us t...

Abstract: "The development of complex system makes challenging task for correct software development. Due to faulty specification, software may involve errors. The traditional testing methods are not sufficient to verify the correctness of such complex system. In order to capture correct system re...

Abstract: "This paper presents the deductive formal verification of high-level properties of control systems with theorem proving, using the [Why3 tool](http://why3.lri.fr/). Properties that can be verified with this approach include stability, feedback gain, and robustness, among others. For the ...

Abstract: "A fast technique for proving steady-state analog circuit operation constraints is described. Based on SAT, the technique is applicable to practical circuit design and modeling scenarios as it does not require algebraic device models. Despite the complexity of representing accurate tra...

Abstract: "We present an approach to modeling and verifying machine-code programs that exhibit non-determinism. Specifi- cally, we add support for system calls to our formal, executable model of the user-level x86 instruction-set architecture (ISA). The resulting model, imp...