Loading…
Back To Schedule
Tuesday, September 15 • 12:45pm - 1:15pm
Towards a Formally-verified Software Toolchain for open ISAs - Boris Shingarov, LabWare

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Feedback form is now closed.

This talk summarizes lessons from several years of experimenting with automatic generation of compiler toolchains from processor description languages (PDL), using approaches ranging from superoptimization via logic programming to SMT-based binary analysis, and presents a new experimental system which builds on these lessons. The new approach takes ISA specifications written in the Sail PDL, as the starting point for software-tools synthesis and verification. Sail is used by practicing engineers to create full-scale formalizations of real ISAs; on the other hand, Sail is based on Lem and is mathematically rigorous. This talk demonstrates how the tool transforms a short sequence of POWER instructions into a proof of an invariant of the final state holding universally over the space of allowed behaviors.

Continue the conversation in Slack

Speakers
avatar for Boris Shingarov

Boris Shingarov

Open-source VM designer, LabWare
Boris Shingarov designs open-source dynamic language VMs at LabWare. Currently Boris works on formal proof of correctness of JIT compilers, particularly for open-source ISAs. In the past, Boris has contributed to the creation of large-scale open-source software ecosystems through... Read More →


Tuesday September 15, 2020 12:45pm - 1:15pm CDT
Track 1