2017-01-24

[Caml-list] First Call for Papers - 10th Conference on Intelligent Computer Mathematics - CICM 2017 - Abstract Submission Deadline 15. March 2017

Call for Papers

10th Conference on Intelligent Computer Mathematics
- CICM 2017 -
July 17-21, 2016
University of Edinburgh, Scotland
http://www.cicm-conference.org/2017

----------------------------------------------------------------------

Digital and computational solutions are becoming the prevalent means
for the generation, communication, processing, storage and curation of
mathematical information. Separate communities have developed to
investigate and build computer based systems for computer algebra,
automated deduction, and mathematical publishing as well as novel user
interfaces. While all of these systems excel in their own right, their
integration can lead to synergies offering significant added
value. The Conference on Intelligent Computer Mathematics (CICM)
offers a venue for discussing and developing solutions to the great
challenges posed by the integration of these diverse areas.

CICM has been held annually as a joint meeting since 2008, co-locating
related conferences and workshops to advance work in these
subjects. Previous meetings have been held in Birmingham (UK 2008),
Grand Bend (Canada 2009), Paris (France 2010), Bertinoro (Italy 2011),
Bremen (Germany 2012), Bath (UK 2013), Coimbra (Portugal 2014),
Washington DC (USA 2015) and Bialystok (Poland 2016).

This is a call for papers for CICM 2017, which will be held in
Edinburgh, Scotland, July 17-21, 2016. CICM 2017 also invites work-in-
progress papers.

The principal tracks of the conference will be:

* Track: Calculemus (chair: Matthew England)
All topics in the intersection of computer algebra systems and
automated reasoning systems including:
- Automated theorem proving in computer algebra systems.
- Computer algebra and symbolic computation in theorem proving
systems.
- Theory, design and implementation of interdisciplinary systems for
computer mathematics.
- Case studies and applications that involve a mix of computation
and reasoning.
- Case studies in formalization of mathematical theories that include
non-trivial computations.
- Representation of mathematics in computer algebra systems.
- Input languages, programming languages, types and constraint
languages, and modeling languages for mathematical assistant systems.

* Track: Digital Mathematical Libraries (DML) (chair: Olaf Teschke)
All topics related to the formation of a Global Digital Mathematics
Library (GDML) network, ranging from experiences from existing DMLs,
policies and standards facilitating interoperability, to development
and integration of new techniques for content creation,
preservation, enhancement and retrieval of the corpus, including:
- DML creation and maintenance (content aggregation, validation,
curation, enhancement).
- DML architecture and representations (organization, workflows,
policies, standards).
- DML access and applications (retrieval, interfaces, interoperability).
- DML collections and systems (experiences from various existing DMLs).

* Track: Mathematical Knowledge Management (MKM) (chair: Florian Rabe)
- Knowledge representation using, e.g., formal logics, computational
systems, narrative document formats, or databases
- Solutions to create, store, disseminate, discover, or manipulate
mathematical knowledge
- Corpora of knowledge inlcuding documents, theories, theorems, proofs,
models, algorithms, exercises, or examples
- Methods, systems, frameworks, case studies, challenges, benchmarks,
or applications for mathematical knowledge
- Comparisons, evaluations, or integrations of MKM solutions

* Track: Systems & Projects (chair: Osman Hasan)
- Systems: Stand-alone; plugins, libraries, or extensions of
existing systems; or integrations of existing systems
- Data: Formalizations; harvests or new processing of existing data;
or case studies, test cases, or benchmark suites for systems
- Projects: finished, ongoing or new
- Survey papers

* Track: Doctoral Programme (chair: TBD)

The overall programme is organized by the General Program Chair Herman
Geuvers. The local arrangements will be coordinated by Jacques
Fleuriot. The publicity chair is Serge Autexier.

We plan to have proceedings of the conference as in previous years
with Springer Verlag as a volume in Lecture Notes in Artificial
Intelligence (LNAI).

*Important Dates*

Conference submissions
- Abstract submission deadline: 15. March 2017
- Submission deadline: 22. March 2017
- Reviews sent to authors: 26. April 2017
- Rebuttals due: 30. April 2017
- Notification of acceptance: 12. May 2017
- Camera ready copies due: 26. May 2017
- Conference: 17.-21. July 2017

Workshop Proposals
- Submission deadline: 10. February 2017
- Notification of acceptance: 15. February 2017

More details on the conference are available from

http://www.cicm-conference.org/2017

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

2017-01-21

[Caml-list] ETAPS 2017 call for participation

******************************************************************

CALL FOR PARTICIPATION

ETAPS 2017

20th European Joint Conferences on Theory And Practice of Software
ETAPS 2017

Uppsala, Sweden, 22-29 April 2017

http://www.etaps.org/2017

******************************************************************

-- 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 2017 is the
twentieth event in the series.


-- MAIN CONFERENCES (24-28 April) --

