miniblog.

← Back to all posts
Jul 3, 2017 at 18:57
Rather than verifying all possible compiler outputs, just check that the current output was optimised correctly!
Photo
Getting compilers right: a reliable foundation for secure software - Microsoft Research
Getting compilers right: a reliable foundation for secure software - Microsoft Research
Think compilers cannot compromise the security of your application? Think twice! Compiler writers work around the clock to deliver better compilers.
X / ?

Related Posts

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
Ferrocene
Part 1 - The Pitch