miniblog.

Feb 21, 2018 at 19:08

Crellvm: verifying LLVM optimisations with Coq: https://sf.snu.ac.kr/crellvm/ Impressively, they find bugs with optimisation passes which showed no bugs with fuzz testing!

Crellvm: Verified Credible Compilation for LLVM

Sep 29, 2020 at 16:37

Formally verifying a whitespace cleanup editor function in Coq!

Trusted Logic

Jan 23, 2020 at 04:01

Highlight of #POPL yesterday: seeing some excellent discussions of Coq for verifying programming languages! https://popl20.sigplan.org/details/PLMW-POPL-2020/3/Theorem-provers-are-a-P-L-researcher-s-best-friend I came away with a much clearer sense of *how* you'd verify an optimising compiler.

Theorem provers are a P.L. researcher's best friend (PLMW 2020) - POPL 2020

What is PLMW? The Programming Languages Mentoring Workshop (PLMW) aims to encourage graduate students and senior undergraduate students to pursue careers in programming language research. This workshop will bring together world leaders in programming languages research and teaching from academia and industry to provide (a) technical sessions on cutting-edge PL research and (b) mentoring sessions on how to prepare for a research career. The workshop will engage students in a process of imagining how they might contribute to our research community. We especially encourage women and underrepr ...

Jun 9, 2019 at 16:48

Defining a subset of #[no_std] Rust, formally verifying it, and releasing it as 'Sealed Rust' for use in safety critical systems like automotive and avionics:

Ferrocene

Part 1 - The Pitch

Related Posts