Forget model checking - let’s prove ISA compliance!pic.twitter.com/OFcvk25Dbj
Prikaži ovu nit
Good morning @POPLconf! Excited for this morning’s invited talk at CPP:
Proof Assistants at the Hardware-Software Interface
By the great master, Adam Chlipala (MIT)
-
-
-
Don’t tell me you can’t formally verify IoT/embedded! This man did it on a university researcher’s budget What’s your excuse?pic.twitter.com/hQlb8XiNlK
Prikaži ovu nit -
RISC-V is looking good to be shipping billions of chips/year in the near term! Western Digital, NVIDIA, and others are already onboard Simple architecture, formally described, with vendors offering formally verified silicon Sorry dinosaurs, this asteroid is coming for you!pic.twitter.com/b6urVj2E1r
Prikaži ovu nit -
For example: Do you really think Intel/AMD/IBM are up to the task of fixing SPECTRE/MELTDOWN type bugs? Why would they be? They use pen, paper, and humans to keep track of these complex matters RISC-V has an actual formal model => can actually prove isolation!!!!!pic.twitter.com/2VDh1PYvMZ
Prikaži ovu nit -
Want tools? Surely they must be super expensive and inaccessible, right? WRONG Kami framework => open source! Bluespec => open source as of THIS MONTH!pic.twitter.com/3OPF2c3oUp
Prikaži ovu nit -
What can you do with this tech? How about a multi-core processor w/ cache hierarchy that’s been proven to faithfully implement the ISA? Yup! That’s a thingpic.twitter.com/odgEgVHKBC
Prikaži ovu nit -
... and yes, you can actually buy and use this stuff It’s happening yo. 2020 is the year! Formal methods NOW!pic.twitter.com/M0QQxrlxl1
Prikaži ovu nit -
Big shoutout to
@SiFive for their amazing industry/academic collaborations!
The work they’re doing to leverage these new advances and get them to market is truly inspiring 
The next gen of comp sci is looking 
!Prikaži ovu nit
Kraj razgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.