SpISA 2019: Workshop on Instruction Set Architecture Specification
September 13 - Portland, OR, USA
13th September 2019 at Portland State
University, Portland OR, USA, as part of
ITP 2019.
The SpISA 2019 workshop is devoted to the specification of instruction set
architectures in a formal setting, and to the formal proofs of code
correctness and other properties with respect to such specifications. We
welcome contributions from academia and industry. Topics of interest
include:
- Specifications of traditional machine architectures (ARM, MIPS,
PowerPC, RISC-V, x86, ...)
- Specifications of virtual machines (JVM, LLVM, Webasm, ...)
- Domain-specific languages for specifying ISAs
- ISA semantics in interactive theorem provers
- Proof methodologies (symbolic simulation, interactive proof, ...)
- Formal applications of instruction set simulators
- Compiler correctness with respect to formal ISA specifications
Important Dates
- Workshop: September 13, 2019
Program
- Session I
- 09:00 - 09:30 Invited talk: x86: mid-life crisis?
Ronak Singhal
- 09:30 - 09:55 Instruction Set Architecture Specification,
Verification, and Validation using Algorithmic C and ACL2
David Hardin
(paper,
slides)
- 09:55 - 10:25 Break
- Session II
- 10:25 - 10:50 Symbolic Execution of x86 assembly in Isabelle/HOL
Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Binoy Ravindran
(paper,
slides)
- 10:50 - 11:15 Formalizing x86-64 Instruction Decoder in K
Sandeep Dasgupta, Andrew H. Miranti, Grigore Rosu
(paper,
slides)
- 11:15 - 11:40 Specifying verified x86 software from scratch
Mario Carneiro
(paper,
slides)
- 11:40 - 12:05 Using x86isa for Microcode Verification
Shilpi Goel, Rob Sumners
(paper,
slides)
- 12:05 - 12:30 GRIFT: A richly-typed, deeply-embedded RISC-V semantics
written in Haskell
Benjamin Selfridge
(paper,
slides)
- 12:30 - 14:00 Lunch
- Session III
- 14:00 - 14:25 The State of Sail
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, Peter Sewell
(paper,
slides)
- 14:25 - 15:30 Panel discussion
Alasdair Armstrong, Shilpi Goel, Joe Hendrix, Ronak Singhal
- 15:30 - 16:00 Break
- Session IV
- 16:00 - 16:25 Formal Verification of Floating-Point RTL with ACL2
David Russinoff
(paper,
slides)
- 16:25 - 16:50 Quameleon: A Lifter and Intermediate Language for
Binary Analysis
Samuel Pollard, Philip Johnson-Freyd, Jon Aytac, Tristan Duckworth, Michael Carson, Geoffrey Hulette, Christopher Harrison
(paper,
slides)
- 16:50 - 17:15 Towards Verified Binary Raising
Joe Hendrix, Guannan Wei, Simon Winwood
(paper)
Program committee
- Sandrine Blazy (Irisa)
- Joey Dodds (Galois)
- Matthew Fernandez (Intel, chair)
- Shilpi Goel (U. Texas)
- John Harrison (Amazon Web Services)
- Magnus Myreen (Chalmers)
- Rishiyur Nikhil (Bluespec)
- Grigore Rosu (U. Illinois))
- David Russinoff (ARM)
- Konrad Slind (Rockwell Collins)
Page last updated .