* ESOP: European Symposium on Programming
(PC chair Hongseok Yang, University of Oxford, UK)
* FASE: Fundamental Approaches to Software Engineering
(PC chairs Marieke Huisman, Universiteit Twente, The
Netherlands, and Julia Rubin, University of British Columbia,
Canada)
* FoSSaCS: Foundations of Software Science
and Computation Structures
(PC chairs Javier Esparza, Technische Universität München,
Germany, Andrzej Murawski, University of Warwick, UK)
* POST: Principles of Security and Trust
(PC chairs Matteo Maffei, Universität des Saarlandes, Germany,
Mark D. Ryan, University of Birmingham, UK)
* TACAS: Tools and Algorithms for
the Construction and Analysis of Systems
(PC chairs Axel Legay, INRIA Rennes, France,
and Tiziana Margaria, LERO, Ireland)

TACAS '17 hosts the 6th Competition on Software Verification
(SV-COMP).


-- INVITED SPEAKERS --

* Unifying speakers:
Michael Ernst (University of Washington, USA)
Kim G. Larsen (Aalborg University, DK)

* FoSSaCS invited speaker:
Joel Ouaknine (University of Oxford, UK)

* TACAS invited speaker:
Dino Distefano (Facebook and Queen Mary University of London, UK)


-- UNIFYING PUBLIC LECTURE

Serge Abiteboul (DI, INRIA Paris & ENS Cachan, France)


-- INVITED TUTORIALS

Véronique Cortier (LORIA, CRNS, France)

Kenneth McMillan (Microsoft Research Redmond, USA)


-- CONTRIBUTED PAPERS --

See the accepted paper lists at the conference website.


-- SATELLITE EVENTS (22-23 April, 29 April) --

17 satellite workshops and other events will take place before or
after ETAPS 2017.

Check their calls for papers and consider contributing!

DICE-FOPARA, GaLoP, GaM, SynCop-PV, VerifyThis (22-23 April)

FESCA, SNR (22 April)
HotSpot, MBT, QAPL, SannellaFest (23 April)

BX, CREST, LiVe, MARS, PLACES, VPT (29 April)


-- REGISTRATION --

Early registration is until Sunday, 12 March 2017 (23:59 GMT+1).

http://www.etaps.org/2017/registration


-- ACCOMMODATION --

The organizers have negotiated special rates from several hotels in
Uppsala.

To benefit from those, follow the instructions on the conference
website. The offers expire on different dates.


-- HOST CITY --

Uppsala city holds a rich history, having for long periods been the
political, religious and academic centre of Sweden. Uppsala
University is over 500 years old and ranked among the top 100 in the
World and has hosted many great scientists over the years, for
instance Carl von Linné, Anders Celsius and Anders Jonas Ångström. The
proximity to the capital of Sweden, Stockholm, provides additional
benefits as a potential site for arranging both pre- and post congress
tours, as well as for excursions or tourism.


-- HOST INSTITUTION --

ETAPS 2017 is hosted by the Department of Information Technology,
Uppsala University.


-- ORGANIZERS

Parosh Abdulla (General chair), Mohamed Faouzi Atig,
Andreina Francisco, Kaj Lampka, Philipp Rümmer, Konstantinos Sagonas,
Björn Victor, Wang Yi, Tjark Weber, Yunyun Zhu


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

2017-01-19

[Caml-list] Call for Participation: BOB 2017 (24. Februar, Berlin) - early-bird ends Jan 23

BOB has a strong focus on functional programming. Come and strengthen
our OCaml contingent!

================================================================

Konferenz

BOB 2017

"Was passiert, wenn wir einfach mal das Beste nehmen?"
24.2.2017
Berlin
http://bobkonf.de/2017/
Programm:
http://bobkonf.de/2017/program.html
Anmeldung:
http://bobkonf.de/2017/registration.html

================================================================

Auf der BOB treffen sich Entwickler, Architekten und Macher, um Pfade
jenseits der Mainstream-Technologien zu beschreiten und die besten
Werkzeuge aufzuspüren, die es heute für die Entwicklung moderner
Software gibt. Unser Ziel ist, dass alle Teilnehmer die Konferenz mit
vielen neuen Erfahrungen verlassen und Verbesserungen für ihr eigenes
Entwicklungsumfeld mit nach Hause nehmen.

Im Programm befinden sich 14 Vorträge und 8 Tutorials zu aktuellen
Themen:

http://bobkonf.de/2017/program.html

Die Themenspanne der Vorträge enthält u.a. funktionaler
Programmierung, Front-End-Entwicklung und fortgeschrittener Nutzung
von Typen.

Die Tutorials - allesamt von ausgewiesenen Experten ihres Fachs
gehalten - beschäftigen sich mit Haskell, Swift, PureScript, React,
QuickCheck, Agda, CRDTs und Servant.

Die Keynote wird John Hughes halten.

Die Anmeldung ist online auf folgender Seite möglich:

http://bobkonf.de/2017/registration.html

WICHTIG: Die Early-Bird-Tarife laufen am 23.1.2017 aus!

Die BOB wird in Kooperation mit der :clojured direkt am Folgetag in
Berlin organisiert - wer beide Konferenzen besucht, profitiert von
Anmelderabatt!

http://www.clojured.de/

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

2017-01-18

[Caml-list] FMCAD 2017 - Call for Papers

CALL FOR PAPERS

