coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Call for Papers - Workshop on Instruction Set Architecture Specification

From: "Fernandez, Matthew" <matthew.fernandez AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Call for Papers - Workshop on Instruction Set Architecture Specification
Date: Sun, 2 Jun 2019 03:07:17 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=matthew.fernandez AT intel.com; spf=Pass smtp.mailfrom=matthew.fernandez AT intel.com; spf=None smtp.helo=postmaster AT mga06.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.600.7
Ironport-phdr: 9a23:ZpthYhGsaSEvpbDNR9Nvtp1GYnF86YWxBRYc798ds5kLTJ7zoMqwAkXT6L1XgUPTWs2DsrQY0rOQ6vu8EjJeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5vIBmssAncuMYbjYRjJ6sw1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK/qRJi347aboKbNPtica3SctwXXnZBXt9VWiBdHo+wc5UDAuwcNuhYtYn9oF4OoAOwCQesGuzv0DlIiWXw3aInzesgEBnK1xEnEd0UrHTUsNX1O7kcUOy70aLFyjDDYOlK2Tfh6IjHbB4greuCXb1ua8rRz1MgFwXYgVqOqI3oJDKV1uIRs2eF6+psT/6gi2kiqwxopDWk28kiio7Mho0Py1DE8z10z5gvKt2jSE90fd6kH4FRtyGALYd2RdkiQ25utS0nybMGoYa2cDUExZko3RLTdvKKfoeS7h7+WuucIC10iXx4dL6nmhq+7VKsxvPiWsWuzlpHriVInsPRun0D1BHf8tWLR/p580u7xzqC1w/e5vtZLUwoj6bWJJwsz7gtnZQJq0vDBDX5mEDuga+WaEok/u+o5vziYrXpvJCQK455hhv/MqQohsywH+A4PhISUGic/OSwzLzj/UvnT7VWlvA6j6fUvZ/AKcgGqKO0DBVZ3pst5hu+FTur3skUkWECLF1feRKHi4bpO0vJIPD9Ffq/hk6jkCt3x/DGILLgDI/BLnbdn7f7e7Zy8UhcxxctwtFe/J9UC7cBIO7tVU/1rtDXEhg5Mwmsz+b9FNp9zp8eWX6IAqKBLKzStkaI6vszLOmIeY8aoy3wK+Ml5v7rlX82g0URfaiv3ZsNaXC3BO5qI0uDYSmkvtBUW2wNp081SPHgoFyESz9aIXioFepo7TYiTYmiEI3rR4a3gbXH0j3tTbNMYWUTQH6BC3HhcYmJSbNETSuOPs9sjXZMAb2oV5Mh2A7ougLgzbNhIufG0iweqZ/nktNy4ruAxlkJ6TVoApHFgCm2RGZukzZQHmJk7OVEuUV4j2y7/+14jvhfTIMB4vxACll8NJjAwug8ANf3CFqYL4W5DW2+S9DjOgkfC9c4wtsAeUF4Qozwjxbf0i7sCLgQxeXSWM4Et5nE1n20HP5Tjm7c3fB43VggXsZLc2ahg/wn+g==

Dear colleagues,

The inaugural Workshop on Instruction Set Architecture Specification
(SpISA2019) will take place on September 13th, 2019 in Portland, Oregon,
USA. SpISA2019 will be collocated with the Tenth International
Conference on Interactive Theorem Proving (ITP2019).

Paper Submission
----------------
SpISA2019 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

Submissions will undergo single-blind peer review. They should be no
more than 4 pages in length including bibliographic references and are
to be submitted in PDF format via EasyChair via the following link:

https://easychair.org/conferences/?conf=spisa19

Important Dates
---------------
Paper submission: June 30, 2019
Author notification: July 25, 2019
Workshop: September 13, 2019

Contact
-------
Matthew Fernandez
<matthew.fernandez AT intel.com>
John Harrison
<jrh013 AT gmail.com>

[Coq-Club] Call for Papers - Workshop on Instruction Set Architecture Specification, Fernandez, Matthew, 06/02/2019