# CALL FOR PAPERS
21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019)
https://conf.researchr.org/home/FTfJP-2019/
Co-located with ECOOP 2019, July 15-19, Hammersmith, London
## About FTfJP 2019
Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.
Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.
The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term "Java-like" is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.
Example topics of interest include:
* Language design and semantics
* Type systems
* Concurrency and new application domains
* Specification and verification of program properties
* Program analysis (static or dynamic)
* Program Synthesis
* Security
* Pearls (programs or proofs)
FTfJP welcomes submissions on technical contributions, case studies,
experience reports, challenge proposals, and position papers.
## Submissions
Contributions are sought in two categories:
* Full Papers (6 pages, excluding references) present a technical
contribution, case study, or detailed experience report. We welcome
both complete and incomplete technical results; ongoing work is
particularly welcome, provided it is substantial enough to stimulate
interesting discussions.
* Short Papers (2 pages, excluding references) should advocate a
promising research direction, or otherwise present a position likely
to stimulate discussion at the workshop. We encourage
e.g. established researchers to set out a personal vision, and
beginning researchers to present a planned path to a PhD.
Both types of contributions will benefit from feedback received at the
workshop. Submissions will be peer reviewed, and will be evaluated
based on their clarity and their potential to generate interesting
discussions. The format of the workshop encourages interaction. FTfJP
is a forum in which a wide range of people share their expertise, from
experienced researchers to beginning PhD students.
## Formatting and Publication
Submissions should be in acmart/sigplan style, 10pt font. Formatting
requirements are detailed on the SIGPLAN Author Information page
(https://www.sigplan.org/Resources/Author).
Accepted papers will be published in the ACM Digital Library by
default, though authors will be able to opt out of this publication,
if desired. At least one author of an accepted paper must attend the
workshop to present the work and participate in the discussions.
## Important Dates
* Submission: 21 April (AoE)
* Notification: 2 June
## Program Committee
* Yuyan Bao (Pennsylvania State University)
* James Bornholt (University of Washington)
* Gidon Ernst (Co-Chair; LMU Munich)
* Marie Farrell (University of Liverpool)
* Carlo A. Furia (USI – Università della Svizzera Italiana)
* Marie-Christine Jakobs (TU Darmstadt)
* Wojciech Mostowski (Halmstad University)
* Toby Murray (Co-Chair; University of Melbourne)
* Christine Rizkallah (University of New South Wales and Data61)
* Martin Schäf (Amazon Web Services)
2019-03-11
[Caml-list] ENTROPY 2019: Deadline Extension -- Final Call for Papers
The deadline for ENTROPY 2019 is extended to March 15, 2019.
You can submit via our Easychair website:
https://easychair.org/conferences/?conf=entropy2019
Questions can be directed to:
entropy2019@sciencesconf.org
**************************************************************************
Final 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
https://entropy2019.sciencesconf.org
Co-located with EuroS&P'19, KTH, Stockholm, June 2019
**************************************************************************
INVITED SPEAKERS
Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge
IMPORTANT DATES
Paper submission: March 15, 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019
AIM AND SCOPE
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.
TOPICS OF INTEREST
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.
SUBMISSION AND PUBLICATION
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
format)
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 https://entropy2019.sciencesconf.org.
PROGRAM CHAIRS
Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille
PROGRAM COMMITTEE
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
http://www.cristal.univ-lille.fr/~nowakd/
You can submit via our Easychair website:
https://easychair.org/conferences/?conf=entropy2019
Questions can be directed to:
entropy2019@sciencesconf.org
**************************************************************************
Final 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
https://entropy2019.sciencesconf.org
Co-located with EuroS&P'19, KTH, Stockholm, June 2019
**************************************************************************
INVITED SPEAKERS
Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge
IMPORTANT DATES
Paper submission: March 15, 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019
AIM AND SCOPE
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.
TOPICS OF INTEREST
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.
SUBMISSION AND PUBLICATION
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
format)
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 https://entropy2019.sciencesconf.org.
PROGRAM CHAIRS
Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille
PROGRAM COMMITTEE
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
http://www.cristal.univ-lille.fr/~nowakd/
2019-03-07
[Caml-list] Second Dali Workshop: First Call for Papers
Dynamic Logic: New Trends and Applications
workshop.dali.di.uminho.pt
First Call for Papers
Porto, 9 October, 2019
(part of the 3rd World Congress on Formal Methods 2019)
OVERVIEW
Building on the pioneer intuitions of Floyd-Hoare logic, dynamic logic
was introduced in the 70's as a suitable logic to reason about, and
verify, classic imperative programs. Since then, the original
intuitions grew to an entire family of logics, which became
increasingly popular for assertional reasoning about a wide range of
computational systems. Simultaneously, their object (i.e. the very
notion of a program) evolved in unexpected ways. This lead to dynamic
logics tailored to specific programming paradigms and extended to new
computing domains, including probabilistic, continuous and quantum
computation. Both its theoretical relevance and practical potential
make dynamic logic a topic of interest in a number of scientific
venues, from wide-scope software engineering conferences to modal
logic specific events. However, no specific event is exclusively
dedicated to it. This workshop aims at filling fill such a gap,
joining an heterogeneous community of colleagues, from Academia to
Industry, from Mathematics to Computer Science.
Support: PT-FLAD Chair & DaLi - POCI-01-0145-FEDER-016692
TOPICS
Submissions are invited on the general field of dynamic logic, its
variants and applications, including, but not restricted to
Dynamic logic, foundations and applications
Logics with regular modalities
Modal/temporal/epistemic logics
Kleene and action algebras and their variants
Quantum dynamic logic
Coalgebraic modal/dynamic logics
Graded and fuzzy dynamic logics
Dynamic logics for cyber-physical systems
Dynamic epistemic logic
Complexity and decidability of variants of dynamic logics
and temporal logics
Model checking, model generation and theorem proving for
dynamic logics
SUBMISSION AND PUBLICATION
Original papers (unpublished and not submitted for publication
elsewhere), up to 15 pages in LNCS style. As in the previous edition,
post-proceedings will be published by Springer in a Lecture Notes of
Computer Science volume, and a special issue with extended, revised
contributions is planed.
Submit via the EasyChair link https://easychair.org/conferences/?conf=dali2019
INVITED SPEAKER
Dexter Kozen, Cornell University
IMPORTANT DATES
Paper Submission: June 14, 2019
Notification: July 19, 2019
Camera Ready: September 2, 2019
Workshop: October 9, 2019
PROGRAMME COMMITTEE
Guillaume Aucher (IRISA, FR)
Carlos Areces (U Cordoba, AR)
Alexandru Baltag, (UvA, NL) - PC co-chair
Luis S. Barbosa, (U Minho, PT) - PC co-chair
Mario Benevides (UFRJ, BR)
Johan van Benthem (U Stanford, USA)
Patrick Blackburn, (U Roskilde, DK)
Thomas Bolander (DTU, Denmark)
Zoe Christoff (U Bayreuth, Germany)
Fredrik Dahlqvist (UCL, UK)
Hans van Ditmarsch (LORIA, Nancy, FR)
Nina Gierasimczuk (DTU, Denmark)
Valentin Goranko (U Stockholm, SE)
Davide Grossi (U Groningen, NL)
Reiner Hahle (TU Darmstadt, DE)
Rolf Hennicker (LMU, Munchen, DE)
Andreas Herzig (U Toulouse, FR)
Dexter Kozen (Cornell, USA)
Clemens Kupke (U Strathclyde, UK)
Alexandre Madeira (U Aveiro, PT)
Manuel A. Martins (U Aveiro, PT)
Paulo Mateus (IST, PT)
Stefan Mitsch (CMU, USA)
Renato Neves (U Minho, PT)
Valeria de Paiva (Nuance Comms, USA)
Aybuke Ozgun (ILLC, NL)
Fernando Velazquez-Quesada (ILLC, NL)
Olivier Roy (U Bayreuth, DE)
Lutz Schroeder (FAU, Erlangen-Nurenberg, DE)
Alexandra Silva (UCL, UK)
Sonja Smets (UvA, NL)
Rui Soares Barbosa (U Oxford, UK)
Tinko Tinchev (Sofia U, BG)
Renata Wassermann (USP, BR)
workshop.dali.di.uminho.pt
First Call for Papers
Porto, 9 October, 2019
(part of the 3rd World Congress on Formal Methods 2019)
OVERVIEW
Building on the pioneer intuitions of Floyd-Hoare logic, dynamic logic
was introduced in the 70's as a suitable logic to reason about, and
verify, classic imperative programs. Since then, the original
intuitions grew to an entire family of logics, which became
increasingly popular for assertional reasoning about a wide range of
computational systems. Simultaneously, their object (i.e. the very
notion of a program) evolved in unexpected ways. This lead to dynamic
logics tailored to specific programming paradigms and extended to new
computing domains, including probabilistic, continuous and quantum
computation. Both its theoretical relevance and practical potential
make dynamic logic a topic of interest in a number of scientific
venues, from wide-scope software engineering conferences to modal
logic specific events. However, no specific event is exclusively
dedicated to it. This workshop aims at filling fill such a gap,
joining an heterogeneous community of colleagues, from Academia to
Industry, from Mathematics to Computer Science.
Support: PT-FLAD Chair & DaLi - POCI-01-0145-FEDER-016692
TOPICS
Submissions are invited on the general field of dynamic logic, its
variants and applications, including, but not restricted to
Dynamic logic, foundations and applications
Logics with regular modalities
Modal/temporal/epistemic logics
Kleene and action algebras and their variants
Quantum dynamic logic
Coalgebraic modal/dynamic logics
Graded and fuzzy dynamic logics
Dynamic logics for cyber-physical systems
Dynamic epistemic logic
Complexity and decidability of variants of dynamic logics
and temporal logics
Model checking, model generation and theorem proving for
dynamic logics
SUBMISSION AND PUBLICATION
Original papers (unpublished and not submitted for publication
elsewhere), up to 15 pages in LNCS style. As in the previous edition,
post-proceedings will be published by Springer in a Lecture Notes of
Computer Science volume, and a special issue with extended, revised
contributions is planed.
Submit via the EasyChair link https://easychair.org/conferences/?conf=dali2019
INVITED SPEAKER
Dexter Kozen, Cornell University
IMPORTANT DATES
Paper Submission: June 14, 2019
Notification: July 19, 2019
Camera Ready: September 2, 2019
Workshop: October 9, 2019
PROGRAMME COMMITTEE
Guillaume Aucher (IRISA, FR)
Carlos Areces (U Cordoba, AR)
Alexandru Baltag, (UvA, NL) - PC co-chair
Luis S. Barbosa, (U Minho, PT) - PC co-chair
Mario Benevides (UFRJ, BR)
Johan van Benthem (U Stanford, USA)
Patrick Blackburn, (U Roskilde, DK)
Thomas Bolander (DTU, Denmark)
Zoe Christoff (U Bayreuth, Germany)
Fredrik Dahlqvist (UCL, UK)
Hans van Ditmarsch (LORIA, Nancy, FR)
Nina Gierasimczuk (DTU, Denmark)
Valentin Goranko (U Stockholm, SE)
Davide Grossi (U Groningen, NL)
Reiner Hahle (TU Darmstadt, DE)
Rolf Hennicker (LMU, Munchen, DE)
Andreas Herzig (U Toulouse, FR)
Dexter Kozen (Cornell, USA)
Clemens Kupke (U Strathclyde, UK)
Alexandre Madeira (U Aveiro, PT)
Manuel A. Martins (U Aveiro, PT)
Paulo Mateus (IST, PT)
Stefan Mitsch (CMU, USA)
Renato Neves (U Minho, PT)
Valeria de Paiva (Nuance Comms, USA)
Aybuke Ozgun (ILLC, NL)
Fernando Velazquez-Quesada (ILLC, NL)
Olivier Roy (U Bayreuth, DE)
Lutz Schroeder (FAU, Erlangen-Nurenberg, DE)
Alexandra Silva (UCL, UK)
Sonja Smets (UvA, NL)
Rui Soares Barbosa (U Oxford, UK)
Tinko Tinchev (Sofia U, BG)
Renata Wassermann (USP, BR)
2019-02-25
[Caml-list] VerifyThis @ ETAPS 2019: Travel Grants + Call for Participation
********************************************************************************
VerifyThis Verification Competition 2019
CALL FOR PARTICIPATION -- TRAVEL GRANTS
Competition to be held at ETAPS 2019
http://verifythis.ethz.ch
********************************************************************************
IMPORTANT DATES
Grant application deadline: March 7, 2019
Competition: April 6 and 7, 2019
ABOUT
VerifyThis 2019 is a program verification competition taking place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019) on April 6-7, 2019 in Prague, Czech Republic.
It is the 8th event in the VerifyThis competition series.
The competition will offer a number of challenges presented in natural language and pseudo code.
Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used.
The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
PARTICIPATION
Participation is open for anybody interested.
Teams of up to two people are allowed.
Registration for ETAPS workshops and physical presence on site is required.
We particularly encourage participation of:
- student teams (this includes PhD students)
- non-developer teams using a tool someone else developed
- several teams using the same tool
TRAVEL GRANTS
The competition has funds for a limited number of travel grants.
A grant covers the incurred travel and accommodation costs up to a certain limit.
The expected limit is EUR 350 for those coming from Europe and EUR 600 for those coming from outside Europe.
To apply for a travel grant, send an email to verifythis@cs.nuim.ie by March 7, 2019. The application should include:
- your name
- your affiliation
- the verification system(s) you plan to use at the competition
- the planned composition of your team (and whether you are developers of the tools you'll be using)
- a short letter of motivation explaining your involvement with formal verification so far
- if you are a student, please state the academic degree you are seeking and have your supervisor send a brief letter of support to verifythis@cs.nuim.ie
ORGANIZERS
* Marieke Huisman, University of Twente, the Netherlands
* Rosemary Monahan, Maynooth University, Ireland
* Peter Müller, ETH Zürich, Switzerland
* Claire Dross, Adacore, France
* Carlo A. Furia, USI Lugano, Switzerland
CONTACT
Email: verifythis@cs.nuim.ie
Web: http://verifythis.ethz.ch
VerifyThis Verification Competition 2019
CALL FOR PARTICIPATION -- TRAVEL GRANTS
Competition to be held at ETAPS 2019
http://verifythis.ethz.ch
********************************************************************************
IMPORTANT DATES
Grant application deadline: March 7, 2019
Competition: April 6 and 7, 2019
ABOUT
VerifyThis 2019 is a program verification competition taking place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019) on April 6-7, 2019 in Prague, Czech Republic.
It is the 8th event in the VerifyThis competition series.
The competition will offer a number of challenges presented in natural language and pseudo code.
Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used.
The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
PARTICIPATION
Participation is open for anybody interested.
Teams of up to two people are allowed.
Registration for ETAPS workshops and physical presence on site is required.
We particularly encourage participation of:
- student teams (this includes PhD students)
- non-developer teams using a tool someone else developed
- several teams using the same tool
TRAVEL GRANTS
The competition has funds for a limited number of travel grants.
A grant covers the incurred travel and accommodation costs up to a certain limit.
The expected limit is EUR 350 for those coming from Europe and EUR 600 for those coming from outside Europe.
To apply for a travel grant, send an email to verifythis@cs.nuim.ie by March 7, 2019. The application should include:
- your name
- your affiliation
- the verification system(s) you plan to use at the competition
- the planned composition of your team (and whether you are developers of the tools you'll be using)
- a short letter of motivation explaining your involvement with formal verification so far
- if you are a student, please state the academic degree you are seeking and have your supervisor send a brief letter of support to verifythis@cs.nuim.ie
ORGANIZERS
* Marieke Huisman, University of Twente, the Netherlands
* Rosemary Monahan, Maynooth University, Ireland
* Peter Müller, ETH Zürich, Switzerland
* Claire Dross, Adacore, France
* Carlo A. Furia, USI Lugano, Switzerland
CONTACT
Email: verifythis@cs.nuim.ie
Web: http://verifythis.ethz.ch
2019-02-19
[Caml-list] ENTROPY 2019: Second Call for Papers - Co-located with EuroS&P'19
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
https://entropy2019.sciencesconf.org
Co-located with EuroS&P'19, KTH, Stockholm, June 2019
**************************************************************************
INVITED SPEAKERS
Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge
IMPORTANT DATES
Paper submission: March 11 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019
AIM AND SCOPE
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.
TOPICS OF INTEREST
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.
SUBMISSION AND PUBLICATION
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
format)
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 https://entropy2019.sciencesconf.org.
PROGRAM CHAIRS
Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille
PROGRAM COMMITTEE
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
http://www.cristal.univ-lille.fr/~nowakd/
**************************************************************************
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
https://entropy2019.sciencesconf.org
Co-located with EuroS&P'19, KTH, Stockholm, June 2019
**************************************************************************
INVITED SPEAKERS
Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge
IMPORTANT DATES
Paper submission: March 11 2019
Author notification: April 10, 2019
Camera-ready versions: April 22, 2019 (strict)
Workshop: 16 June 2019
AIM AND SCOPE
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.
TOPICS OF INTEREST
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.
SUBMISSION AND PUBLICATION
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
format)
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 https://entropy2019.sciencesconf.org.
PROGRAM CHAIRS
Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille
PROGRAM COMMITTEE
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
http://www.cristal.univ-lille.fr/~nowakd/
[Caml-list] ETAPS 2019 call for participation
******************************************************************
CALL FOR PARTICIPATION
22nd European Joint Conferences on Theory And Practice of Software
ETAPS 2019
Prague, Czech Republic, 6-11 April 2019
http://www.etaps.org/2019
https://conf.researchr.org/home/etaps-2019
******************************************************************
-- ABOUT ETAPS --
ETAPS is the primary European forum for academic and industrial
researchers working on topics relating to software science. ETAPS,
established in 1998, is a confederation of five main annual
conferences, accompanied by satellite workshops. ETAPS 2019 is the
twenty-second event in the series.
-- MAIN CONFERENCES (8-11 April) --
* ESOP: European Symposium on Programming
(PC chair Luís Caires, Universidade Nova de Lisboa, Portugal)
* FASE: Fundamental Approaches to Software Engineering
(PC chairs Reiner Hähnle, Technische Univ Darmstadt, Germany,
and Wil van der Aalst, RWTH Aachen University, Germany)
* FoSSaCS: Foundations of Software Science
and Computation Structures
(PC chairs Mikolaj Bojanczyk, University of Warsaw, Poland,
and Alex Simpson, University of Ljubljana, Slovenia)
* POST: Principles of Security and Trust
(PC chairs Flemming Nielson, Danmarks Tekniske Univ, Denmark,
and David Sands, Chalmers Tekniska Högskola, Sweden)
* TACAS: Tools and Algorithms for
the Construction and Analysis of Systems
(PC chairs Tomás Vojnar, Brno Univ of Technology, Czech Rep,
and Lijun Zhang, Chinese Academy of Sciences, China)
TACAS '19 hosts the 8th Competition on Software Verification (SV-COMP)
and TOOLympics, an event to celebrate the achievements of the various
competitions or comparative evaluations.
-- INVITED TALKS AND TUTORIALS --
* Unifying speakers:
Marscha Chechik (University of Toronto, Canada)
Kathleen Fisher (Tufts University, USA)
* FoSSaCS invited speaker:
Thomas Colcombet (IRIF, France)
* TACAS invited speaker:
Cormac Flanagan (University of California at Santa Cruz, USA)
* Tutorial speakers:
Dirk Beyer (LMU München, Germany)
Cesare Tinelli (University of Iowa, USA)
-- CONTRIBUTED PAPERS --
See the accepted paper lists at webpages of the individual
conferences.
For the 2nd year, the proceedings of the ETAPS main conferences in
LNCS/ARCoSS will appear in Gold Open Access.
-- PROGRAM --
See the full program here:
https://conf.researchr.org/program/etaps-2019/program-etaps-2019
-- SATELLITE EVENTS (6-7 April) --
18 satellite workshops and other events will take place before
ETAPS 2019.
DICE-FOPARA, GaLoP, HSB, QAPL, SynCoP, VerifyThis,
TOOLympics (6-7 April)
BEHAPI, InterAVT, LiVe, MeTRiD, PERR (6 April)
CREST, HCVS, PLACES, SPIoT, SYNTCOMP Camp,
Mentoring Workshop (7 April)
-- REGISTRATION --
Early registration is until Sunday, 11 March 2019,
https://regmaster4.com/2019conf/ETAPS19/register.php
-- HOST CITY AND VENUE --
ETAPS 2019 will take place in the centre of Prague, the beautiful
capital of the Czech Republic.
The main conferences will be held at Orea Hotel Pyramida, while the
workshops will take place at the School of Computer Science, Faculty of
Mathematics and Physics, Charles University. Both are close to the
Prague Castle.
For the special deal for accommodation at the conference hotel, see
the conference website.
-- HOST INSTITUTION --
ETAPS 2019 is hosted by the School of Computer Science of the Charles
University.
-- ORGANIZERS
Jan Kofron and Jan Vitek (general chairs), Barbora Buhnova, Milan
Ceska, Ryan Culpepper, Vojtech Horky, Paley Li, Petr Maj, Artem
Pelenitsyn, David Safranek
-- FURTHER INFORMATION --
Please do not hesitate to contact the organizers at
jan.kofron@d3s.mff.cuni.cz and j.vitek@neu.edu.
CALL FOR PARTICIPATION
22nd European Joint Conferences on Theory And Practice of Software
ETAPS 2019
Prague, Czech Republic, 6-11 April 2019
http://www.etaps.org/2019
https://conf.researchr.org/home/etaps-2019
******************************************************************
-- ABOUT ETAPS --
ETAPS is the primary European forum for academic and industrial
researchers working on topics relating to software science. ETAPS,
established in 1998, is a confederation of five main annual
conferences, accompanied by satellite workshops. ETAPS 2019 is the
twenty-second event in the series.
-- MAIN CONFERENCES (8-11 April) --
* ESOP: European Symposium on Programming
(PC chair Luís Caires, Universidade Nova de Lisboa, Portugal)
* FASE: Fundamental Approaches to Software Engineering
(PC chairs Reiner Hähnle, Technische Univ Darmstadt, Germany,
and Wil van der Aalst, RWTH Aachen University, Germany)
* FoSSaCS: Foundations of Software Science
and Computation Structures
(PC chairs Mikolaj Bojanczyk, University of Warsaw, Poland,
and Alex Simpson, University of Ljubljana, Slovenia)
* POST: Principles of Security and Trust
(PC chairs Flemming Nielson, Danmarks Tekniske Univ, Denmark,
and David Sands, Chalmers Tekniska Högskola, Sweden)
* TACAS: Tools and Algorithms for
the Construction and Analysis of Systems
(PC chairs Tomás Vojnar, Brno Univ of Technology, Czech Rep,
and Lijun Zhang, Chinese Academy of Sciences, China)
TACAS '19 hosts the 8th Competition on Software Verification (SV-COMP)
and TOOLympics, an event to celebrate the achievements of the various
competitions or comparative evaluations.
-- INVITED TALKS AND TUTORIALS --
* Unifying speakers:
Marscha Chechik (University of Toronto, Canada)
Kathleen Fisher (Tufts University, USA)
* FoSSaCS invited speaker:
Thomas Colcombet (IRIF, France)
* TACAS invited speaker:
Cormac Flanagan (University of California at Santa Cruz, USA)
* Tutorial speakers:
Dirk Beyer (LMU München, Germany)
Cesare Tinelli (University of Iowa, USA)
-- CONTRIBUTED PAPERS --
See the accepted paper lists at webpages of the individual
conferences.
For the 2nd year, the proceedings of the ETAPS main conferences in
LNCS/ARCoSS will appear in Gold Open Access.
-- PROGRAM --
See the full program here:
https://conf.researchr.org/program/etaps-2019/program-etaps-2019
-- SATELLITE EVENTS (6-7 April) --
18 satellite workshops and other events will take place before
ETAPS 2019.
DICE-FOPARA, GaLoP, HSB, QAPL, SynCoP, VerifyThis,
TOOLympics (6-7 April)
BEHAPI, InterAVT, LiVe, MeTRiD, PERR (6 April)
CREST, HCVS, PLACES, SPIoT, SYNTCOMP Camp,
Mentoring Workshop (7 April)
-- REGISTRATION --
Early registration is until Sunday, 11 March 2019,
https://regmaster4.com/2019conf/ETAPS19/register.php
-- HOST CITY AND VENUE --
ETAPS 2019 will take place in the centre of Prague, the beautiful
capital of the Czech Republic.
The main conferences will be held at Orea Hotel Pyramida, while the
workshops will take place at the School of Computer Science, Faculty of
Mathematics and Physics, Charles University. Both are close to the
Prague Castle.
For the special deal for accommodation at the conference hotel, see
the conference website.
-- HOST INSTITUTION --
ETAPS 2019 is hosted by the School of Computer Science of the Charles
University.
-- ORGANIZERS
Jan Kofron and Jan Vitek (general chairs), Barbora Buhnova, Milan
Ceska, Ryan Culpepper, Vojtech Horky, Paley Li, Petr Maj, Artem
Pelenitsyn, David Safranek
-- FURTHER INFORMATION --
Please do not hesitate to contact the organizers at
jan.kofron@d3s.mff.cuni.cz and j.vitek@neu.edu.
2019-02-18
[Caml-list] CADE-27: Second Call for Papers
The 27th International Conference on Automated Deduction (CADE-27)
Natal, Brazil
25-30 August 2019
http://www.cade-27.info
CALL FOR PAPERS
CADE is the major international forum for presenting research on all aspects
of automated deduction. High-quality submissions on the general topic of
automated deduction, including foundations, applications, implementations,
theoretical results, practical experiences and user studies are solicited.
Key dates:
Abstract deadline (extended): 20 February 2019
Submission deadline (extended): 27 February 2019
* Logics of interest include propositional, first-order, equational,
higher-order, classical, description, modal, temporal, many-valued,
constructive, other non-classical, meta-logics, logical frameworks, type
theory, set theory, as well as any combination thereof.
* Paradigms of interest include theorem proving, model building, constraint
solving, computer algebra, model checking, proof checking, and their
integration.
* Methods of interest include resolution, superposition, completion,
saturation, term rewriting, decision procedures, model elimination,
connection methods, tableaux, sequent calculi, natural deduction, as
well as their supporting algorithms and data structures, including
matching, unification, orderings, induction, indexing techniques, proof
presentation and explanation, proof planning.
* Applications of interest include program analysis, verification and
synthesis of software and hardware, formal methods, computational logic,
computer mathematics, natural language processing, computational
linguistics, knowledge representation, ontology reasoning, deductive
databases, declarative programming, robotics, planning, and other areas
of artificial intelligence.
Submissions can be made in two categories: regular papers and system
descriptions. The page limit in Springer LNCS style is 15 pages excluding
references for regular papers and 10 pages excluding references for system
descriptions. Submissions must be unpublished and not submitted for
publication elsewhere. They will be judged on relevance, originality,
significance, correctness, and readability. System descriptions must
contain a link to a working system and will also be judged on usefulness
and design. Proofs of theoretical results that do not fit in the page limit,
executables of systems, and input data of experiments should be made
available, via a reference to a website or in an appendix of the paper.
For papers containing experimental evaluations, all data needed to rerun
the experiments must be available. Reviewers will be encouraged to consider
this additional material, but submissions must be self-contained within the
respective page limit; considering the additional material should not be
necessary to assess the merits of a submission. The review process will
include a feedback/rebuttal period where authors will have the option to
respond to reviewer comments. The PC chair may solicit further reviews after
the rebuttal period.
The proceedings of the conference will be published in the Springer LNCS/LNAI
series. Formatting instructions and the LNCS style files can be obtained at
http://www.springer.de/comp/lncs/authors.html
At every CADE conference the Program Committee selects one of the accepted
papers to receive the CADE Best Paper Award. The award recognizes a paper
that the Program Committee collegially evaluates as the best in terms of
originality and significance, having substantial confidence in its correctness.
Overall technical quality, completeness, scholarly accuracy, and readability
are also considered. Characteristics associated with a best paper include,
for instance, introduction of a strong new technique or approach, solution
of a long-standing open problem, introduction and solution of an interesting
and important new problem, highly innovative application of known ideas or
existing techniques, and presentation of a new system of outstanding power.
Under exceptional circumstances, the Program Committee may give two awards
(ex aequo) or give no award.
IMPORTANT DATES
Abstract deadline: 20 February 2019
Submission deadline: 27 February 2019
Rebuttal phase: 2 April 2019
Notification: 15 April 2019
Final version: 27 May 2019
SUBMISSION INSTRUCTIONS
Papers should be submitted via
https://easychair.org/conferences/?conf=cade27
CADE-27 ASSOCIATED EVENTS
Automated Reasoning: Challenges, Applications, Directions, Exemplary
Achievements (ARCADE), http://cl-informatik.uibk.ac.at/users/swinkler/arcade/
The CADE ATP System Competition, http://www.tptp.org/CASC/27/
Deduction Mentoring Workshop
Logical and Semantic Frameworks, with Applications (LSFA),
https://sites.google.com/view/lsfa2019
Proof eXchange for Theorem Proving (PxTP), http://pxtp.gforge.inria.fr/2019/
Theorem Prover Components for Educational Software (ThEdu'19),
http://www.uc.pt/en/congressos/thedu/thedu19
The 6th Vampire Workshop
CADE-27 ORGANIZERS
Conference Chair:
Elaine Pimentel Federal University of Rio Grande do Norte, Brazil
Organizers:
Carlos Olarte Federal University of Rio Grande do Norte, Brazil
Joao Marcos Federal University of Rio Grande do Norte, Brazil
Claudia Nalon University of Brasilia, Brazil
Giselle Reis CMU, Qatar
Program Committee Chair:
Pascal Fontaine Universite de Lorraine, CNRS, Inria, LORIA, France
Workshop, Tutorial, and Competition Chair:
Giles Reger University of Manchester, UK
Publicity Chair:
Geoff Sutcliffe University of Miami, USA
Program Committee:
Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina
Franz Baader, TU Dresden, Germany
Clark Barrett, Stanford University, USA
Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands
Maria Paola Bonacina, Universita degli Studi di Verona, Italy
Leonardo Mendonca de Moura, Microsoft Research, USA
Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan
Clare Dixon, University of Liverpool, UK
Mnacho Echenim, Universite de Grenoble, France
Marcelo Finger, University of Sao Paulo, Brazil
Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France
Silvio Ghilardi, Universita degli Studi di Milano, Italy
Juergen Giesl, RWTH Aachen University, Germany
Rajeev Gore, The Australian National University, Australia
Stefan Hetzl, Technische Universitaet Wien, Austria
Marijn J. H. Heule, The University of Texas at Austin, USA
Nao Hirokawa, JAIST, Japan
Moa Johansson, Chalmers University of Technology, Sweden
Cezary Kaliszyk, University of Innsbruck, Austria
Deepak Kapur, University of New Mexico, USA
Benjamin Kiesl, Technische Universitaet Wien, Austria
Konstantin Korovin, The University of Manchester, UK
Laura Kovacs, Technische Universitaet Wien, Austria
Ramana Kumar, DeepMind, UK
Claudia Nalon, University of Brasilia, Brazil
Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany
Carlos Olarte, Federal University of Rio Grande do Norte, Brazil
Jens Otten, University of Oslo, Norway
Andre Platzer, Carnegie Mellon University, USA
Andrew Reynolds, The University of Iowa, USA
Philipp Ruemmer, Uppsala University, Sweden
Renate A. Schmidt, The University of Manchester, UK
Stephan Schulz, DHBW Stuttgart, Germany
Roberto Sebastiani, University of Trento, Italy
Natarajan Shankar, SRI International, USA
Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany
Martin Suda, Czech Technical University, Czech Republic
Geoff Sutcliffe, University of Miami, USA
Rene Thiemann, University of Innsbruck, Austria
Uwe Waldmann, Max Planck Institute for Informatics, Germany
Christoph Weidenbach, Max Planck Institute for Informatics, Germany
Sarah Winkler, University of Innsbruck, Austria
Natal, Brazil
25-30 August 2019
http://www.cade-27.info
CALL FOR PAPERS
CADE is the major international forum for presenting research on all aspects
of automated deduction. High-quality submissions on the general topic of
automated deduction, including foundations, applications, implementations,
theoretical results, practical experiences and user studies are solicited.
Key dates:
Abstract deadline (extended): 20 February 2019
Submission deadline (extended): 27 February 2019
* Logics of interest include propositional, first-order, equational,
higher-order, classical, description, modal, temporal, many-valued,
constructive, other non-classical, meta-logics, logical frameworks, type
theory, set theory, as well as any combination thereof.
* Paradigms of interest include theorem proving, model building, constraint
solving, computer algebra, model checking, proof checking, and their
integration.
* Methods of interest include resolution, superposition, completion,
saturation, term rewriting, decision procedures, model elimination,
connection methods, tableaux, sequent calculi, natural deduction, as
well as their supporting algorithms and data structures, including
matching, unification, orderings, induction, indexing techniques, proof
presentation and explanation, proof planning.
* Applications of interest include program analysis, verification and
synthesis of software and hardware, formal methods, computational logic,
computer mathematics, natural language processing, computational
linguistics, knowledge representation, ontology reasoning, deductive
databases, declarative programming, robotics, planning, and other areas
of artificial intelligence.
Submissions can be made in two categories: regular papers and system
descriptions. The page limit in Springer LNCS style is 15 pages excluding
references for regular papers and 10 pages excluding references for system
descriptions. Submissions must be unpublished and not submitted for
publication elsewhere. They will be judged on relevance, originality,
significance, correctness, and readability. System descriptions must
contain a link to a working system and will also be judged on usefulness
and design. Proofs of theoretical results that do not fit in the page limit,
executables of systems, and input data of experiments should be made
available, via a reference to a website or in an appendix of the paper.
For papers containing experimental evaluations, all data needed to rerun
the experiments must be available. Reviewers will be encouraged to consider
this additional material, but submissions must be self-contained within the
respective page limit; considering the additional material should not be
necessary to assess the merits of a submission. The review process will
include a feedback/rebuttal period where authors will have the option to
respond to reviewer comments. The PC chair may solicit further reviews after
the rebuttal period.
The proceedings of the conference will be published in the Springer LNCS/LNAI
series. Formatting instructions and the LNCS style files can be obtained at
http://www.springer.de/comp/lncs/authors.html
At every CADE conference the Program Committee selects one of the accepted
papers to receive the CADE Best Paper Award. The award recognizes a paper
that the Program Committee collegially evaluates as the best in terms of
originality and significance, having substantial confidence in its correctness.
Overall technical quality, completeness, scholarly accuracy, and readability
are also considered. Characteristics associated with a best paper include,
for instance, introduction of a strong new technique or approach, solution
of a long-standing open problem, introduction and solution of an interesting
and important new problem, highly innovative application of known ideas or
existing techniques, and presentation of a new system of outstanding power.
Under exceptional circumstances, the Program Committee may give two awards
(ex aequo) or give no award.
IMPORTANT DATES
Abstract deadline: 20 February 2019
Submission deadline: 27 February 2019
Rebuttal phase: 2 April 2019
Notification: 15 April 2019
Final version: 27 May 2019
SUBMISSION INSTRUCTIONS
Papers should be submitted via
https://easychair.org/conferences/?conf=cade27
CADE-27 ASSOCIATED EVENTS
Automated Reasoning: Challenges, Applications, Directions, Exemplary
Achievements (ARCADE), http://cl-informatik.uibk.ac.at/users/swinkler/arcade/
The CADE ATP System Competition, http://www.tptp.org/CASC/27/
Deduction Mentoring Workshop
Logical and Semantic Frameworks, with Applications (LSFA),
https://sites.google.com/view/lsfa2019
Proof eXchange for Theorem Proving (PxTP), http://pxtp.gforge.inria.fr/2019/
Theorem Prover Components for Educational Software (ThEdu'19),
http://www.uc.pt/en/congressos/thedu/thedu19
The 6th Vampire Workshop
CADE-27 ORGANIZERS
Conference Chair:
Elaine Pimentel Federal University of Rio Grande do Norte, Brazil
Organizers:
Carlos Olarte Federal University of Rio Grande do Norte, Brazil
Joao Marcos Federal University of Rio Grande do Norte, Brazil
Claudia Nalon University of Brasilia, Brazil
Giselle Reis CMU, Qatar
Program Committee Chair:
Pascal Fontaine Universite de Lorraine, CNRS, Inria, LORIA, France
Workshop, Tutorial, and Competition Chair:
Giles Reger University of Manchester, UK
Publicity Chair:
Geoff Sutcliffe University of Miami, USA
Program Committee:
Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina
Franz Baader, TU Dresden, Germany
Clark Barrett, Stanford University, USA
Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands
Maria Paola Bonacina, Universita degli Studi di Verona, Italy
Leonardo Mendonca de Moura, Microsoft Research, USA
Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan
Clare Dixon, University of Liverpool, UK
Mnacho Echenim, Universite de Grenoble, France
Marcelo Finger, University of Sao Paulo, Brazil
Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France
Silvio Ghilardi, Universita degli Studi di Milano, Italy
Juergen Giesl, RWTH Aachen University, Germany
Rajeev Gore, The Australian National University, Australia
Stefan Hetzl, Technische Universitaet Wien, Austria
Marijn J. H. Heule, The University of Texas at Austin, USA
Nao Hirokawa, JAIST, Japan
Moa Johansson, Chalmers University of Technology, Sweden
Cezary Kaliszyk, University of Innsbruck, Austria
Deepak Kapur, University of New Mexico, USA
Benjamin Kiesl, Technische Universitaet Wien, Austria
Konstantin Korovin, The University of Manchester, UK
Laura Kovacs, Technische Universitaet Wien, Austria
Ramana Kumar, DeepMind, UK
Claudia Nalon, University of Brasilia, Brazil
Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany
Carlos Olarte, Federal University of Rio Grande do Norte, Brazil
Jens Otten, University of Oslo, Norway
Andre Platzer, Carnegie Mellon University, USA
Andrew Reynolds, The University of Iowa, USA
Philipp Ruemmer, Uppsala University, Sweden
Renate A. Schmidt, The University of Manchester, UK
Stephan Schulz, DHBW Stuttgart, Germany
Roberto Sebastiani, University of Trento, Italy
Natarajan Shankar, SRI International, USA
Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany
Martin Suda, Czech Technical University, Czech Republic
Geoff Sutcliffe, University of Miami, USA
Rene Thiemann, University of Innsbruck, Austria
Uwe Waldmann, Max Planck Institute for Informatics, Germany
Christoph Weidenbach, Max Planck Institute for Informatics, Germany
Sarah Winkler, University of Innsbruck, Austria
Subscribe to:
Posts (Atom)