International Conference on
Formal Methods in Computer-Aided Design (FMCAD)
Vienna, Austria, October 2-6, 2017

http://www.fmcad.org/FMCAD17


IMPORTANT DATES

Abstract Submission: May 01, 2017
Paper Submission: May 08, 2017
Author Response Period: June 19-23, 2017
Author Notification: July 14, 2017
Camera-Ready Version: Aug 09, 2017

All deadlines are 11:59 pm AoE (Anywhere on Earth)

FMCAD Tutorial Day: October 2, 2017
FMCAD Regular Program: October 3-6, 2017

Part of the FMCAD 2017 program:
- Symposium in memoriam of Helmut Veith
- FMCAD Student Forum

CONFERENCE SCOPE AND PUBLICATION

FMCAD 2017 is the seventeenth in a series of conferences on the theory and
applications of formal methods in hardware and system verification. FMCAD
provides a leading forum to researchers in academia and industry for
presenting and discussing groundbreaking methods, technologies, theoretical
results, and tools for reasoning formally about computing systems. FMCAD
covers formal aspects of computer-aided system design including verification,
specification, synthesis, and testing.

FMCAD employs a rigorous peer-review process. Accepted papers are distributed
through both ACM and IEEE digital libraries. In addition, published articles
are made available freely on the conference page; the authors retain the
copyright. There are no publication fees. At least one of the authors is
required to register for the conference and present the accepted paper. A
small number of outstanding FMCAD submissions will be considered for
inclusion in a Special Issue of the journal on Formal Methods in System
Design (FMSD).


TOPICS OF INTEREST

FMCAD welcomes submission of papers reporting original research on advances
in all aspects of formal methods and their applications to computer-
aided design. Topics of interest include (but are not limited to):

-- Model checking, theorem proving, equivalence checking, abstraction and
reduction, compositional methods, decision procedures at the bit- and
word-level, probabilistic methods, combinations of deductive methods and
decision procedures.

-- Synthesis and compilation for computer system descriptions, modeling,
specification, and implementation languages, formal semantics of
languages and their subsets, model-based design, design derivation and
transformation, correct-by-construction methods.

-- Application of formal and semi-formal methods to functional and
non-functional specification and validation of hardware and software,
including timing and power modeling, verification of computing systems
on all levels of abstraction, system-level design and verification for
embedded systems, cyber-physical systems, automotive systems and
other safety-critical systems, hardware-software co-design and
verification, and transaction-level verification.

-- Experience with the application of formal and semi-formal methods to
industrial-scale designs; tools that represent formal verification
enablement, new features, or a substantial improvement in the automation
of formal methods.

-- Application of formal methods to verifying safety, correctness,
connectivity, and security properties of networks and distributed
systems.


SUBMISSIONS

Submissions must be made electronically in PDF format via EasyChair:

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

Two categories of papers are invited: Regular papers, and Tool & Case Study
papers. Regular papers are expected to offer novel foundational ideas,
theoretical results, or algorithmic improvements to existing methods,
along with experimental impact validation where applicable. Tool & Case
Study papers are expected to report on the design, implementation or use of
verification (or related) technology in a practically relevant context
(which need not be industrial), and its impact on design processes.

Both Regular and Tool & Case study papers must use the IEEE Transactions
format on letter-size paper with a 10-point font size. Regular papers can be
up to 8 pages in length and tool papers up to 4 pages, although there
is no requirement to fill all pages in either category. Authors will be
required to select the appropriate paper category at abstract submission
time. Submissions may contain an optional appendix, which will not appear
in the final version of the paper. The reviewers should be able to assess
the quality and the relevance of the results in the paper without reading
the appendix.

Submissions in both categories must contain original research that has not
been previously published, nor is concurrently submitted for publication.
Any partial overlap with published or concurrently submitted papers must be
clearly indicated. If experimental results are reported, authors are
strongly encouraged to provide the reviewers access to their data at
submission time, so that results can be independently verified.

FMCAD 2017 COMMITTEES

PROGRAM CHAIRS:

Daryl Stewart, ARM
Georg Weissenbacher, TU Wien

STUDENT FORUM CHAIR:

Keijo Heljanko, Aalto University

LOCAL ARRANGEMENTS CHAIR & WEBMASTER:

Jens Katelaan, TU Wien

PUBLICATION CHAIR:

Mitra Tabaei Befrouei, TU Wien

PROGRAM COMMITTEE

