# Association for Automated Reasoning

March 2017

## From the AAR President, Larry Wos

Tarskian geometry comes into play again, especially because it offers obstacles quite different from other areas of mathematics and logic. Not too long ago, from this area, I offered, as a challenge, the proving of a theorem, Satz 3.17, without the use of any diagram. In this column, I offer a related, but far greater challenge, that of proving Satz 4.14, again without the use of a diagram. (The symbol "|" denotes logical or, and the symbol "-" denotes logical not.)

%  following is Satz 4.14
-Col(xa,xb,xc) | -E(xa,xb,xa1,xb1)
| E3(xa,xb,xc,xa1,xb1,insert5(xa,xb,xc,xa1,xb1)).

Satz 4.14 may prove challenging even if you include a diagram, and you might enjoy trying to meet that challenge.

As before, I also offer you some Tarskian geometry axioms, followed by some theorems and possible definitions. As to which of the axioms and which of the theorems and definitions will prove useful, I leave to you to discover.

%  Some axioms for Tarskian geometry
E(x,y,y,x).
-E(x,y,z,v) | -E(x,y,z2,v2) | E(z,v,z2,v2).
-E(x,y,z,z) | x=y.
T(x,y,ext(x,y,w,v)).
E(y,ext(x,y,w,v),w,v).
-E(x,y,x1,y1) | -E(y,z,y1,z1) | -E(x,v,x1,v1) | -E(y,v,y1,v1) | -T(x,y,z)
|  -T(x1,y1,z1) | x=y | E(z,v,z1,v1).
-T(x,y,x) | x=y.
-T(xa,xp,xc) | -T(xb,xq,xc) | T(xp,ip(xa,xp,xc,xb,xq),xb).
-T(xa,xp,xc) | -T(xb,xq,xc) | T(xq,ip(xa,xp,xc,xb,xq),xa).
-T(alpha,beta,gamma).
-T(beta,gamma,alpha).
-T(gamma,alpha,beta).

%  Theorems and definitions
%  following is Satz 2.1
E(xa,xb,xa,xb).
%  following is Satz 2.2
-E(xa,xb,xc,xd) | E(xc,xd,xa,xb).
%  following is Satz 2.3
-E(xa,xb,xc,xd) | -E(xc,xd,xe,xf) | E(xa,xb,xe,xf).
%  following is Satz 2.4
-E(xa,xb,xc,xd) | E(xb,xa,xc,xd).
%  following is Satz 2.5
-E(xa,xb,xc,xd) | E(xa,xb,xd,xc).
%  following is Satz 2.8
E(xa,xa,xb,xb).
%  following is Satz 2.11
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1)
|  E(xa,xc,xa1,xc1).
%  following is Satz 2.12
xq = xa | -T(xq,xa,xd) | -E(xa,xd,xb,xc) | xd = ext(xq,xa,xb,xc).
%  following is Satz 2.13
-E(xb,xc,xa,xa) | xb=xc.
%  following is Satz 2.14
-E(xa,xb,xc,xd) | E(xb,xa,xd,xc).
%  following is Satz 2.15
-T(xa,xb,xc) | -T(xA,xB,xC) | -E(xa,xb,xB,xC)| -E(xb,xc,xA,xB)
|  E(xa,xc,xA,xC).
% Following is Satz 3.1
T(xa,xb,xb).
% Following is Satz 3.2
-T(xa,xb,xc) | T(xc,xb,xa).
% Following is Satz 3.3
T(xa1,xa1,xb1).
% Following is Satz 3.4
-T(xa,xb,xc) | -T(xb,xa,xc) | xa = xb.
% Following is Satz 3.5a
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xb,xc).
% Following is Satz 3.6a
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xb,xc,xd).
% Following is Satz 3.7a
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xc,xd).
% Following is Satz 3.5b
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xc,xd).
% Following is Satz 3.6b
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd).
% Following is Satz 3.7b
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xb,xd).
% Following is Satz 3.13a
alpha != beta.
% Following is Satz 3.13b
beta != gamma.
% Following is Satz 3.13a
alpha != gamma.
% Following is Satz 3.14a
T(xa,xb,ext(xa,xb,alpha,gamma)).
% Following is Satz 3.14b
xb != ext(xa,xb,alpha,gamma).
% Following is Satz 3.17
-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1)
|  T(xp,crossbar(xa,xb,xc,xa1,xb1,xp),xc).
-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1)
|  T(xb,crossbar(xa,xb,xc,xa1,xb1,xp),xb1).
% Following is Satz 4.2
-IFS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1).
% Following is Satz 4.3
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xc,xa1,xc1) | -E(xb,xc,xb1,xc1)
|  E(xa,xb,xa1,xb1).
% Following is Satz 4.5
-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) | T(xa1,insert(xa,xb,xa1,xc1),xc1).
-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) |
E3(xa,xb,xc,xa1,insert(xa,xb,xa1,xc1),xc1).
% Following is Satz 4.6
-T(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | T(xa1,xb1,xc1).
% Following is Satz 4.11a
-Col(xa,xb,xc) | Col(xb,xc,xa).
% Following is Satz 4.11b
-Col(xa,xb,xc) | Col(xc,xa,xb).
% Following is Satz 4.11c
-Col(xa,xb,xc) | Col(xc,xb,xa).
% Following is Satz 4.11d
-Col(xa,xb,xc) | Col(xb,xa,xc).
% Following is Satz 4.11e
-Col(xa,xb,xc) | Col(xa,xc,xb).
% Following is Satz 4.12
Col(xa,xa,xb).
% Following is Satz 4.12b
Col(xa,xb,xa).
% Following is Satz 4.13
-Col(xa,xb,xc) | - E3(xa,xb,xc,xa1,xb1,xc1) | Col(xa1,xb1,xc1).
%  definition of the function insert
insert(xa,xb,xa1,xc1) = ext(ext(xc1,xa1,alpha,gamma),xa1,xa,xb).
%  definition 2.10
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xb,za,zb).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xd,zb,zd).
-T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xb,za,zb) | -E(xb,xc,zb,zc)
|  -E(xa,xd,za,zd) | -E(xb,xd,zb,zd)| AFS(xa,xb,xc,xd,za,zb,zc,zd).
%  definition 4.1
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xc,za,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xc,xd,zc,zd).
-T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xc,za,zc) | -E(xb,xc,zb,zc)
|  -E(xa,xd,za,zd) | -E(xc,xd,zc,zd)| IFS(xa,xb,xc,xd,za,zb,zc,zd).
%  definition 4.4
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa2,xb1,xb2).
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa3,xb1,xb3).
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa2,xa3,xb2,xb3).
-E(xa1,xa2,xb1,xb2) | -E(xa1,xa3,xb1,xb3) | -E(xa2,xa3,xb2,xb3)
|  E3(xa1,xa2,xa3,xb1,xb2,xb3).
%  definition 4.10
-Col(xa,xb,xc) | T(xa,xb,xc) | T(xb,xc,xa) | T(xc,xa,xb).
Col(xa,xb,xc) | -T(xa,xb,xc).
Col(xa,xb,xc) | -T(xb,xc,xa).
Col(xa,xb,xc) | -T(xc,xa,xb).
%  definition 4.15
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | Col(xa,xb,xc).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E3(xa,xb,xc,xa1,xb1,xc1).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xa,xd,xa1,xd1).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1).
-Col(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | -E(xa,xd,xa1,xd1)
|  -E(xb,xd,xb1,xd1) | FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1).

