Stories by matt_d

Partial sums of blsi and blsmsk

C4: The C Compiler Concurrency Checker

An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation

RISC vs. CISC is the Wrong Lens for Comparing Modern x86, ARM CPUs

Automatic Rust verification tools (2021)

20 Years of Networks-on-Chip (NoCs)

Verifying a Quantum Compiler

The ARM processor (Thumb-2), part 1: Introduction

RefinedC: Automating Foundational Verification of C Code with Refined Ownership

Differential Analysis of x86-64 Instruction Decoders [pdf]

Programming Language Design and Implementation (PLDI) 2021: Accepted Papers

Circuit Synthesis for Analog Computing

The Last CPU - HotOS XVIII: Hot Topics in Operating Systems (2021) [pdf]

Commodore’s Assemblers: Part 1: MOS Cross-Assembler

Verifying Vectorized Rust Revisited

Machine Learning in Compiler Optimization

Counterexamples in Type Systems

Atomics in AArch64

Formally Verified Speculation and Deoptimization in a JIT Compiler (POPL 2021)

Mostly harmless: An account of pseudo-normal floating point numbers

63 64 65 66 67 68 69 70 71 72