coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Deadline extension - CFP 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] Deadline extension - CFP Workshop on Instruction Set Architecture Specification
Date: Fri, 28 Jun 2019 23:57:54 +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 mga07.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.600.7
Ironport-phdr: 9a23:6cIkjBXNGpIM+paFRz0d146+wyDV8LGtZVwlr6E/grcLSJyIuqrYbRWCt8tkgFKBZ4jH8fUM07OQ7/m6HzZZqszc+DBaKdoQDkZD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrsvxhfTvHdEZutayX1oKFmOmxrw+tq88IRs/ihNpv4t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+oPM/hFoYnhqVUArhq+ChWjCuzg0TJImmb20Kkm3+g9DQ3KwgotFM8OvnTOq9X1Mb8fXe61wqbW1zXDaelZ2THg54fWcxEtueyHU7VqfsrN1UkvFx3Kj1uepYf4OD6V0/4Cs3SH7+pgS+2uhXQrqw9vrTi1wMcjkI/JiZ8LxVHF7ih5wYA1JcGmR05/e9KrDJxQtySDOoZwX8gsTWZouCMgxb0Hv562ZDYFx448xx/fd/OHc5KH4hP5VOqLJjd4nn1ldbSijBix6Uit0vDwW8e73VpQsyZInNbBumoQ2xHd68WLUOZx8lu91TqXygzf9vtILV4qmabBNZIswrE9moAOvUnNHSL6gFj6ga6Se0k+5OSl6+vqbq/7qpOALYN4lAHzPrgol8eiG+o3KBIOUHKe+emk1L3s40n5QLJSg/0znanWqozWKMYBqq64BQ9Vzpgs6xKlAzi619QYmGELLFNDeB2Zk4jkI0zCLf73APulnlihnjhmy+rbMrDvA5jBNGXPnKv9cbpl7k5T0gszzdRR55JODbEBJer+Wkrru9zEEh85MxK7wuj9BNVzyIweQ2SPDbWfMKzPr1CJ5/kiI+iKZI8Jpjn9L+Ip6OLpjX88gVMdZ7Wm3YMLaHCkGfRrO1mWYX31gtsYDWgKuhc+Q/fxhV2ZUT9TYm6yULgm6jE6DoKmF4bDSZq3jLyPxifoVqFRMypNDUnJGnP1fa2FXe0NYWScOIUpxjcDTP2qT5Ir/RCorg7zjbR9eLn64Cod4NjN2cJz7uvfmAN2vRl9E9id3n7HBzVxl38URzIpmq5yu0p0zFuOw4B5heBVEZpY4PYfAVRyDoLV0+EvU4O6YQnGZNrcEA/3EOXjOik4S5cK+/FLZk98H9u4iRWahnirBaMYk/qAA5lmq/uBjUi0HN50zjP97Idkj1QiRZIQZ2ipj/YgsQnVG4PN1U6ekvTyLPhO7Gv27G6GiFG2kgRASgcpCPfEW2wSYg3dqtGrvk4=

Dear colleagues,

As an extension to the previously posted CFP below, we will be accepting
submissions until July 7 2019.

----

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, final deadline: July 7, 2019
Author notification: July 31, 2019
Workshop: September 13, 2019

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

[Coq-Club] Deadline extension - CFP Workshop on Instruction Set Architecture Specification, Fernandez, Matthew, 06/29/2019