By the length of this column, when compared with the earlier column focusing on Satz 3.17, you would assume (correctly) that 4.14 is far more difficult to prove, especially without a diagram. Again, I suggest that if you intend to form an approach, you might begin with attempts to prove various cited theorems.

## Herbrand Award: Call for Nominations

Martin Giese
On behalf of the CADE Inc. Board of Trustees

The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

• Larry Wos (1992)
• Woody Bledsoe (1994)
• Alan Robinson (1996)
• Wu Wen-Tsun (1997)
• Gerard Huet (1998)
• Robert S. Boyer and J Strother Moore (1999)
• William W. McCune (2000)
• Donald W. Loveland (2001)
• Mark E. Stickel (2002)
• Peter B. Andrews (2003)
• Harald Ganzinger (2004)
• Martin Davis (2005)
• Wolfgang Bibel (2006)
• Alan Bundy (2007)
• Edmund Clarke (2008)
• Deepak Kapur (2009)
• David Plaisted (2010)
• Nachum Dershowitz (2011)
• Melvin Fitting (2012)
• Greg Nelson (2013)
• Robert L. Constable (2014)
• Andrei Voronkov (2015)
• Zohar Manna and Richard Waldinger (2016)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE-26 is

15 April 2017

Nominations pending from previous years must be resubmitted in order to be considered.

Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to

Christoph Weidenbach, President of CADE Inc.
weidenbach (at) mpi-inf.mpg.de

with copies to

Martin Giese, Secretary of CADE Inc. and AAR
martingi (at) ifi.uio.no

## Woody Bledsoe Student Travel Awards at CADE 2017

The Woody Bledsoe Student Travel Award was created to honour the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.

The winners of the CADE 2017 Woody Bledsoe Student Travel Award will be partially reimbursed (up to value 750 EUR) for their conference registration, transportation, and accommodation expenses.

A nomination consists of a recommendation letter of up to 300 words from the student's advisor. Nominations for CADE 2017 should be sent by e-mail to the Program Committee Chair Leonardo de Moura, and at the same time to Martin Giese, Secretary of CADE Inc. and AAR.

Nominations must arrive no later than May 12, 2017. The winners will be notified by May 26, 2017.

The awards will be presented at CADE 2017; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.

## Ackermann Award 2017 - The EACSL Outstanding Dissertation Award For Logic In Computer Science, Call For Nominations

Nominations are now invited for the 2017 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1.1.2015 and 31.12.2016 are eligible for nomination for the award. The deadline for submission is 1 April 2017. Submission details follow below. Nominations can be submitted from 1 January 2017 and should be sent to the chair of the Jury, Anuj Dawar, by e-mail.

The Award
The 2017 Ackermann Award will be presented to the recipient(s) at the annual conference of the EACSL, 20-24 August 2017, in Stockholm (Sweden). The award consists of

• a certificate,
• an invitation to present the thesis at the CSL/LICS conference,
• the publication of the laudatio in the CSL/LICS proceedings, and
• travel support to attend the conference.

The jury is entitled to give the award to more (or less) than one dissertation in a year.

Jury
The jury consists of:

• Anuj Dawar (University of Cambridge), the president of EACSL;
• Dale Miller (INRIA and Ecole Polytechnique), ACM SigLog representative;
• Orna Kupferman (Hebrew University of Jerusalem);
• Daniel Leivant (Indiana University, Bloomington);
• Luke Ong (University of Oxford);
• Jean-Eric Pin (CNRS and University of Paris 7);
• Simona Ronchi Della Rocca (University of Torino), the vice-president of EACSL;
• Thomas Schwentick (TU Dortmund).

How to submit
The candidate or his/her supervisor should submit

1. the thesis (ps or pdf file);
2. a detailed description (not longer than 20 pages) of the thesis
3. ENGLISH (ps or pdf file);
4. a supporting letter by the PhD advisor and two supporting letters by other senior researchers (in English); supporting letters can also be sent directly to Anuj Dawar;
5. a short CV of the candidate;
6. a copy of the document asserting that the thesis was accepted as a PhD thesis at a recognized University (or equivalent institution) and that the candidate has received his/her PhD within the specified period.

The submission should be sent by e-mail as attachments to the chairman of the jury, Anuj Dawar with the following subject line and text:

• Subject: Ackermann Award Submission
• Text: Name of candidate, list of attachments

Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text. Letters of support and documents can also be faxed to:
Anuj Dawar
Ackermann Award
+44 1223 334678

The Jury has the right to declare submissions to be out of scope or not to meet the requirements.

## Special Issues

### Journal of Automated Reasoning: Special Issue on Milestones in Interactive Theorem Proving, call for papers

Larry Paulson, Jeremy Avigad, Gerwin Klein  (guest editors)

The past few decades have seen major achievements in interactive theorem proving, such as the formalisation of deep mathematical theorems and significant bodies of theoretical computer science, as well as the verification of complex software and hardware systems. Too often, these impressive results have been published in abbreviated or fragmentary form in conference proceedings, or not at all. This special issue welcomes full-length papers describing past work not previously published in a journal, along with new developments of any length. Small, self-contained Proof Pearls and applications of all kinds are also welcome.

This special issue will be devoted to applications of interactive theorem proving in their full variety: formalised mathematics, formalised theory, formalised semantics, formal proofs of hardware or software systems. They can be large or small.

Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.

Important Dates
1 Oct 2017 Notification of accepted papers
1 Jan 2018 Final version

### Journal of Automated Reasoning: Special Issue on Automated Reasoning Systems, call for papers

Armin Biere, Cesare Tinelli, Christoph Weidenbach  (guest editors)

Important Dates

• 3 Apr 2017: Submission deadline
• 1 Nov 2017: Notification of acceptance/rejection
• 1 Mar 2018: Final version

