Gerwin Klein

proves stuff about seL4, systems code, programming languages, security. Classical logician. Chief Scientist & Co-Founder at Proofcraft. @[email protected]

[Gerwin Klein @lsf37]

It's official, two of my colleagues and I have founded a new company in software verification: Proofcraft!
https://t.co/fhj6HSqLOz

[Mike Hicks @michael_w_hicks]

Shout-out to seL4, this years software award winner. Still a leader on the power and possibility of proved correct software!

[Gerwin Klein @lsf37]

@ShriramKMurthi @TheOfficialACM @GernotHeiser @UNSW @htuch314 @Google @ETH_en @Qualcomm @DVC_Peradeniya @tobycmurray @UniMelb Thank you!

[Association for Computing Machinery @TheOfficialACM]

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: https://t.co/VtPDuYz1cc

[Association for Computing Machinery @TheOfficialACM]

@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;

[Toby Murray @tobycmurray]

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

[Gerwin Klein @lsf37]

JFlex 1.9.0 is out: https://t.co/nqDAqP3Nzj

A little faster, all known bugs fixed, better warnings and new features. Enjoy!

[Type Theory Forall @ttforall]

📢 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.

https://t.co/pftTSkM1Ki

Available at your favorite podcast manager

[Gerwin Klein @lsf37]

@pruvisto @TaliaRinger @larsr_h With that you can build base images that contain multiple sessions that will all be available in that image.

[Gerwin Klein @lsf37]

@pruvisto @TaliaRinger @larsr_h That’s not quite right. Sessions and images are separate things in Isabelle. An image is just a heap dump, a session is a logical unit. You can depend on multiple sessions, but there is one designated main parent session that corresponds to an image you want to build on.

[Gerwin Klein @lsf37]

@sproulM_ Just played around a bit asking it about seL4 and it’s just good enough to be slightly wrong. Bit scary tbh.

[Gerwin Klein @lsf37]

@sproulM_ Ah well, and there I thought AI might finally be useful for something.

[PULP Platform @pulp_platform]

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. https://t.co/NduAW0BBC4

[Robert Sison (@[email protected]) @robs_cse]

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)

[seL4 @seL4Foundation]

We're pleased to announce that all videos and presentation slides from the truly awesome #seL4 #Summit are now available to the community, see https://t.co/27t78Ca1AV

[Lawrence Paulson @LawrPaulson]

The Archive of Formal Proofs has now been updated for Isabelle 2022: https://t.co/7oYe2rQvme
3.6 million lines of proofs in 709 entries by 430 authors

[seL4 @seL4Foundation]

Pleased to see that our member @Google has announced KataOS, a #security-focused #OperatingSystem, leveraging #Rust & #seL4 microkernel https://t.co/F1YunS3wi5

[Gernot Heiser @GernotHeiser]

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

[seL4 @seL4Foundation]

Day 4 of the #seL4 #Summit is the Boot camp: learning to build and use CAmkES, TRENTOS, seL4 Core Platform

[seL4 @seL4Foundation]

The seL4 GitHub test suite explained by ⁦@lsf37⁩ #seL4 #Summit