caml-list - the Caml user's mailing list
 help / Atom feed
From: David Nowak <>
To:,,, "" <types-announce@LISTS.SEAS.UPENN.EDU>,,,,,,
Subject: [Caml-list] ENTROPY 2019: Second Call for Papers - Co-located with EuroS&P'19
Date: Tue, 19 Feb 2019 18:10:40 +0100
Message-ID: <> (raw)

NEW: two more invited speakers

            Second Call for papers — ENTROPY 2019
        ENabling TRust through Os Proofs … and beYond

Second International workshop on the use of theorem provers for modelling 
and verification at the hardware-software interface 


Co-located with EuroS&P'19, KTH, Stockholm, June 2019


Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge


Paper submission: March 11 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019


Low level software such as kernels and drivers, along with the hardware 
this software runs on, is critical for application security. In contrast 
with user applications, OS kernel software runs in privileged CPU mode 
and is thus highly critical. Large projects such as seL4, VeriSoft, 
CertiKoS and Prosper have invested considerable resources in developing 
formally verified systems such as hypervisors and microkernels, supplying 
proofs that they satisfy critical properties. Such proofs are delicate in 
terms of the scale and complexity of real systems, the models used in 
performing the proof search, and the relations between the two, which 
recent vulnerabilities such as Spectre and Meltdown have shown to be a 
highly non-trivial issue.

The purpose of this workshop is to share, compare and disseminate best 
practices, tools and methodologies to verify OS kernels, also setting the 
stage for future steps in the direction of fully verified systems, 
dealing with issues related to modelling, model validation, and large 
proof maintenance through system evolution. On one hand, we need to make 
low-level proofs more scalable, modular and cost-effective. On the other 
hand, once certified systems are available, preservation and maintenance 
of their proofs of validity become key questions.

The goal of the ENTROPY workshop is to provide a forum for researchers 
and practitioners in this space, linking operating systems, formal 
methods, and hardware architecture, interested in system design as well 
as machine verified mathematical proofs using proof assistants such as 
Coq, Isabelle and HOL4.

This will be the second edition of the ENTROPY workshop series. The 
first workshop was organised by the Pip Development Team at University 
of Lille in 2018.


Specific topics include, but are not limited to:

* Verified kernels and hypervisors
* Verified security architectures and models
* Tools and frameworks for hardware security analysis
* Tools and frameworks for security analysis
* Formal hardware models and model validation techniques
* Theorem prover based tools and frameworks for verification of low level code
* Combinations of static analysis and theorem proving
* Theories and techniques for compositional security analysis
* Case studies and industrial experience reports
* Proof maintenance techniques and problems
* Compositional models and verification techniques
* Proof oriented design

The aim of the workshop is to stimulate innovation and active exchange 
of ideas, so position papers, work-in-progress and industrial 
experience submissions are welcome.


There are two categories of submissions:

1. Regular papers describing fully developed work and complete results 
(10 pages, references included, IEEE format)
2. Short papers, position papers, industry experience reports,
work-in-progress submissions (4 pages, references included, IEEE 

All papers should be in English and describe original work that has not 
been published or submitted elsewhere. The submission category should 
be clearly indicated. All submissions will be fully reviewed by members 
of the Programme Committee. Papers will appear in IEEE Xplore in a 
companion volume to the regular EuroS&P proceedings. For formatting and 
submission instructions see


Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille


Christoph Baumann, Ericsson AB
Gustavo Betarte, Univ. de la República, Uruguay
David Cock, ETH Zurich
Mads Dam, KTH Royal Institute of Technology (chair)
Anthony Fox, ARM
Deepak Garg, MPI Saarbrucken
Ronghui Gu, Columbia University
Samuel Hym, Univ. Lille
Thomas Jensen, INRIA and Univ. Rennes
Toby Murray, Univ. Melbourne
David Nowak, CNRS & Univ. Lille (chair)
Vicente Sanchez-Leighton, Orange Labs
Thomas Sewell, Chalmers

David Nowak

             reply index

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-02-19 17:10 David Nowak [this message]
2019-03-11 20:24 ` [Caml-list] ENTROPY 2019: Deadline Extension -- Final Call for Papers David Nowak

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \ \ \ \ \ \ \ \ \ \ \ \
    --cc=types-announce@LISTS.SEAS.UPENN.EDU \

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror

AGPL code for this site: git clone public-inbox