The past few decades have seen major developments and practical achievements in automated reasoning systems. For example, SAT solving has become an inherent part of the standard hardware production process; SMT solvers are now the backbone of most software verification techniques; first-order theorem provers have pushed the productivity of interactive theorem proving to a new level; computer algebra systems have solved difficult problems in mathematics and biology; knowledge representation systems have become indispensable for reasoning in the world wide web; automatic termination checkers routinely prove the termination of complex programs.

This special issue is dedicated to automated reasoning systems in their full variety along the following dimensions:

• considered logic: propositional (including (D)QBF), first-order modulo theories, modal, temporal, decidable fragments of larger logics, FOL, and HOL, ...;
• considered problem: satisfiability, interpolation, quantifier elimination, consequence finding, model building, reachability, termination, ...;
• application area: formal methods, artificial intelligence, mathematics, biology, product development, security, ...;
• user base: academic, educational, or industrial.
In particular, we welcome papers emphasizing engineering aspects because, while often crucial for the success of automated reasoning tools, they are typically not given a sufficiently detailed treatment in theory papers or system description papers published at conferences or workshops.

We welcome full-length papers describing past work not previously published in a journal as well as papers of any length describing new developments. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are also eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.

We encourage submissions that include most, if not all, of the following:

• theory details,
• implementation details,
• applications, and
• experiments.

### Annals of Mathematics and Artificial Intelligence: Special Issue on Formalization of Geometry, Automated and Interactive Geometric Reasoning, call for papers

Pascal Schreck, Tetsuo Ida, Laura Kovacs

For this special issue of AMAI, we are seeking original contributions on various aspects of formalization of geometry having in view computational applications mainly oriented to proof but also to modeling in geometry. Relevant topics include (but are not limited to):

• Polynomial algebra, invariant and coordinate-free methods, probabilistic, synthetic, and logical approaches, techniques for automated geometric reasoning from discrete mathematics, combinatorics, and numerics;
• Symbolic and numeric methods for geometric computation, geometric constraint solving, automated generation/reasoning and manipulation with diagrams;
• Design and implementation of geometry software, special-purpose tools, automated theorem provers, experimental studies;
• Applications of formalization of geometry to mechanics, geometric modeling, CAGD/CAD, computer vision, robotics, and education.

Important dates:

• September 1, 2017: paper submission -- via website: www.editorialmanager.com/amai/ selecting issue: S688 Formalization of Geometry and Reasoning
• January 1, 2018: author notification
• March 1, 2018: revisions and camera-ready paper submission

## Conferences

### MFPS 23: Mathematical Foundations of Programming Semantics, call for papers

The 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII) will take place on the campus of Ljubljana University, Slovenia, between 12 and 15 June 2017. MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.

Topics include, but are not limited to, the following:

bio-computation; concurrent qualitative and quantitative distributed systems; process calculi; probabilistic systems; constructive mathematics; domain theory and categorical models; formal languages; formal methods; game semantics; lambda calculus; programming-language theory; quantum computation; security; topological models; logic; type systems; type theory.
We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example.

### TbiLLC 2017: Twelfth International Tbilisi Symposium on Language, Logic and Computation, call for papers

18-22 September, 2017, Kakheti, Georgia

The Programme Committee invites submissions for contributions on all aspects of language, logic and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:

• Natural language syntax, semantics, and pragmatics
• Linguistic typology and semantic universals
• Language evolution and learnability
• Historical linguistics, history of logic
• Natural logic, inference and entailment in natural language
• Logic, games, and formal pragmatics
• Logics for artificial intelligence
• Constructive, modal and algebraic logic
• Algorithmic game theory
• Computational social choice
• Formal models of multiagent systems
• Information retrieval, query answer systems
• Distributional and probabilistic models of information and meaning

Authors can submit an abstract of three pages (including references) at the EasyChair conference system.

The programme, including lectures and tutorials can be found on the TbiLLC website.

Important Dates

• Submission deadline: 15 March 2017
• Final abstracts due: 15 June 2017
• Registration deadline: 1 August 2017
• Symposium: September 18-22, 2017

Workshops
There will also be a workshop on "Language entitled Signs and gestures -- exploring the divide between sign language and speech-accompanying gestures". More information will be available on the TbiLLC website.

### iFM 2017: 13th Intl. Conference on integrated Formal Methods, call for papers

20-22 September 2017, Turin, Italy

Important dates

• Abstract submission: Tuesday March 28
• Paper submission: Tuesday April 4
• 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.
More details about the submission process are available from the conference website.

Invited Speakers

• Jane Hillston (University of Edinburgh, UK)
• André Platzer (CMU, USA)
• Matrin Vechev (ETH Zürich, 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.

### CALCO 2017: 7th International Conference on Algebra and Coalgebra in Computer Science, call for papers

June 13 - 16, 2017, Ljubljana, Slovenia
Scope
CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science.

It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011), Warsaw (Poland, 2013) and Nijmegen (the Netherlands, 2015).

The seventh edition will be held in Ljubljana, Slovenia, colocated with MFPS XXXIII.

See the conference website for the topics of interest and submission guidelines.

Invited Speakers

• Nicoletta Sabadini - University of Insubria, IT
• Alex Simpson - University of Ljubljana, SL
• James Worrell - University of Oxford, UK (joint with MFPS)
• Catuscia Palamidessi - Ecole polytechnique, FR (joint with MFPS)
• Vincent Danos - Ecole normale superieure, FR (joint with MFPS)
• Marco Gaboardi - University at Buffalo, USA (joint with MFPS)

Special Session On Metrics, Privacy And Learning (joint event with MFPS)

Best Paper And Best Presentation Awards
This edition of CALCO will feature two awards: a Best Paper Award whose recipients will be selected by the PC before the conference and a Best Presentation Award, elected by the participants.

Important dates:

• Abstract submission: April 3, 2017
• Paper submission: April 7, 2017
• Author notification: May 15, 2017
• Final version due: May 31, 2017

Satellite Workshops: Calco Early Ideas And Calco Tools
The CALCO Early Ideas Workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute.

The CALCO Tools Workshop is dedicated to tools based on algebraic and/or coalgebraic principles.

CALCO 2017 will run together with the CALCO Early Ideas Workshop, with dedicated sessions at the end of each conference day. CALCO Tools will take place on June 13.

### MFCS 2017: 42nd International Symposium on Mathematical Foundations of Computer Science, call for papers

August 21-25, 2017, Aalborg, Denmark

