coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Tutorial on formal semantics of RISC-V instruction set
- Date: Thu, 19 Apr 2018 11:30:52 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
- Ironport-phdr: 9a23:C59OlBRJnwJSV1VhPZ6JDTpOPdpsv+yvbD5Q0YIujvd0So/mwa69bBGN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/n/XhMJtj6xVrhyuqBNjzIPPeo6ZKOBzc7nBcd4UR2dMWNtaWSxbAoO7aosCF/YMMvtCoIn4ulADsxu+BQ2tBOP30DBIgmX51rA93us7DA7JxgkgEM4VvXvIt9X6LqYSUeSvwKnNzDXDc+la1ing54jVax0sp+yHU7x3ccrU00YvFgXFg02TqYzjITyayvgNvmaa4udgT+6gl2knqwRprji1x8cskZXGhpwPxlDD7yV5z4A4LsC7Rk5jedOoDYVcuiKAO4Z4Xs8uWX9ktDwkxrEbpZK3ZDUGxIokyhLFZfGLb5KE7xb9WOqLPzt0mm9pdbSijBio60eg0PfzVsys3VZKsCVFlt7Mu2gK1xzO9siHRfx9/kan2TaAzgzT8f1ELloolaXBMZIu3qUwmYASsUTHBCP2nUT2jLOMeko65+eo9vzrYrTgppCCK495khzyProtl8ClD+k0LhICU3aB9eiiybHv4VX1QLBQgf03lqnZvoraJcMepqOhGQBaz5ws6xOjADq9zNsYhmMILFNBeB6diojpOk3OLOrmAviinlSgiC1ryOzePr39HpXNKWDOn6vmfbZk8kJT1A4zzc1E6J9PEbEAIPfzWlfru9DCDx85NRa0w+f9B9ln2IMeQzHHPqjMO6TL9FSM++gHIu+WZYZTtiyuBeIi4qvHgXY80XQdeaix1J8eICSxEv1jKG2SenPthpEEEHtMswYjGr+5wGaeWCJeMi7hF5k34Ss2Xdr/XNXzA7u1ibnE5x+VW5hfZ2RIEFeJSCq6fJ6NWvNKbSOOZMJtj25dDOTze8oazRir8TTC5f9/NOONp38Trpvi0J5w5vGVmB0vp2QtUpatllqVRmQxpVsmAj872Kck+R5610uM1ql+jLlDCdVP7rVCSQ47MdjZzvA8BtzvCFrM
|
The following tutorial, on a formal specification of the RISC-V open
instruction set, may be of interest to some Coq Clubbers.
(The larger event it is attached to may also be of interest!)
Title: RISC-V ISA Formal Specification
Speaker: Thomas Bourgeat, MIT
Venue: 8th RISC-V Workshop, Barcelona, Spain
Date: 4:50pm to 5:25pm, Monday, May 7, 2018
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 a circuit (to
model-check against
other designs).
If time permits, we will show how the same code can be used
to
explore some nondeterminism in the specification.
Registration info: https://riscv.org/workshops/
Workshop agenda: https://tmt.knect365.com/risc-v-workshop-barcelona/agenda/1
|
- [Coq-Club] Tutorial on formal semantics of RISC-V instruction set, Adam Chlipala, 04/19/2018
Archive powered by MHonArc 2.6.18.