[TYPES/announce] ANN: RISC-V Workshop (with talks involving formal methods)

[Rishiyur Nikhil]

The 8th Annual RISC-V Workshop will be held May 7-10 at Univeritat
Politecnica de Catalunya.  Registration info can be found at:

    https://riscv.org/workshops/

Of particular interest to the Types community are two tutorials on May 7:

- Formal Specification of the RISC-V ISA
    Speaker: Thomas Bourgeat, MIT
    Abstract: In this tutorial we will demonstrate several flavors of
    a formal specification of the RISC-V ISA, written in Haskell.  We
    will present the important part of the code, use it as a software
    simulator, automatically transform it into a coq specification
    (used to prove the correctness of a small imperative language),
    and automatically synthesize it to circuit (to model check against
    other designs).

    If time permits, we will show how the same code can be used to
    explore some non-determinism in the specification.

- Formal Specification of the RISC-V Weak Memory Model
    Speaker: Dan Lustig, NVidia

    The spec has been two axiomatic formalizations in Herd and Alloy,
    and a formal operation model in SAIL.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20180429/8799f870/attachment.html>