Background:
MFCS conference series is organized since 1972. Traditionally, the conference moved between the Czech Republic, Slovakia, and Poland, while since a few years ago, the conference travels around Europe (in 2013 it was held in Austria, then in 2014 in Hungary, in 2015, in Italy). In 2016 the conference returned to Poland and in 2017 it will be held in Denmark. MFCS is a high-quality venue for original research in all branches of theoretical computer science. The broad scope of the conference encourages interactions between researchers who might not meet at more specialized venues. MFCS 2017 consists of invited lectures and contributed talks, selected by an international program committee of researchers focusing on diverse areas of theoretical computer science. The conference will be accompanied by workshops.

We encourage submission of original research papers in all areas of theoretical computer science, including (but not limited to) the following (alphabetically ordered):

• algebraic and co-algebraic methods in computer science
• algorithms and data structures
• automata and formal languages
• bioinformatics
• combinatorics on words, trees, and other structures
• computational complexity (structural and model-related)
• computational geometry
• computer-assisted reasoning
• concurrency theory
• cryptography and security
• databases and knowledge-based systems
• formal specifications and program development
• foundations of computing
• logics in computer science
• mobile computing
• models of computation
• networks (incl. wireless, sensor, ad-hoc networks)
• parallel and distributed computing
• quantum computing
• semantics and verification of programs
• theoretical issues in artificial intelligence
• types in computer science

All submitted papers will be reviewed by the program committee. Accepted papers will be collected into the conference proceedings.

Important Dates:
Abstract submission deadline: April 20th, 2017 (AoE)
Paper submission deadline: April 24th, 2017 (AoE)
Notification of authors: June 12th, 2017 (AoE)
Camera-ready copies due: June 22nd, 2017 (AoE)
Early registration deadline: June 23rd, 2017 (AoE)
Late registration deadline: August 7th, 2017 (AoE; afterward, only on-site registration)
Conference dates: August 21-25, 2017

Paper Submission:
Papers should be submitted electronically through EasyChair.

Submissions should be prepared using the LIPIcs style and have a length of up to 12 pages (excluding references and an optional appendix). Further details are available on the conference website.

### RV2017: The 17th International Conference on Runtime Verification, call for papers and tutorials

September 13-16, 2017, Seattle, WA, USA

Runtime verification is concerned with the monitoring and analysis of the runtime behaviour of software and hardware systems. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they provide an additional level of rigor and effectiveness compared to conventional testing, and are generally more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair.

Topics of interest to the conference include, but are not limited to:

• specification languages
• monitor construction techniques
• program instrumentation
• logging, recording, and replay
• combination of static and dynamic analysis
• specification mining and machine learning over runtime traces
• monitoring techniques for concurrent and distributed systems
• runtime checking of privacy and security policies
• statistical model checking
• metrics and statistical information gathering
• program/system execution visualization
• fault localization, containment, recovery and repair
• integrated vehicle health management (IVHM)

Application areas of runtime verification include cyber-physical systems, safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.

We welcome contributions exploring the combination of runtime verification techniques with machine learning and static analysis. Whilst these are highlight topics, papers falling into these categories will not be treated differently from other contributions.

An overview of previous RV conferences and earlier workshops can be found at: http://www.runtime-verification.org.

Important Dates
Papers as well as tutorial proposals will follow the following timeline:

• Abstract deadline: April 24, 2017 (Anywhere on Earth)
• Paper and tutorial deadline: May 1, 2017 (Anywhere on Earth)
• Tutorial notification: May 21, 2017
• Paper notification: June 26, 2017
• Conference: September 13-16, 2017

General Information on Submissions
All papers and tutorials will appear in the conference proceedings in an LNCS volume. Detailed information is available at the conference website.

Paper Submissions
There are three categories of papers which can be submitted: regular, short or tool papers. Papers in each category will be reviewed by at least 3 members of the Program Committee.

• Regular Papers (up to 15 pages, not including references) should present original unpublished results. We welcome theoretical papers, system papers, papers describing domain-specific variants of RV, and case studies on runtime verification.
• Short Papers (up to 6 pages, not including references) may present novel but not necessarily thoroughly worked out ideas, for example emerging runtime verification techniques and applications, or techniques and applications that establish relationships between runtime verification and other domains.
• Tool Demonstration Papers (up to 8 pages, not including references) should present a new tool, a new tool component, or novel extensions to existing tools supporting runtime verification. The paper must include information on tool availability, maturity, selected experimental results and it should provide a link to a website containing the theoretical background and user guide. Furthermore, we strongly encourage authors to make their tools and benchmarks available with their submission.
The Program Committee of RV 2017 will give a best paper award, and a selection of accepted regular papers will be invited to appear in a special issue of the Springer Journal on Formal Methods in System Design.

Tutorial Submissions
Tutorials are two-to-three-hour presentations on a selected topic. Additionally, tutorial presenters will be offered to publish a paper of up to 20 pages in the LNCS conference proceedings, not including references.

A proposal for a tutorial must contain the subject of the tutorial, a proposed timeline, a note on previous similar tutorials (if applicable) and the differences to this incarnation, and a brief biography of the presenter. The proposal should not exceed 2 pages.

### SAT 2017: 20th International Conference on Theory and Applications of Satisfiability Testing

August 28 to September 1, 2017, Melbourne, Australia

The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. In addition to plain propositional satisfiability, it also includes Boolean optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning. Topics include, but are not restricted to:

• Theoretical advances (including algorithms, proof complexity, parameterized complexity, and other complexity issues);
• Practical search algorithms;
• Knowledge compilation;
• Implementation-level details of SAT solving tools and SAT-based systems;
• Problem encodings and reformulations;
• Applications (including both novel applications domains and improvements to existing approaches);
• Case studies and reports on insightful findings based on rigorous experimentation.

SAT 2017 will take place in Melbourne, Australia alongside CP 2017 and ICLP 2017 from August 28th to September 1st, 2017 which is the week immediately following IJCAI 2017.

Important Dates

• Abstract submission: 26 Apr 2017
• Paper submission: 2 May 2017
• Author response period: 29-31 May 2017
• Camera ready: 28 Jun 2017

### ILP 2017: 27th International Conference on Inductive Logic Programming, call for papers

September 4th - 6th 2017, Orléans, France

Authors are invited to submit papers presenting original results on all aspects of learning in logic, multi-relational learning and data mining, statistical relational learning, graph and tree mining, relational reinforcement learning, connections with other learning paradigms, and learning in other logic-based knowledge representation frameworks.

Typical, but not exclusive, topics of interest for submissions include:

