[TYPES/announce] Colocated with PLDI: Workshop on Deep Specifications in the Wild

[Adam Chlipala]

Those of you attending PLDI in Barcelona next week may be interested in 
also attending a workshop (on Thursday, after PLDI proper ends) run by 
our DeepSpec Project.

The workshop web site: http://pldi17.sigplan.org/track/dsw-2017-papers
The more general project web site: https://deepspec.org/

Briefly, our project is about scaling proof-assistant-based formal 
methods to more significant systems, especially through reuse of 
well-specified components.  A large element of the project is education 
and community-building, hence this workshop!

We have a speaker line-up that combines industry early-adopters of 
formal methods with some of our project leaders.  Full schedule 
information is on our workshop web site, but here is an overview.


    Invited Speakers from Industry

  * *Aleksey Nogin <https://nogin.org/>* from /HRL
    <http://www.hrl.com/>/, on integrating formal-methods tools in the
    DARPA HACMS program
    <http://www.darpa.mil/program/high-assurance-cyber-military-systems>
  * *Dominic Rizzo* from /Google
    <https://www.google.com/intl/en/about/>/, on applying proof
    assistants to cryptography at Google
  * *Michael Tautschnig <http://www.tautschnig.net/>* from /Amazon
    <https://aws.amazon.com/>/, on static analysis of hypervisor code


    Speakers From the DeepSpec Project

  * *Andrew W. Appel <https://www.cs.princeton.edu/%7Eappel/>* from
    /Princeton <https://www.cs.princeton.edu/>/, on verifying concurrent
    C programs with the Verified Software Toolchain
  * *Lennart Beringer <http://www.cs.princeton.edu/%7Eeberinge/>* from
    /Princeton <https://www.cs.princeton.edu/>/, on verifying
    cryptographic C code with the Verified Software Toolchain
  * *Adam Chlipala <http://adam.chlipala.net/>* from /MIT
    <https://www.csail.mit.edu>/, on generating low-level cryptographic
    code automatically from specifications
  * *Zhong Shao <http://www.cs.yale.edu/homes/shao/>* from /Yale
    <http://cpsc.yale.edu/>/, on verifying the CertiKOS hypervisor OS kernel

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20170615/9d697cd0/attachment.html>