Jade Alglave University College London and Microsoft Research
Christel Baier Technical University of Dresden
Roderick Bloem Graz University of Technology
Hana Chockler King's College London
Andreas Griesmayer ARM
Arie Gurfinkel University of Waterloo
Ziyad Hanna Cadence Design Systems
Fei He Tsinghua University
Alan J. Hu University of British Columbia
Warren A. Hunt Jr. University of Texas
Alexander Ivrii IBM
Barbara Jobstmann EPFL and Cadence Design Systems
Dejan Jovanovic SRI International
Gerwin Klein Data61 and UNSW Australia
Igor Konnov TU Wien
Rebekah Leslie-Hurd Intel
Ines Lynce INESC-ID/IST, Universidade de Lisboa
Ken McMillan Microsoft Research
Charles Morisset Newcastle University
Lee Pike Galois Inc.
Mitra Purandare IBM
Ajitha Rajan University of Edinburgh
Ahmed Rezine Linköping University
Sean Safarpour Synopsys
Roopsha Samanta Purdue University
Martina Seidl Johannes Kepler University Linz
Natasha Sharygina USI Lugano
Anna Slobodova Centaur Technology
Ana Sokolova University of Salzburg
Daryl Stewart ARM
Murali Talupur FormalSim
Michael Tautschnig Queen Mary University of London
Thomas Wahl Northeastern University
Chao Wang University of Southern California
Georg Weissenbacher TU Wien
Florian Zuleger TU Wien

FMCAD STEERING COMMITTEE

Armin Biere, Johannes Kepler University in Linz, Austria
Alan Hu, University of British Columbia, Canada
Warren A. Hunt Jr., University of Texas at Austin, USA
Vigyan Singhal, Oski Tech


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] DL 2017, Call for Papers

-------------------------------------------------------------------------------
CALL FOR PAPERS
30th International Workshop on Description Logics, DL 2017
July 18th to July 21st, 2017 - Montpellier, France
http://dl.kr.org/dl2017/
-------------------------------------------------------------------------------

Call for Papers
====================
DL 2017: the 30th International Workshop on Description Logics

The DL workshop is the major annual event of the description logic research
community. It is the forum at which those interested in description logics,
both from academia and industry, meet to discuss ideas, share information and
compare experiences. The workshop will be held in Montpellier, France from
July 18th to July 21st, 2017.

Important Dates (Firm Deadlines)
============
Paper registration deadline:
April 28, 2017
Paper submission deadline:
May 8, 2017
Notification of acceptance:
June 12, 2017
Camera-ready copies:
July 3, 2017
Workshop:
July 18-21, 2017

Since we want the DL submission deadlines to be after the IJCAI notification
date, the schedule is tight and NO DEADLINE EXTENSIONS will be possible.


Invited Speakers
=============
* Markus Krötzsch, Technical University of Dresden
* Andreas Pieris, University of Edinburgh
* Uli Sattler, University of Manchester


Workshop Scope
=============
We invite contributions on all aspects of description logics, including but
not limited to:
* Foundations of description logics: decidability and complexity of reasoning,
expressive power, novel inference problems, inconsistency management,
reasoning techniques, and modularity aspects
* Extensions of description logics: closed-world and nonmonotonic reasoning,
epistemic reasoning, temporal and spatial reasoning, procedural knowledge,
query answering, reasoning over dynamic information
* Integration of description logics with other formalisms: object-oriented
representation languages, database query languages, constraint-based
programming, logic programming, and rule-based systems
* Applications and use areas of description logics: ontology engineering,
ontology languages, databases, ontology-based data access, semi-structured
data, graph structured data, linked data, document management, natural
language, learning, planning, Semantic Web, cloud computing, conceptual
modelling, web services, business processes
* Systems and tools around description logics: reasoners, software tools for
and using description logic reasoning (e.g. ontology editors, database
schema design, query optimisation, and data integration tools),
implementation and optimisation techniques, benchmarking, evaluation,
modelling


Submissions
==========
* Submissions may be of two types:
(1) Papers accepted at some conference can be submitted as accepted elsewhere
together with a 1-page abstract that also specifies where the paper has
been accepted.
(2) Other submissions consist of 11 pages LNCS plus references. There is no
page limit on the list of references. If the paper should not appear in
the proceedings, an additional 1-page abstract has to be submitted.

* For submissions with an additional 1-page abstract, only the abstract is
published in the proceedings. The abstracts might not be indexed in dblp.
This option is designed for authors who wish to announce results that have
been published elsewhere, or which the authors intend to submit or have
already submitted to a venue with an incompatible prior / concurrent
publication policy.
* All submissions may optionally include a clearly marked appendix (e.g.,
with additional proofs or evaluation data). The appendix will be read at
the discretion of the reviewers and not included in the proceedings. The
appendix does not need to be in LNCS format.
* Submission page: https://easychair.org/conferences/?conf=dl2017
* Accepted papers and 1-page abstracts will be made available electronically
in the CEUR Workshop Proceedings series (http://www.CEUR-ws.org/).
* Accepted submissions, be they full papers or 1-page abstracts, will be
selected for either oral or poster presentation at the workshop. Submissions
will be judged solely based upon their content, and the type of submission
will have no bearing on the decision between oral and poster presentation.

Organisation
==========
* Alessandro Artale, Free University of Bozen-Bolzano (Programme co-Chair)
* Birte Glimm, University of Ulm (Programme co-Chair)
* Meghyn Bienvenu, University of Montpellier (Workshop co-Chair)
* Marie-Laure Mugnier, University of Montpellier (Workshop co-Chair)

Resources
========
* Information about submission, registration, travel information, etc., is
available on the DL 2017 homepage: http://dl.kr.org/dl2017/
* The official description logic homepage is at http://dl.kr.org/

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] CAV 2017: Call for Papers