• Theoretical aspects: logical foundations, probabilistic logic-based learning, computational and/or statistical learning theories, theories on abduction, data/model representation,
• Representations and languages for logic-based learning: subsets of first-order logic (datalog, description logics for instance), higher-order logic, probabilistic logical representations, links between alternative representations.
• Algorithms and systems:
• supervised/unsupervised/semi-supervised relational learning, relational reinforcement learning, abductive learning, inductive databases
• learning from structured data (e.g., labeled graphs, tree patterns) and semi-structured data (e.g., XML documents),
• logical, probabilistic and statistical approaches ; distance and kernel-based methods; propositionalization; predicate invention;
• systems that implement inductive logic programming algorithms with special emphasis on issues like efficiency and scalability.
• Applications of ILP:
• - bioinformatics, cheminformatics, medical informatics, robotics, engineering
• - natural language processing: computational linguistics, text/web mining
• - social science, art and humanities, games, social networks

We solicit three kinds of papers:

1. Regular papers describing original mature work representing a self-contained theoretical contribution and/or containing appropriate experimental evaluation. These papers will be reviewed by at least 3 members of the program committee. Each accepted paper will be given a standard time slot for presentation and will be invited to submit a final version to the Springer LNAI post-conference proceedings without further reviews.
In case the paper is not accepted as a long paper, it may be accepted as a work-in-progress paper, in which case it will be assigned a reduced time slot for presentation, and the authors have the opportunity to submit a revised version that will be reviewed after the conference for possible inclusion in the Springer LNAI post-conference proceedings.
Long papers must not exceed 12 pages (including references).
2. Late-breaking papers describing original work in progress, brief accounts of original ideas without conclusive experimental evaluation, and other relevant work of potentially high scientific interest but not yet qualifying for the long paper category. Late-breaking papers will be accepted/rejected by PC chairs on the grounds of relevance. Authors of accepted late-breaking papers will be assigned a reduced time slot for presentation.
Each late-breaking paper will then be reviewed by at least 3 members of the program committee taking also into account the oral presentation. Based on these reviews, the authors may be given the opportunity to submit a long version for the Springer LNAI post-conference proceedings. In this case, the long paper will be reviewed again by the assigned PC members of the short paper and be finally accepted if satisfactorily addressing the reviewer's requirements.
Late-breaking papers must not exceed 6 pages (including references).
3. Papers relevant to the conference topics and recently published or accepted for publication by a first-class conference such as ECML/ PKDD, ICML, KDD, ICDM, AAAI, IJCAI, etc. or journal such as MLJ, DMKD, JMLR etc. The PC chairs will accept/reject such papers on the grounds of relevance and quality of the original publication venue. Authors of accepted papers will be assigned a reduced time slot for presentation. These papers will not appear in the Springer LNAI post-conference proceedings.

Submission:
All Paper submissions will be electronic through the ILP 2017 easychair site. More information is available on the conference website.

A special issue of a journal is planned following the conference. It will be opened to everyone. This special issue welcomes conference submissions from all the three categories above, which should be significantly revised and extended to meet the journal criteria. They will be reviewed by the Program Committee.

Dates
Abstract registration (long paper): 28 April 2017
Long paper submission: 5 May 2017
Long paper notification: 9 June 2017
Late breaking and previously published paper submission: 28 June 2017
Late breaking and previously published paper notification: 3 July 2017

September 12 to 15, 2017, Lublin, Poland

