ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Thu 7 Sep 2023 11:00 - 11:30 at B - Fifth Avenue - Verification 2 Chair(s): Niki Vazou

Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use semantics in rather different ways. The best-known work applying single semantics across diverse tools relies on domain-specific languages like Sail, where the language and its translation tools are specialized to the realm of instruction sets. In the context of the open RISC-V instruction-set family, we decided to explore a different approach, with semantics written in a carefully chosen subset of Haskell. This style does not depend on any new language translators, relying instead on parameterization of semantics over type-class instances. We have used a single core semantics to support testing, interactive proof, and model checking of both software and hardware, demonstrating that monads and the ability to abstract over them using type classes can support pleasant prototyping of ISA semantics.

Thu 7 Sep

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
Verification 2ICFP Papers and Events at B - Fifth Avenue
Chair(s): Niki Vazou IMDEA Software Institute
10:30
30m
Talk
Explicit Refinement Types
ICFP Papers and Events
Jad Elkhaleq Ghalayini University of Cambridge, Neel Krishnaswami University of Cambridge
DOI
11:00
30m
Talk
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)Experience Report
ICFP Papers and Events
Thomas Bourgeat , Ian Clester Georgia Institute of Technology, Andres Erbsen MIT, Samuel Gruetter Massachusetts Institute of Technology, Pratap Singh CMU, Andy Wright MIT, Adam Chlipala Massachusetts Institute of Technology
DOI