CAV 2017: 29th International Conference on Computer-Aided Verification


Important Dates: All deadlines are AOE (Anywhere on Earth).

Papers:
  Paper submission: January 24, 2017 (Tuesday)
  Author response period: March 20-22, 2017 (Monday – Wednesday)
  Author notification: April 12, 2017 (Wednesday)
  Final version: May 5, 2017 (Friday)

Conference:
  Workshops: July 22-23, 2017
  Main conference: July 24-28, 2017

Submission URL


Scope

CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis and synthesis methods for hardware and software systems.  CAV considers it vital to continue spurring advances in hardware and software verification while expanding to domains such as cyber-physical, social, and biological systems.  The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer LNCS series. A selection of papers will be invited to a special issue of Formal Methods in System Design and the Journal of the ACM.

Topics of interest include but are not limited to:

Algorithms and tools for verifying models and implementations
Algorithms and tools for system synthesis
Mathematical and logical foundations of verification and synthesis
Specifications and correctness criteria for programs and systems
Deductive verification using proof assistants
Hardware verification techniques
Program analysis and software verification
Software synthesis
Hybrid systems and embedded systems verification
Compositional and abstraction-based techniques for verification
Probabilistic and statistical approaches to verification
Verification methods for parallel and concurrent systems
Testing and run-time analysis based on verification technology
Decision procedures and solvers for verification and synthesis
Applications and case studies in verification and synthesis
Verification in industrial practice
New application areas for algorithmic verification and synthesis
Formal models and methods for security
Formal models and methods for biological systems


Paper Submission

NEW this year:
There is no separate registration deadline. Full papers should be uploaded by the submission deadline.
Tool papers require a concurrent artifact submission together with the paper submission. Artifact evaluation occurs concurrently with the review process and the PC gets access to the artifact evaluation during the PC discussions.
Submissions on a wide range of topics are sought, particularly ones that identify new research directions.  CAV 2017 is not limited to topics discussed in previous instances of the conference.  Authors concerned about the appropriateness of a topic may communicate with the conference chairs prior to submission.

As explained below, CAV 2017 will follow a lightweight double-blind review process.  Submissions that are not "blinded" will be rejected without review.  Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed.  The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments.  The PC chairs may solicit further reviews after the rebuttal period.

Papers must be submitted in PDF format here

Submissions will be in two categories: Regular Papers and Tool Papers.

Regular Papers

Regular Papers should not exceed 16 pages in LNCS format, not counting references and appendices.  Authors can include a clearly marked appendix at the end of their submissions, that is exempt from the page limit restrictions. However, the reviewers are not obliged to read the contents of these appendices.  These papers should contain original research and sufficient detail to assess the merits and relevance of the contribution.  Papers will be evaluated on basis of a combination of correctness, technical depth, significance, novelty, clarity, and elegance. We welcome papers on theory, case studies, and comparisons with existing experimental research, as well as combinations of new theory with experimental evaluation.  A strong theoretical paper is not required to have an experimental component.  On the other hand, strong papers reproducing and comparing existing results experimentally do not require new theoretical insights.

We encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs or experimental data.  These materials should be uploaded at submission time, as a single pdf or a tarball, not via a URL.  It will be made available to reviewers only after they have submitted their first-draft reviews and hence need not be anonymized.  Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper.

Tool Papers

Tool Papers should not exceed 6 pages, not counting references.  These papers should describe system and implementation aspects of a tool with a large (potential) user base (experiments not required, rehash of theory strongly discouraged).  Papers describing tools that have already been presented (in any conference) will be accepted only if significant and clear enhancements to the tool are reported and implemented.  Note that tool papers require the submission of an artifact for evaluation by the submission deadline.  Artifacts will be evaluated concurrently with the review process and the program committee will have access to the artifact evaluation while making their decision.  In special cases, where an artifact cannot be submitted, the authors should contact the program chairs to find alternate modes of artifact evaluation.

Lightweight Double-Blind Reviewing Process
CAV 2017 will employ a lightweight double-blind reviewing process. This means that committee members will not have access to authors' names or affiliations as they review a paper; however, authors' names will be revealed once reviews have been submitted.

To facilitate this, submitted papers must adhere to two rules:
Author names and institutions must be omitted, and references to authors' own related work should be in the third person (e.g., not "We build on our previous work…" but rather "We build on the work of …").

The purpose of this process is to help the PC and external reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try.  Nothing should be done in the name of anonymity that weakens the submission, makes the job of reviewing the paper more difficult, or interferes with the process of disseminating new ideas. For example, important background references should *not* be omitted or anonymized, even if they are written by the same authors and share common ideas, techniques, or infrastructure.  Authors should feel free to disseminate their ideas or draft versions of their paper as they normally would.  For instance, authors may post drafts of their papers on the web or give talks on their research ideas.



Artifact Submission and Evaluation

Authors of accepted regular papers will be invited to submit (but are not required to submit) the relevant artifact for evaluation by the artifact evaluation committee.

Authors of all tool papers are required to submit their artifact to the artifact evaluation committee at the paper submission time. Unlike regular papers, the results of the artifact evaluation for tool papers will be available to the program committee during the online discussions.

