Pinned Tweet
It's official, two of my colleagues and I have founded a new company in software verification: Proofcraft!
proofcraft.systems
Gerwin Klein retweeted
Shout-out to seL4, this years software award winner. Still a leader on the power and possibility of proved correct software!
Gerwin Klein retweeted
Michael Norrish, @ANUmedia; Thomas Sewell, @Cambridge_Uni; Simon Winwood, @galois , receive the 2022 ACM Software System Award! Learn more about their award-winning research here: awards.acm.org/software-syst…
Gerwin Klein retweeted
@GernotHeiser , @UNSW; Gerwin Klein, Proofcraft; @htuch314 , @Google; Kevin Elphinstone, @UNSW; June Andronick, Proofcraft; David Cock, @ETH_en; Philip Derrin, @Qualcomm; Dhammika Elkaduwe, @DVC_Peradeniya; Kai Engelhardt; @tobycmurray , @UniMelb; Rafal Kolanski, Proofcraft;
Gerwin Klein retweeted
If you’re curious about formal methods & #seL4, this episode is a wonderful deep dive cum oral history. On a personal level it reminded me how much I miss working alongside @lsf37 every day, without whose mentorship I’d surely not have ended up in academia. Viva verified software
📢 One more episode is out! This time we talk with @lsf37 about the formally verified seL4 microkernel using Isabelle! We also talk about his PhD thesis on formally verifying a piece of the Java Virtual Machine.
typetheoryforall.com/2023/02…
Available at your favorite podcast manager
JFlex 1.9.0 is out: jflex.de
A little faster, all known bugs fixed, better warnings and new features. Enjoy!
Gerwin Klein retweeted
📢 One more episode is out! This time we talk with @lsf37 about the formally verified seL4 microkernel using Isabelle! We also talk about his PhD thesis on formally verifying a piece of the Java Virtual Machine.
typetheoryforall.com/2023/02…
Available at your favorite podcast manager
Gerwin Klein retweeted
The videos from the seL4 Summit 2022 @seL4Foundation are now online😀. Check out Nils's @niwist talk on fence.t, a novel RISC-V instruction that clears the processor's microarchitectural state and thus any timing dependence on execution history. youtube.com/watch?v=tLcum9Yk…
Gerwin Klein retweeted
Some good news: We've had a paper accepted to FM'23 on our formalisation of the prevention of microarchitectural timing channels by operating systems
(Joint work between @cis_unimelb, @UNSWCOMPUTING and Proofcraft w/ coauthors @buckdotly, @tobycmurray, @lsf37 and @GernotHeiser)
Ongoing work is with @tobycmurray (@cis_unimelb) collaborating with Scott Buckley, @GernotHeiser (@UNSWCOMPUTING), and @lsf37 (Proofcraft).
Relevant prior publications:
🔖 Heiser et al '20 doi.org/10.1145/3421473.3421… '19 doi.org/10.1145/3317550.3321…
🔖 Ge et al '19 doi.org/10.1145/3302424.3303…
Gerwin Klein retweeted
We're pleased to announce that all videos and presentation slides from the truly awesome #seL4 #Summit are now available to the community, see sel4.systems/news/2022#summi…
Gerwin Klein retweeted
The Archive of Formal Proofs has now been updated for Isabelle 2022: isa-afp.org
3.6 million lines of proofs in 709 entries by 430 authors
Gerwin Klein retweeted
Pleased to see that our member @Google has announced KataOS, a #security-focused #OperatingSystem, leveraging #Rust & #seL4 microkernel phoronix.com/news/Google-Kat…
Gerwin Klein retweeted
The #seL4 #Summit is over. It was an awesome event. And it was fantastic to once again work closely with the incredible June Andronick, like in the old days. Thanks all who participated! @seL4Foundation
