Five Kinds of Nondeterminism
(buttondown.com)
No newsletter next week, I'm teaching a TLA+ workshop.
No newsletter next week, I'm teaching a TLA+ workshop.
Comparing Two Verilog CPU Implementations Using EBMC
(philipzucker.com)
About a year ago my friends and I built a 4bit cpu out of a kit from aliexpress. https://www.philipzucker.com/td4-4bit-cpu/ It’s a lot of fun. I also think the system is so simple that is is kind of a nice target for tinkering around with formal methods.
About a year ago my friends and I built a 4bit cpu out of a kit from aliexpress. https://www.philipzucker.com/td4-4bit-cpu/ It’s a lot of fun. I also think the system is so simple that is is kind of a nice target for tinkering around with formal methods.
Nvidia Security Team: “What if we just stopped using C?” (2022)
(adacore.com)
Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today.
Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today.
Preventing conflicts in authoritative DNS config using formal verification
(cloudflare.com)
Over the last year, Cloudflare has begun formally verifying the correctness of our internal DNS addressing behavior — the logic that determines which IP address a DNS query receives when it hits our authoritative nameserver.
Over the last year, Cloudflare has begun formally verifying the correctness of our internal DNS addressing behavior — the logic that determines which IP address a DNS query receives when it hits our authoritative nameserver.
Compiling C to Safe Rust, Formalized
(arxiv.org)
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C, and cannot be realistically rewritten by hand. Automatically translating C to Rust is thus an appealing course of action.
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C, and cannot be realistically rewritten by hand. Automatically translating C to Rust is thus an appealing course of action.
The Hoare Cube
(wordpress.com)
I wrote earlier this year about my attempt to understand the repercussions of toggling and when giving a semantics to Hoare triples.
I wrote earlier this year about my attempt to understand the repercussions of toggling and when giving a semantics to Hoare triples.
Discharging Lean goals into SMT solvers
(github.com/ufmg-smite)
This project is inspired by SMTCoq and aims to provide Lean tactics that discharge goals into SMT solvers. It is under active development and is currently in a beta phase. While it is ready for use, it is important to note that there are still some rough edges and ongoing improvements being made.
This project is inspired by SMTCoq and aims to provide Lean tactics that discharge goals into SMT solvers. It is under active development and is currently in a beta phase. While it is ready for use, it is important to note that there are still some rough edges and ongoing improvements being made.
Modelling the archetype of a message-passing bug with TLA+ (2022)
(medium.com)
Two years ago, I tried to describe “the archetype of a message-passing bug”, using both a real-world example in Rust, as well as plain English.
Two years ago, I tried to describe “the archetype of a message-passing bug”, using both a real-world example in Rust, as well as plain English.