To submit an artifact, please prepare a virtual machine (VM) image of your artifact and keep it accessible through an HTTP link throughout the evaluation process. As the basis of the VM image, please choose commonly used OS versions that have been tested with the virtual machine software and that evaluators are likely to be accustomed to. We encourage you to use https://www.virtualbox.org and save the VM image as an Open Virtual Appliance (OVA) file. Please include the prepared link in the appropriate field of the paper submission form.

In addition, please supply at submission time a link to a short plain-text file describing the OS and parameters of the image, as well as the host platform on which you prepared and tested your virtual machine image (OS, RAM, number of cores, CPU frequency). Please describe how to proceed after booting the image, including the instructions for locating the full documentation for evaluating the artifact.

If you are not in a position to prepare the artifact as above, please contact PC chairs for an alternative arrangement.

It is to the advantage of authors to prepare an artifact that is easy to evaluate by the artifact evaluation committee and that yields expected results. We next provide some guidelines.  Document in detail how to reproduce most of the experimental results of the paper using the artifact; keep this process simple through easy-to-use scripts and provide detailed documentation assuming minimum expertise of users. Ensure the artifact is in the state ready to run. It should work without a network connection. It should not require the user to install additional software before running. It should use reasonably modest resources (RAM, number of cores), so that the results can be reproduced on various hardware platforms including laptops. The evaluation should take reasonable amount of time to complete. When possible include source code within your virtual machine image and point to the most relevant and interesting parts of the source code tree.

Members of the artifact evaluation committee and the program committee are asked to use submitted artifact for the sole purpose of evaluating the contribution associated with the artifact.


Invited speakers

* Chris Hawblitzel, Microsoft Research:Chris Hawblitzel, Microsoft Research
  Fast verification of fast cryptography for secure sockets

* Marta Kwiatkowska, OxfordMarta Kwiatkowska, Oxford

* Viktor Vafeiadis, MPI-SWSViktor Vafeiadis, MPI-SWS
  Formal reasoning under weak memory consistency


Organization

Conference co-chairs
Viktor Kuncak, EPFL, Switzerland
Rupak Majumdar, Max Planck Institute for Software Systems, Germany

Workshop Chair
Eva Darulová, Max Planck Institute for Software Systems, Germany

Sponsorship Chair
Barbara Jobstmann, EPFL and Cadence

CAV Fellowship Chair
Thomas Wahl, Northeastern University

Publicity Chair
Mikaël Mayer, EPFL

CAV Award Committee
Tom Ball  (Chair), Microsoft research
Kim G. Larsen, Aalborg University
Natarajan Shankar, SRI International
Pierre Wolper, Liege University

Program Committee
Aws Albarghouthi
Christel Baier
Per Bjesse
Jasmin Blanchette
Sergiy Bogomolov
Ahmed Bouajjani
Rohit Chadha
Bor-Yuh Evan Chang
Swarat Chaudhuri
Wei-Ngan Chin
Hana Chockler
Alessandro Cimatti
Isil Dilig
Dino Distefano
Cezara Dragoi
Michael Emmi
Javier Esparza
Georgios Fainekos
Azadeh Farzan
Aarti Gupta
Gerard Holzmann
Marieke Huisman
Radu Iosif
Franjo Ivancic
Stefan Kiefer
Zachary Kincaid
Barbara König
Daniel Kröning
Viktor Kuncak(Co-chair)
Rustan Leino
Rupak Majumdar (Co-chair)
Kenneth McMillan
Alexander Nadel
Madhusudan Parthasarathy
Corina Pasareanu
Nadia Polikarpova
Pavithra Prabhakar
Arjun Radhakrishna
Zvonimir Rakamaric
Andrey Rybalchenko
Roopsha Samanta
Rahul Sharma
Anna Slobodova
Ana Sokolova
Fabio Somenzi
Zhendong Su
Serdar Tasiran
Emina Torlak
Willem Visser
Mahesh Viswanathan
Yakir Vizel
Tomas Vojnar
Thomas Wahl
Bow-Yaw Wang
Georg Weissenbacher
Verena Wolf
Lenore Zuck
Damien Zufferey

Steering Committee
Orna Grumberg, Technion, Israel
Aarti Gupta, Princeton University, USA
Daniel Kroening, University of Oxford, UK
Kenneth McMillan, Microsoft Research, USA

Artifact Evaluation Committee
Ayca Balkan, UCLA
Stephanie Balzer, CMU
James Bornholt, University of Washington
Simon Cruanes, INRIA Nancy
Matthias Dangl University of Passau
Marko Doko, MPI-SWS
Chuchu Fan, UIUC
Pietro Ferrara, Julia
Johannes Hoelzl, TU Munich
Lars Hupel, TU Munich
Swen Jacobs, Saarland University
Moa Johansson, Chalmers
Dejan Jovanovic, SRI
Ralf Jung, MPI-SWS
Ivan Kuraj, MIT
Andreas Lochbihler, ETH Zurich
Jose Morales, IMDEA
Van Chan Ngo, CMU
Zvonimir Pavlinovic, NYU
Markus Rabe, UC Berkeley
Mukund Raghothaman, UPenn
Andrew Reynolds, University of Iowa
Nima Roohi, UIUC
Christian Schilling, University of Freiburg
Muralidaran Vijayaraghavan, MIT
Nicolas Voirol, EPFL