It is organized by the Department of the Foundations of Computer Science at the Faculty of Philosophy of the John Paul II Catholic University of Lublin, in co-operation with the journal Studia Logica (see http://www.studialogica.org and http://link.springer.com/journal/11225).

We call for relevant contributions applying the different approaches to:

• deontic logic,
• normative aspects of action theory,
• formal ethics,
• legal theory,
• handling norms in computer systems.

A special session on obligations derived from permissions, related to the a special issue of Studia Logica, will be a part of the conference.

Invited Speakers

• Jan Broersen
• Fenrong Liu
• Paul McNamara
• Olivier Roy
• Marek Sergot
• Jan Wolenski

Paper Submission
Extended abstracts of a length between 1 and 3 pages (including references), should be submitted via EasyChair (https://easychair.org/conferences/?conf=trends2017). More information about the submission process is available on the conference website.

Publication
Authors are encouraged to submit papers presented at Trends in Logic XVII to Studia Logica journal, where they will be a subject of full reviewing process.

Important Dates
Deadline for submissions: May 31th, 2017
Notification of acceptance: June 30th, 2017
Deadline for early registration: July 31th, 2017
Conference: September 12th-15th, 2017

### MEMOCODE 2017: 15th ACM/IEEE International Conference on Formal Methods and Models for System Design, call for papers

September 29 - October 2, 2017, Vienna, Austria

MEMOCODE's objective is to bring together researchers and practitioners interested in formal methods and models for system design and development to exchange ideas, research results, and lessons learned. System design covers the development of hardware, firmware, middleware, and application software for systems ranging from single embedded devices to highly networked CPS and systems in the IoT. In particular, MEMOCODE 2017 seeks research contributions on formal foundations, engineering methods, tools, and experimental case studies. Research areas of interest include, but are not limited to the following:

• Modeling Languages, Methods and Tools
• Formal Methods and Tools
• Models and Methods for Developing Critical Systems
• Quantitative/Qualitative Reasoning
• Formal Methods/Models in Practice

Important Dates

• Submission deadline (abstract): May 12, 2017
• Submission deadline (paper): May 19, 2017
• Notification of acceptance: July 10, 2017
• Final version of papers: July 28, 2017

For submission details and other information, see the conference website.

### FMCAD 2017: Formal Methods in Computer-Aided Design, call for papers

October 2-6, 2017, Vienna, Austria

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, connectivity and security properties of networks and distributed systems.

Important Dates (all deadlines are 11:59 pm anywhere on earth)

• 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
• 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
For submission details and other information, see the conference website.

### TABLEAUX/FroCoS/ITP, call for posters

25-29 September 2017, Brasilia Brazil

TABLEAUX/FroCoS/ITP 2017 will have a poster session, which is intended for descriptions of works in progress, student projects and relevant research being published elsewhere.

Submissions should be in English, in the form of at most one page abstract, ENTCS format containing title and authors name with affiliation. The files should be sent directly to Elaine Pimentel.

The deadline for posters submission is June 15, 2017. The notification will be sent to authors June 30th.

Proceedings of this session will not be published. Formatting instructions for posters will be made available soon.

## Workshops

### IWIL 2017: 12th International Workshop on the Implementation of Logics, call for papers

7th May 2017, Maun, Botswana

IWIL 2017 will be held in conjunction with the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning

We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to:

• Propositional logic and decision procedures, including SMT
• First-order and higher order logics
• Non-classical logics, including modal, temporal, description, non-monotonic reasoning
• Formal foundations for efficient implementation of logics
• Data structures and algorithms for the efficient representation and processing of logical concepts
• Proof/model search organization and heuristics for logical reasoning systems
• Data analysis and machine learning approaches to search control
• Techniques for proof/model search visualization and analysis
• Reasoning with ontologies and other large theories
• Implementation of efficient theorem provers and model finders for different logics
• System descriptions of logical reasoning systems
• Issues of reliability, witness generation, and witness verification
• Evaluation and benchmarking of provers and other logic-based systems
• I/O standards and communication between reasoning systems

We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice.

Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL-2017.

Details about the submission process can be found on the workshop's website.

Important Dates:

• Submission of papers/abstracts: March 20th, 2017
• Notification of acceptance: April 10th, 2017
• Camera ready versions due: April 21st, 2017
• Workshop: May 7th, 2017

### AFM: Automated Formal Methods 2017, call for papers

May 19, 2017, NASA Ames Research Center, Moffett Field, CA, USA

In association with 9th NASA Formal Methods Symposium (NFM) 2017

AFM is a one-day workshop centered around the use and integration of highly automated formal verification tools for specification, interactive theorem proving, satisfiability (SAT) and satisfiability modulo theories (SMT), model checking, program verification, static analysis, runtime verification, code generation, and testing, as well as interfaces, documentation, and education. AFM functions both as a user's meeting for SRI's tools such as PVS, SAL and Yices, and as a workshop for those interested in state of the art automation for formal methods generally.

Paper deadline: March 27, 2017. See the workshop web site for details.

### WiL 2017: Women in Logic Workshop

June 19 2017, Reykjavik, Iceland

We are holding the first Women in Logic (WiL) workshop as a LICS associated workshop this year. The workshop intends to follow the pattern of meetings such as Women in Machine Learning (WiML, http://wimlworkshop.org/) or Women in Engineering (WIE, (http://www.ieee-ras.org/membership/women-in-engineering) that have been taking place for quite a few years. Women are chronically underrepresented in the LICS community; consequently they sometimes feel both conspicuous and isolated, and hence there is a risk that the under-representation is self-perpetuating.

The workshop will provide an opportunity for women in the field to increase awareness of one another and one another's work, to combat the feeling of isolation. It will also provide an environment where women can present to an audience comprised of mostly women, replicating the experience that most men have at most LICS meetings; we hope that this will be particularly attractive to early-career women.

Topics of interest of this workshop include but are not limited to the usual Logic in Computer Science (LICS) topics. These are listed as automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification.

Invited Speakers

• Claudia Nalon (University of Brasilia, Brasil)
• Catuscia Palamidessi (INRIA Saclay and LIX, France)

Submission deadline is 31 March 2017. See the workshop web site for details.

### Metafinite 2017: Workshop on Metafinite model theory and definability and complexity of numeric graph parameters

June 19 2017, Reykjavik, Iceland

The workshop will bring together three strands of investigation dealing with the model theory and complexity of numeric graph parameters and their generalization to other first order structures.

(A) Gurevich and Graedel in 1998 initiated the study of metafinite model theory to study descriptive complexity of numeric parameters. Metafinite model theory found most of its applications in databases and abstract state machines (ASM), but was not widely studied in connection to numeric combinatorial parameters.

(B) Courcelle, Makowsky and Rotics initiated a definability theory for graph polynomials in 2000 and proved metatheorems for graph polynomials and numeric structural parameters.

(C) Kotek, Makowsky and Ravve questioned wether the Turing model of computation was the right choice to discuss the complexity of numeric graph parameters and proposed alternatives using the Blum-Shub-Smale model of computation.

The aim of the workshop is to bring together researchers of these three strands in order to further explore and elaborate on the appropriate framework for the study of numeric structural parameters and polynomials and to investigate further metatheorems.

Keynote Speakers

• Y. Gurevich (Microsoft, Redmond, USA)
• E. Graedel (RWTH Aachen, Germany)

Submission deadline is 7 April 2017. See the workshop web site for details.

### ARCADE: Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements

6 August 2017, Gothenburg, Sweden

The main goal of this workshop is to bring together key people from various subcommunities of automated reasoning such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community. The title of the workshop is indicative of the kind of discussions we would like to encourage:

• Challenges: What are the next grand challenges for research on automated reasoning?
• Applications: Is automated reasoning applicable in real-world (industrial) scenarios.
• Directions: Based on the grand challenges and requirements from real-world applications, what are the research directions the community should promote?
• Exemplary Achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself?

Submission deadline is 12 May 2017. See the workshop web site for details.

### PCR'17: Workshop on Parallel Constraint Reasoning

6 August 2017, Gothenburg, Sweden

The workshop focuses on theory, implementation, and applications of parallel constraint reasoning. The phenomenal recent success in constraint reasoning has made approaches previously deemed impractical within the reach of both industrial and academic applications. Since some time the technology for producing CPUs has hit a physical barrier for obtaining sequential speed-up through laying out transistors on a chip. Since speed-up is no longer achievable through sequential hardware, there is an ongoing shift to wide-spread parallel computing. The workshop program will be organized as a collection of high-quality invited talks.

See the workshop web site for details.

### ThEdu'17: Theorem Prover Components for Educational Software

6 August 2017, Gothenburg, Sweden

(Computer) Theorem Proving (TP) is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. Topics of interest include:

• methods of automated deduction applied to checking students' input;
• methods of automated deduction applied to prove post-conditions for particular problem solutions;
• combinations of deduction and computation enabling systems to propose next steps;
• automated provers specific for dynamic geometry systems;
• proof and proving in mathematics education.

Submission deadline is 18 June 2017. See the workshop web site for details.

### HCVS: Horn Clauses for Verification and Synthesis

7 August 2017, Gothenburg, Sweden

Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the Automated Deduction, Constraint/Logic Programming and Verification communities have centered around efficiently solving problems presented as Horn clauses. This workshop aims to bring together researchers working in the communities of Automated Deduction (e.g CADE), Constraint/Logic Programming (e.g., ICLP and CP) and Program Verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.

Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:

• Automated deduction
• Analysis and verification of programs in various programming paradigms (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent)
• Program synthesis
• Program testing
• Program transformation
• Constraint solving
• Type systems
• Case studies and tools
• Challenging problems

Submission deadline is 11 June 2017. See the workshop web site for details.

### Vampire 2017: The 4th Vampire Workshop

7 August 2017, Gothenburg, Sweden

The workshop aims at discussing recent developments in implementing, applying benchmarking and comparing first-order theorem provers and their combinations with other systems. Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The workshop is going to to shed the light on on problems such as

• what is essential for substantial progress in theorem proving tools;
• what are the best implementation principles to be used;
• what are the best heuristics and strategies, depending on application areas;
• both successful and unsuccessful case studies;
• missing features in modern theorem provers.

Submission deadline is 1 July 2017. See the workshop web site for details.

### The 6th Unilog - World Congress and School on Universal Logic, call for workshops and tutorials

June 16-26, 2018, Vichy, France

The previous edition in Istanbul gathered more than 400 logicians from about 50 different countries. For the 6th edition we will follow the same format:

• A school of logic of 5 days with 30 tutorials
• A congress of 6 days with about 30 sessions/workshops
• A contest (the topic will be announced soon)
• A secret speaker (speaker whose identity is revealed only at the time of her / its / his speech).

Timeline
Call for Workshops and Tutorials: Now - Deadline: April 11, 2017
First call for contributing talks: May 2017 - Deadline to submit an abstract: September 15, 2017
Early registration: December 1st, 2017

If you want to submit a workshop or a tutorial, send a proposal to vichy@uni-log.org by April 11, 2017 following the format of the previous edition:

## Spring and Summer Schools

### DeepSpec Summer School on Verified Systems

The first DeepSpec Summer School on Verified Systems will be held in Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq Intensive from July 13 to 15.

An overview of the program is available here. Applications are currently being considered on a space-available basis.

### First School on Foundations of Programming and Software systems -- Probabilistic programming

May 29th - June 4th 2017, Braga, Portugal

It is our greatest pleasure to announce the first edition of the School on Foundations of Programming and Software systems. The school is jointly funded by EATCS, ETAPS, ACM SIGLOG, and ACM SIGPLAN. The topic of the first edition is Probabilistic programming. It will take place in Braga, Portugal, May 29th - June 4th 2017.

Probabilistic programming languages are used for modelling and analysis purposes across multiple areas of computer science, including machine learning, security, and quantitative biology. In particular,they provide a rigorous foundation for machine learning where they are used to describe probabilistic models and to perform inference in presence of uncertain information. Probabilistic programs are also used in cryptography and in privacy for modelling and quantifying security. The goal of the school is to introduce attendants to theoretical and practical aspects of programming languages, and will propose courses that cover the following topics: semantics, analysis, verification, applications to machine learning, privacy, and security. The school will have lectures by Andy Gordon, Catuscia Palamidessi, Christel Baier, Dexter Kozen, Frank Wood, Hongseok Yang, Javier Esparza, Michael Carbin, Peter Selinger, Prakash Panangaden, Sriram Sankaranarayanan, and Vitaly Shmatikov.

If you have any queries feel free to contact the organisers.

### Marktoberdorf Summer School: Logical Methods for Safety and Security of Software Systems

August 2-11 2017, Marktoberdorf, Germany

The "Marktoberdorf Summer School" is an 10-day event for young computer scientists and mathematicians, typically doctoral and post-doctoral researchers. It provides mini-courses on state-of-the-art topics in "Logical Methods for Safety and Security of Software Systems" and leaves ample room for interaction between participants and speakers.

Speakers and courses:

• Christel Baier: Probabilistic Model Checking
• Gilles Barthe: Relational Verification for Differential Privacy and Cryptography
• Nicolaj Bjørner: Satisfiability Modulo Theories
• Cédric Fournet: Security Verification in F*
• Orna Grumberg: Program Repair
• Joost-Pieter Katoen: Foundations of Probabilistic Programming
• Daniel Kroening: Static Analysers for Black Hats and White Hats
• Orna Kupfermann: Automated Synthesis of Temporal-Logic Specifications
• Magnus Myreen: Verification of an ML Compiler
• Tobias Nipkow: Verified Analysis of Functional Data Structures
• Larry Paulson: Proof Support for Hybrid System Analysis
• Andre Platzer: Dynamic Logic for Dynamical Systems

Apply online: https://asimod.in.tum.de/2017/participation.shtml

### SC2 Summer School 2017

July 31 - August 4, 2017, Saarbruecken, Germany

The school introduces graduate students and researchers from academia and industry into research and methodology in both Satisfiability Checking (SAT/SMT) and Symbolic Computation with one focus on their interconnections. It combines a thorough introduction into the theory of both fields with lectures on state-of-the-art software systems and their implementation. This is supplemented with presentations by lecturers from industry discussing the practical relevance of the topics of the school.

Speakers and courses:

• Marijn Heule: State-of-the-art SAT Solving
• Cesare Tinelli: Foundations of Satisfiability Modulo Theories
• Keijo Heljanko, Tomi Janhunen, Tommi Junttila: Practical Session on SAT/SMT
• Hoon Hong: Symbolic Computation (Quantifier Elimination)
• James Davenport: Symbolic Computation through Maple and Reduce
• Christopher W. Brown: Cylindrical Algebraic Decomposition and Real Polynomial Constraints
• Tom Bienmueller: Industrial Applications and Challenges for Verifying Reactive Embedded Software
• David Deharbe: Formal Verification in an Industrial Setting
• Grant Passmore: Formal Verification of Financial Algorithms
• Christoph Weidenbach: State-of-the-art FOL Solving
• Jasmin Blanchette: Interactive Theorem Proving in Higher-Order Logics

## Open Positions

### PhD positions on the AI4REASON project in Prague, Czech Republic

Czech Technical University in Prague, Czech Institute of Informatics, Robotics and Cybernetics, Josef Urban

Job description
You will be working on the ERC project AI4REASON (http://ai4reason.org). The project's goal is to develop new combinations of AI, Machine Learning and Theorem Proving methods that learn reasoning guidance from large proof corpora and use such guidance to steer the automated reasoning processes at various levels of granularity. Our motivation is to

• facilitate automated computer encoding, understanding and large-scale verification of mathematics, science, software and hardware designs, and to
• research AI methods that combine learning and reasoning over large repositories of complex mathematical knowledge, getting closer to human-level scientific thinking.

Topics of interest include:

• machine learning procedures over large proof libraries
• methods that propose useful intermediate lemmas for long proofs
• methods that efficiently apply learned knowledge in proof search
• feedback loops between learning and automated reasoning
• statistical and deductive methods for automated formalization of informal mathematics
• learning from aligned informal, semiformal and formal corpora

The work will include close collaboration with several international partners: University of Innsbruck, Google Research, University of Miami, Radboud University Nijmegen and others.

Requirements
You should meet the following requirements:

• A master's degree (or equivalent) in Computer Science, Mathematics
• or a related field, with a strong interest in Machine Learning, AI
• and/or Automated Reasoning;
• Commitment and a cooperative attitude;
• Proficiency in written and spoken English.

You will enroll in the PhD program in Artificial Intelligence at CTU with an individual study plan.

Application
Inquiries and applications should be sent via email to Josef Urban with "AI4REASON PhD" in the subject. When sending an application please include your CV together with a brief description of your research accomplishments and interests, including the names of two references.

Deadlines: March 1, 2017, or until the positions are filled. Earlier applications are welcome and and early start date is an advantage.

### PhD positions at ETH Zürich, Switzerland

The Chair of Programming Methodology at ETH Zürich is looking for excellent candidates for newly-opened PhD positions. The successful applicant will join our research group and begin work along on a new project for two PhD candidates, beginning in 2017. The project will investigate the question of how to connect modern capability-based type systems (such as that employed by the Rust programming language), and formal program reasoning techniques, in order to develop a new kind of lightweight verification tool specifically targeted at enabling everyday programmers to reason about the correctness of their code. This work is part of our ongoing Viper project.

Key requirements for successful applications:

• Strong commitment to research
• Interest in programming languages, tool building, formal reasoning, and software correctness
• Excellent M.Sc. or B.Sc. degree in Computer Science or in a related subject with a strong Computer Science component
• Proficiency in English and excellent communication skills, both oral and written
Applications and questions should be sent to Mrs. Marlies Weissert. The application should include a CV and a description of research interests. We will consider applications until the positions are filled. The start date is negotiable.

• PhD and post-doc positions are fully funded and have an attractive salary and social benefits.
• Full scholarships are available for outstanding B.Sc. students interested in the PhD.
• ETH has one of the top computer science departments in the world: CS University Rankings
• Zürich is consistently ranked among the top destinations in the world for quality of life
• General information on doctoral studies at ETH is available at www.inf.ethz.ch/education/ds

### Postdoctoral openings at Carnegie Mellon University, USA

We invite applications for two postdoctoral researcher positions at Carnegie Mellon University. The researchers will be supervised by Anupam Datta and Matthew Fredrikson.

The researcher will work to develop the emerging area of computational accountability -- theories and tools to analyze big data systems in support of security and privacy goals. The technical approach involves a combination of methods from security and privacy, programming languages and verification, statistics and causality, applied to machine learning algorithms and implementations. The ideal candidate should have expertise in at least one of these areas and interest in the others.

More details on this research direction can be found here. Interested candidates can email their CV and short description of relevant research background to Anupam Datta and Matt Fredrikson with the subject "CMU Accountability Postdoc 2017".

### Phd positions in verification of concurrent and distributed systems at Irif, France

Constantin Enea

Several Phd positions are available in my group at University Paris Diderot, France, on various topics related to the construction of reliable software running on top of shared-memory or distributed infrastructures.

The main focus is developing automated formal methods for distributed data structures (DDSs) like Amazon Simple Storage Service, Cassandra, Google AppEngine Datastore, MongoDB, etc., which are at the basis of a wide range of automated services. The design and the usage of such data structures are based on new principles, for which we currently lack rigorous engineering methodologies. Specifically, we lack design procedures based on precise specifications, and automated reasoning techniques for enhancing the reliability of the engineering process. The main objectives are to develop (1) coherent formal specifications that provide precise requirements at design time and explicit guarantees during their usage, (2) programming principles, compatible with these specifications, for building applications on top of DDSs, and (3) efficient automated reasoning techniques for debugging or validating DDSs implementations against their specifications.

I am looking for candidates with a strong background in Computer Science with an interest in formal methods, programming languages, and algorithms. Experience in distributed systems and software development would be advantageous.

### 10+ Open Positions on Formal Methods and Cyber-Physical Systems in Tokyo, Japan

Ichiro Hasuo

For our new 5.5-year research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for 10+ senior researchers and postdocs, together with research assistants (PhD students) and internship students.

This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application (esp. in automotive industry). The project covers diverse areas that include: formal methods, programming languages, software science, software engineering, control theory, machine learning, numerical optimization, user interface, mathematical logic and category theory.

### Google Summer of Code opportunities for students on projects related to automated reasoning and proof compression

Bruno Woltzenlogel Paleo

Two of my projects (Scavenger and Skeptik) are going to participate in Google Summer of Code this year. Both projects are implemented in Scala. Scavenger is a first-order theorem prover, and Skeptik is a tool for compressing formal proofs. Undergraduate, M.Sc. and Ph.D. students are eligible to apply. More information can be found at http://www.aossie.org/.

Student application deadline for the google summer of code: April 3 16:00 UTC

### Several Positions on Higher-Order Proof Automation at VU Amsterdam, the Netherlands, and Inria Nancy, France

Matryoshka is an ambitious research project that aims at developing efficient higher-order superposition provers and higher-order SMT (satisfiability modulo theories) solvers and integrating them in proof assistants. The project is funded by a European Research Council Starting Grant from March 2017 to February 2022. It is co-located between Vrije Universiteit Amsterdam (Jasmin Blanchette) in the Netherlands and Inria Nancy – Grand Est (Pascal Fontaine) in France.

Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. To make interactive verification more cost-effective, we propose to deliver powerful automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. Our approach will be to enrich the superposition calculus and SMT with higher-order reasoning in a careful manner, to preserve their desirable properties. We will develop highly automatic provers building on modern superposition provers and SMT solvers, following a Russian doll architecture. To reach end users, these new provers will be integrated in proof assistants, including Coq, Isabelle/HOL, and the TLA+ Proof System.

We are looking for outstanding candidates for several Ph.D., postdoctoral, software engineer, and intern positions due to start in the next two years. Candidates should ideally have some experience with automatic or interactive theorem proving and be at ease with both theory and engineering. Please contact Jasmin Blanchette and Pascal Fontaine for more information.

## The Editor's Corner: change of editors and survey about the AAR Newsletter

Philipp Rümmer and Sophie Tourret
newly appointed co-editors of the AAR Newsletter

We would like to thank the AAR board for trusting us with the duty of editing the AAR newsletter. We will do our best to keep its quality at the (high) level set by our predecessors.

To get started, we would like to learn a bit more about the audience of the newsletter. If you have five minutes to spare, we would be grateful if you can provide input by answering this short survey. The survey is anonymous, and all suggestions or opinions are welcome. Of course, you can always write directly at newsletter@aarinc.org to let us know of your opinion, or of any event that you want to see in the newsletter, including job opportunities, book publications and anything you would like the AR community to know about.