2017-01-16

[Caml-list] iFM 2017: Call for Papers (13th Intl. Conference on integrated Formal Methods), submission open


CALL FOR PAPERS

************************************************************************

13th International Conference on
integrated Formal Methods (iFM 2017)


Turin, Italy, 20-22 September 2017

************************************************************************

Important dates

    Abstract submission: Tuesday March 28
    Paper submission: Tuesday April 4
    Notification: Friday May 26
    Camera-ready copy: Tuesday June 11
    Conference: September 20-22

Deadlines expire at 23:59 anywhere on earth on the dates displayed above.


Objectives and Scope

Applying formal methods may involve the usage of different formalisms and different analysis techniques to validate a system, either because individual components are most amenable to one formalism or technique, because one is interested in different properties of the system, or simply to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modeling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding both modeling and analysis. The conference covers all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.

Areas of interest include but are not limited to:

- Formal and semi-formal modelling notations
- Combining formal methods
- Integration of formal methods into software engineering practice
- Program verification, model checking, and static analysis
- Runtime analysis, monitoring, and testing
- Program synthesis
- Analysis and synthesis of hybrid, embedded, probabilistic, distributed, or concurrent systems
- Model learning
- Theorem proving, decision procedures, SAT and SMT solving 


Submission Guidelines

iFM 2017 solicits high quality papers reporting research results and/or experience reports related to the overall theme of method integration.

We solicit papers in the following categories:

- Research papers describe original scientific research results, validated by experimental results where applicable. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. Limit: 15 pages.
- Case study papers report on applications of formal methods, preferably in a real world setting. A case study paper need not introduce novel techniques or tools, but it must include a rigorous empirical evaluation and potentially be of interest to practitioners. Limit: 15 pages.
- Regular tool papers present a new tool or novel extensions to an existing tool. They should provide a short description of the theoretical foundations, while focusing on the tool's design and implementation concerns, as well as empirical evaluation of its practical capabilities. Papers that present extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions of the tool. Authors are strongly encouraged to make their tools publicly available, preferably on the web. Limit: 15 pages.
- Tool demonstration papers focus on the usage aspects of tools. Foundations and empirical evaluation are not required, but the paper should explain why the tool is relevant for the community, and, in particular, for practitioners. As with regular tool papers, authors are strongly encouraged to make their tools publicly available, preferably on the web. Limit: 8 pages.

Page limits include bibliography and any appendices. All submissions must be original, unpublished, and not submitted for publication elsewhere. Each paper will undergo a thorough review process.

Submissions should be made using the iFM 2017 Easychair site: https://easychair.org/conferences/?conf=ifm2017  Submissions must be in PDF format, using the Springer LNCS style files; we suggest to use the LaTeX2e package (the llncs.cls class file, available in llncs2e.zip and the typeinst.dem available in typeinst.zip as a template for your contribution). The conference proceedings will be published in the Formal Methods subline of Springer's Lecture Notes in Computer Science series.

All accepted papers must be presented at the conference. Their authors must be prepared to sign a copyright transfer statement. At least one author of each accepted paper must register to the conference by the early registration date, to be indicated by the organizers, and present the paper.

Invited Speakers

-Jane Hillston (University of Edinburgh, UK)

-André Platzer (CMU, USA)

-Matrin Vechev (ETH Zurich, Switzerland)


Best Paper Prizes

We are pleased to have received generous sponsorship from Springer for two Best Paper awards of 500 EUR each.  These awards will be decided by the Programme Committee, and will be announced and awarded at the conference.


Workshops

iFM 2017 will be accompanied by a series of workshops. Further information is available from the conference website http://ifm2017.di.unito.it/


Conference Location

iFM 2017 is organized by the University of Turin and will take place in Turin, Italy

Ingrid Chieh Yu
Associate professor
Dept. of Informatics, University of Oslo
Tel + 47 2284 5525, email ingridcy@ifi.uio.no


2017-01-13

[Caml-list] CADE-26 Call for Papers

The 26th International Conference on Automated Deduction (CADE-26)
Gothenburg, Sweden

6-11 August 2017

http://www.cade-26.info

CALL FOR PAPERS

CADE is the major international forum at which research on all aspects
of automated deduction is presented. 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: 11 February 2017
Submission deadline: 18 February 2017

* 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 chairs 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: 11 February 2017
Submission deadline: 18 February 2017
Rebuttal phase: 8 April 2017
Notification: 22 April 2017
Final version: 27 May 2017

SUBMISSION INSTRUCTIONS

Papers should be submitted via

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

CADE-26 ORGANIZERS

Conference Chairs:
Wolfgang Ahrendt Chalmers University of Technology
Moa Johansson Chalmers University of Technology

Program Committee Chair:
Leonardo de Moura Microsoft Research

Workshop, Tutorial, and Competition Chair:
Philipp Ruemmer Uppsala University

Publicity Chair:
Magnus Myreen Chalmers University of Technology

Program Committee:

Clark Barrett Stanford University
Christoph Benzmueller Freie Universitaet Berlin
Jasmin Christian Blanchette Inria Nancy & LORIA
Nikolaj Bjorner Microsoft Research
Maria Paola Bonacina Universita degli Studi di Verona
Leonardo de Moura Microsoft Research
Hans de Nivelle University of Wroclaw
Stephanie Delaune CNRS, IRISA
Gilles Dowek Inria & ENS Paris-Saclay
Amy Felty University of Ottawa
Silvio Ghilardi Universita degli Studi di Milano
Reiner Haehnle Technical University of Darmstadt
Marijn Heule The University of Texas at Austin
Moa Johansson Chalmers University of Technology
Dejan Jovanovic SRI International
Deepak Kapur University of New Mexico
Konstantin Korovin The Manchester University
Laura Kovacs Vienna University of Technology
Christopher Lynch Clarkson University
Assia Mahboubi INRIA
Aart Middeldorp University of Innsbruck
Dale Miller INRIA and LIX/Ecole Polytechnique
Albert Oliveras Technical University of Catalonia
Lawrence Paulson University of Cambridge
Ruzica Piskac Yale University
Philipp Ruemmer Uppsala University
Renate Schmidt The University of Manchester
Stephan Schulz DHBW Stuttgart
Roberto Sebastiani University of Trento
Viorica Sofronie-Stokkermans University Koblenz-Landau
Geoff Sutcliffe University of Miami
Cesare Tinelli The University of Iowa
Ashish Tiwari SRI International
Andrei Voronkov The University of Manchester
Christoph Weidenbach Max Planck Institute for Informatics
Freek Wiedijk Radboud University Nijmegen

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

2017-01-10

[Caml-list] LPAR-21 extended deadlines

****************************************************************************
EXTENDED DEADLINES!! EXTENDED DEADLINES!!

The 21st International Conference on
Logic for Programming, Artificial Intelligence and Reasoning
LPAR-21

Cresta Riley's Hotel, Maun, Botswana
http://www.LPAR-21.info

CALL FOR PAPERS

The series of International Conferences on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR) is a forum where, year after year, some of
the most renowned researchers in the areas of logic, automated reasoning,
computational logic, programming languages and their applications come to
present cutting-edge results, to discuss advances in these fields, and to
exchange ideas in a scientifically emerging part of the world. The 21st LPAR
will be held will be held in Maun, Botswana, at Cresta Riley's Hotel, 7-12th
May 2017. The proceedings will be published by EasyChair Publications, in the
EPiC Series in Computing. The volume will be open access and the authors will
retain copyright.

==Important Dates

Abstract submission: 18 January 2017
Paper submission: 22 January 2017
Notification: 1 March 2017
Camera ready: 1 April 2017
Workshops: 7 May 2017
Conference: 8-12 May 2017

==Topics

New results in the fields of computational logic and applications are welcome.
Also welcome are more exploratory presentations, which may examine open
questions and raise fundamental concerns about existing theories and practices.

Topics of interest include, but are not limited to:

+ Abduction and interpolation methods
+ Answer set programming
+ Automated reasoning
+ Constraint programming
+ Contextual reasoning
+ Decision procedures
+ Description logics
+ Foundations of security
+ Hardware verification
+ Implementations of logic
+ Inconsistency- and exception tolerant reasoning
+ Interactive theorem proving
+ Knowledge representation and reasoning
+ Logic and computational complexity
+ Logic and databases
+ Logic and games
+ Logic and machine learning
+ Logic and the web
+ Logic and types
+ Logic in artificial intelligence
+ Logic of distributed systems
+ Logic of knowledge and belief
+ Logic programming
+ Logical aspects of concurrency
+ Logical foundations of programming
+ Modal and temporal logics
+ Model checking
+ Non-monotonic reasoning
+ Ontologies and large knowledge bases
+ Paraconsistent logics
+ Probabilistic and fuzzy reasoning
+ Program analysis
+ Rewriting
+ Satisfiability checking
+ Satisfiability modulo theories
+ Software verification
+ Specification using logic
+ Unification theory

==Organization

Program Chairs:
David Sands (Chalmers University of Technology, Sweden)
Thomas Eiter (Technische Universitaet Wien, Austria)
Conference Chair:
Geoff Sutcliffe (University of Miami, USA)

==Submission Details

Submissions of two kinds are welcome:

- Regular papers that describe solid new research results. They can be
up to 15 pages long in EasyChair style, including figures but excluding
references and appendices (that reviewers are not required to read).

- Experimental and tool papers that describe implementations of
systems, report experiments with implemented systems, or compare
implemented systems. They can be up to 8 pages long in the EasyChair
style.

Both types of papers must be electronically submitted in PDF via EasyChair:

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

Authors must register a title and an abstract by the abstract submission
deadline.

==Participation

Authors of accepted papers are required to ensure that at least one of
them will be present at the conference.

For more details about the venue and organization, see the conference
webpage http://www.LPAR-21.info

****************************************************************************

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs