Newsletter No. 121

September 2017

September 2017

- From the AAR President, Larry Wos
- Guest Column: Report on the first ARCADE workshop at CADE-26
- Letter to the Editors: On the first big proof in the history of theorem proving
- Proposals for Sites for CADE-27 in 2019 Solicited
- Announcement of CADE Trustee Elections
- Further Announcements
- Special Issues
- Conferences: Calls for Papers
- CPP 2018: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
- NFM 2018: The 10th NASA Formal Methods Symposium
- FLOPS 2017: The 14th International Symposium on Functional and Logic Programming
- FSCD 2018: Third International Conference on Formal Structures for Computation and Deduction
- IJCAR 2018: The 9th International Joint Conference on Automated Reasoning
- CAV 2018: The 30th International Conference on Computer Aided Verification
- FM 2018: The 22nd International Symposium on Formal Methods

- Conferences: Calls for Participation
- MEMOCODE 2017: 15th ACM/IEEE International Conference on Formal Methods and Models for System Design
- FMCAD 2017: International Conference on Formal Methods in Computer-Aided Design
- PPDP 2017: The 19th International Symposium on Principles and Practice of Declarative Programming
- LOPSTR 2017: The 27th International Symposium on Logic-Based Program Synthesis and Transformation
- GCAI 2017: The 3rd Global Conference on Artificial Intelligence
- HVC 2017: Thirteenth Haifa Verification Conference

- Workshops
- Autumn and Winter Schools
- Open Positions
- One Professor/Reader/Senior Lecturer and One Lecturer in Program Analysis and Cyber Security at the University of Manchester, UK
- Announcement of a full professorship in Computer Aided Verification (succeeding Helmut Veith) at TU Wien
- PhD Position on Integrating Automated Provers in Proof assistant at University Paris Saclay, France
- PhD/PostDoc position at University of Freiburg, Germany
- Multiple postdoc and PhD positions at TU Darmstadt, Germany

In this column, algebra again takes center stage. Here I offer substantial challenges for you.

I was first introduced to the notion of proof when I entered the math
department at the University of Chicago as a graduate student.
I was treated to lectures by I. J. Kaplansky, Paul Halmos, and others who
proved one theorem after another.
For example, suppose that the theorem was to prove commutativity for groups in
which the square of `x`

, for all `x`

, is the identity
`e`

.
Then, if a proof was offered, on the blackboard
would appear a series of equations the last of which would be `xy = yx`

.
For that problem, the assumption that commutativity was not present was not
used (as the proof proceeded), namely, the assumption that `ab ≠ ba`

for constants `a`

and `b`

.
In particular, I did not often witness a proof by contradiction.
Instead, typically all the steps of the proof were obtained by forward reasoning,
reasoning from axioms and other properties.
Such a proof is called a direct proof.

If, at the time (in the early 1950s), the intention was to automate the finding of proofs, the
programmer (if such existed), seeking a direct proof, could have placed, say,
`xy = yx`

on some list and continually
compared the conclusions drawn by the program to see whether the goal had
been reached.
From the viewpoint of history, computer programs were not around in the early 1950s in general -- none, certainly, for automated reasoning.
In contrast, if this theorem were given to an automated reasoning program of
the type I rely on today, then as part of the input I would include a clause
asserting `ab ≠ ba`

for constants `a`

and `b`

.
The program, if successful, would return a proof by contradiction, using the
given inequality.

Now, if this inequality were used to detect unit conflict and in no other way, then all the reasoning offered by the program would be forward reasoning. Such a proof is called a forward proof. On the other hand, if the program offered a proof none of whose steps relied purely on axioms and various hypotheses, then the proof is a backward proof. And if the proof exhibited both forward and backward reasoning, it is a bidirectional proof. Bidirectional proofs are frequently easier to obtain with an automated reasoning program. One reason rests with the level of a bidirectional proof. You might say that compared with either a forward or backward proof, a bidirectional proof (so to speak) meets in the middle. (If the only inference rule in use is condensed detachment, however, then for efficiency forward reasoning had best be used.)

The proofs under discussion here are first-order proofs, in contrast to higher-order proofs that some reasoning programs can find, as with M. Beeson's extension of OTTER.
All proofs yielded by OTTER, Bill McCune's splendid contribution to the
field, focus on first-order reasoning.
My particular preference is for forward proofs (as opposed to bidirectional proofs), if such can be found with the
program in use and within the constraints imposed.
For the given example, I would ideally prefer a proof that completes with
`xy = yx`

.
But for reasons regarding instantiation and the lack of appropriate strategy to control its use,
the proofs I have found, in my research, are proofs by contradiction.
In particular, for example, I never find a proof that deduces `xy = yx`

, which is the desired conclusion to be proved for groups of exponent 2.
Proofs by contradiction are what are usually sought in automated reasoning, in contrast to proofs that simply terminate with the discovery of the sought-after goal;
the discovery of a contradiction provides an excellent (so-to-speak) stop
condition.

I now turn to the set of challenges and, specifically, to an achievement made by Bob Veroff in 2005. The theorem that was offered is taken from median algebra. A proof of the theorem did exist, but no first-order proof existed, from what I know, until Veroff found one. The following axioms for median algebra are to be used.

% Following 4 axioms for median algebra, from Veroff in turn from D. Knuth. f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity).(Yes, the problem was conveyed by Knuth to Veroff.)

For the target, the conclusion of the theorem, I present it in two forms, each negated, by interchanging the arguments.

% Denial of distributivity, as recently sent by Veroff. f(f(a1,a2,a3),a4,a5) != f(f(a1,a4,a5),f(a2,a4,a5),f(a3,a4,a5)) | $ANS(DIST). % Alternative denial of distributivity, as recently sent by Veroff. f(f(a1,a4,a5),f(a2,a4,a5),f(a3,a4,a5)) != f(f(a1,a2,a3),a4,a5) | $ANS(DIST).For the first challenge, you are asked to obtain a proof of any type, but the proof must be first-order. For your second challenge, you are asked to find a proof in which no demodulation occurs. (As many of you know, I prefer proofs in which demodulation is not relied upon.) In other words, you are asked to find a proof without relying on a Knuth-Bendix approach. For your third challenge, you are asked to find a proof that is forward, using denial only at the so-called unit conflict stage. A proof that uses a denial, such as

`ab ≠ ba`

, only for unit conflict but not for drawing conclusions is, of course, a forward proof.
One more challenge might indeed prove intriguing and perhaps be most difficult to meet. The challenge is in the context of proof elegance, a topic I addressed in the book titled Automated Reasoning and the Discovery of Missing and Elegant Proofs. Specifically, you are asked to find a proof of distributivity from the given axioms, a proof that is free of demodulation, that is based on forward reasoning, and -- the aspect of elegance -- that has a length less than or equal to 50 (as measured in the number of deduced equations).

I plan in a future column to focus on an aspect of elegance different from that of concern in this last challenge.

Giles Reger and Dmitriy Traytel, PC Chairs of ARCADE

The main goal of the ARCADE workshop was to bring together key people from various sub-communities of automated reasoning to discuss the present, past, and future of the field. ARCADE invited non-technical position statements of 2-4 pages. Out of 19 submitted abstracts the program committee selected 14 for presentation and discussion at the workshop.

With its 45 attendees, the first installment of the ARCADE workshop was half as large as CADE itself. Several participants came to Gothenburg only or mainly because of ARCADE.

The workshop was divided into five sessions. Each session consisted of 2-3 short talks of either 5 or 10 minutes followed by a discussion of the presented topics driven by questions submitted by the authors. The accepted abstracts and proposed questions were published on the workshop's web-page in advance of the workshop to allow attendees to consider these points beforehand. In the following we present an incomplete but representative selection of highlights from the discussion sessions.

The first session discussed how to bridge the gaps between the various
sub-communities of automated reasoning (AR) as well as the even wider gaps
between automated reasoning and other communities. James Davenport highlighted
some of the very basic problems, including varying terminology across
communities, which popped up in the SC^{2} project about combining SMT solvers and
computer algebra systems. To make progress for SC^{2}, patience and many dialogues
were necessary. A discussion around combining AR methods concluded that simple
and elegant tools with good interfaces are a prerequisite to success.

The topic of the second session was machine learning (ML) and more generally artificial intelligence (AI). Although historically AR was a part of AI, Maria Paola Bonacina made the point that AI has become synonymous with ML, while AR has become a second choice technology in cases where ML fails. As a community we cannot be satisfied with this status, but the immediate countermeasures remain unclear. Various ways of combining AR and ML have been discussed: namely, to use AR to explain the decision made by ML and to use ML to guide the search in AR. The idea of a joint workshop bringing AR and ML together was proposed.

The next session dealt with the user friendliness of AR tools and their
applicability in industry. Marijn Heule presented the industry success story of
the ACL2 proof assistant. The key to success was that success in industry

was
an original design goal of ACL2. Yet, the needs of industry were not
necessarily aligned with the research directions in AR. Industry cares about
usability and efficiency, but not so much about completeness. A suggestion was
made that we become more user-driven, with support (through calls for papers
etc.) for experimental user studies, and support for industry-focused problems
in competitions. Reiner Hähnle pointed out that to sustainably support this
through funding agencies, computer science in general needs to be reclassified
as an engineering science (as opposed to a theoretical science).

The fourth session focused on methods to make proofs produced by systems more
easily checkable. For proofs produced by SAT solvers this meant including
reasoning about absence of formulas (e.g., clause deletion in DRAT) and
advanced features used by SAT solvers (e.g., symmetry breaking) in the proof
format. In the case of first-order (FO) solvers the solution is less clear and
the consensus was that it is hard to go beyond the very general standardized
semantic-less TSTP proof format, as there is no agreement on the prime

FO
calculus.

The last session dealt with current challenges for actual reasoners, such as
lifting answer set programs to first-order, adding synthesis to SMT via
quantifier instantiation, and extracting common principles (Model Portfolio

)
from different calculi for fragments of first-order logic. In the discussion,
it was observed that the common principle of those challenges was the
identification of a weak spot in existing approaches. A resulting consideration
was to focus the evaluation of reasoners around the number of uniquely solved
problems. Geoff Sutcliffe confirmed that the CASC competition measures this,
but does not reward tools that perform well according to this metric.

In a final round of discussion, we considered various constellations of `N`

authors and `M`

pages for a document that would summarize the state-of-the-art in
AR and upcoming challenges. For `N > 40`

and `M < 5`

, an idea of a CACM article on
the challenges in AR was discussed. Another proposal was a survey of AR, with
`N < 20`

and `M > 40`

. For `N = 1`

and `M > 300`

, an more up-to-date textbook than the
Handbook of Automated Reasoning

to attract new PhD students was considered
helpful. In this space, John Harrison's Handbook of Practical Logic and
Automated Reasoning

is a good hands-on introduction to many topics, but it is
deliberately selective in what it covers to keep things elementary

. Rumors tell
that Christoph Weidenbach is working on another textbook draft.

After the workshop, the authors have been invited to update their original submissions with respect to the discussions held and to submit them to a post-proceedings that will be published as an EPiC volume. Additionally, attendees have been invited to submit papers covering points that arose from the discussions. The aim is for the post-proceedings to appear in October.

The organization of ARCADE was very smooth and easy going, mainly due to the great support that we received from the CADE community. We thank Christoph Weidenbach, who initiated the workshop and jointly with Jasmin Blanchette helped recruiting most of the program committee. We are very grateful to Wolfgang Ahrendt and the local organization team for taking great care of everything on-site and reserving the venue for the ARCADE dinner. The latter was suggested by Reiner Hähnle and turned out to be a great choice. We thank the program committee (and one sub-reviewer) for detailed, careful, and constructive reviews and the pleasant discussion. This report benefited from notes taken by James Davenport during the workshop and from Jasmin Blanchette's comments. Finally, we thank the authors and the attendees for creating such a diverse and timely program and discussion that will certainly have an impact on the future of automated reasoning.

Maria Paola Bonacina, Universite degli Studi di Verona

In the guest column of AAR Newsletter No. 120 (June 2017) Christoph Weidenbach proposes as challenge the development of automated reasoning procedures that search simultaneously for a proof or a counter-model. While the idea itself is not new, since for example Ricardo Caferra and Nicolas Zabel had an article entitled A method for simultaneous search for refutations and models by equational constraint solving as early as 1992, I agree that the time is ripe given the awsome advances of our field as witnessed this summer at CADE-26 and Big Proof. Model-based methods appear a natural starting point for this quest.

The purpose of this letter is to complement Chris' column
on the historical record of the first big proof that Chris mentions,
namely Bill McCune's
automated proof that Robbins algebra are Boolean,
of which Chris writes
The formalization of the Robbins conjecture is a problem in first-order
logic with equality. Bill designed a specific version of Otter, called EQP,
to fit exactly this problem.

First, the formalization of the Robbins theorem only requires equational logic.
Second,
EQP is not a version of
Otter:
it is a distinct theorem prover for reasoning in equational theories,
possibly with AC operators,
while Otter is a theorem prover for full first-order logic with equality.
Third,
saying that EQP was designed "to fit exactly" the Robbins problem
is too strong and may be misunderstood as implying that EQP was
somehow *ad hoc*, which is not the case:
EQP is a *generic* prover for (AC) equational reasoning
in the same category as
Waldmeister.

In those years I was working on
parallel
theorem proving by Clause-Diffusion,
using Bill's code as sequential base for the
Clause-Diffusion
provers.
I visited Argonne, and Bill and I were in correspondence by e-mail for years.
Bill told me that he wrote EQP because he felt that Otter had become big,
with many options and parameters,
and Bill wanted a leaner prover to experiment with.
In hindsight,
clearly the Robbins conjecture was one of the objectives of this
experimentation, but there is no historical evidence that I know of
to suggest that it was the only one:
Bill was interested in
automated reasoning in mathematics and
specifically in algebraic structures presented by sets of equations,
often including *associative and commutative* (AC) operators.
This goal requires high-performance equational reasoning
and reasoning modulo AC.
Bill decided that it was not a good idea to encapsulate these
features in Otter as a special configuration
and opted for developing a different prover.

For an idea of the differences between EQP and Otter,
it suffices to consider that EQP features a main control loop,
called the *pair algorithm*, that Otter does not have
and that is different from Otter's *given-clause algorithm*.
The concept of *ordering-based strategies* is to keep things small
with respect to *well-founded orderings*.
Thus, it is crucial to perform *contraction*
(e.g., simplification, subsumption)
with higher priority than *expansion*
(e.g., ordered resolution, superposition, ordered paramodulation).
In the *given-clause loop*
at every iteration the prover selects a *given clause*
and performs all expansion inferences between the given clause and all
previously selected clauses.
Then,
it applies the newly generated clauses to reduce the previously existing ones,
a process called *backward contraction*.
If paramodulation is done modulo AC,
there are many AC-paramodulants.
Bill observed that generating all the AC-paramodulants between the given
equation and all other previously selected equations before allowing
backward contraction was detrimental for performance,
because it meant too much expansion without contraction.
Thus, he devised the *pair algorithm*,
where at every iteration the prover selects a *pair of equations*
and performs only the expansion inferences between them.
The pair algorithm was a main ingredient in both sequential and parallel
proofs of the Robbins theorem by EQP and its Clause-Diffusion
parallelization
Peers-mcd,
respectively.
This difference in the main control loop exemplifies how
EQP and Otter are different provers.

Christoph Weidenbach, President of CADE, and
Martin Giese, Secretary of AAR and CADE

We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2019. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome. CADE's/IJCAR's recent location history is as follows:

- 2009: CADE-22 in North America
- 2010: IJCAR 2010 as part of FLoC in Europe
- 2011: CADE-23 in Europe
- 2012: IJCAR 2012 in Europe
- 2013: CADE-24 in North America
- 2014: IJCAR 2014 as part of FLoC in Europe
- 2015: CADE-25 in Europe
- 2016: IJCAR 2016 in Europe
- 2017: CADE-26 in Europe

The upcoming CADE/IJCAR event will be:

- 2018: IJCAR 2018 in Europe

The deadline for proposals is **30 October 2017.**

In addition, we encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.

Proposals should address the following points that also represent criteria for evaluation:

- National, regional, and local AR community support:
- CADE Conference Chair and host institution,
- CADE Local Arrangements Committee,
- availability of (and reward for) student-volunteers.

- National, regional, and local government and industry support, both organizational and financial.
- Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
- Appropriateness of proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities (a.k.a. residence halls).
- Conference and exhibit facilities for the anticipated number of registrants (typically 100-200), for example,
- number, capacity and audiovisual equipment of meeting rooms,
- a large plenary session room that can hold all the registrants,
- enough rooms for parallel sessions/workshops/tutorials,
- Internet connectivity and workstations for demos/competitions,
- catering services,
- presence of professional staff.

- Residence accommodations and food services in a range of price categories and close to the conference facilities, for example
- number and cost range of hotels,
- availability and cost of dormitory rooms (e.g., at local universities) and kind of services they offer.

- Rough budget projections for the various budget categories, e.g.,
- cost of renting/cleaning the meeting rooms, if applicable,
- cost of professional conference secretariat, if hired,
- financial model for satellite workshops and/or co-located events.

- Balance with regard to the geographical distribution of previous conferences.

Prospective organizers are encouraged to get in touch with the CADE secretary and president (at martingi (at) ifi.uio.no and weidenbach (at) mpi-inf.mpg.de) for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.

Martin Giese, Secretary of AAR and CADE

An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:

- Christoph Benzmüller (vice-president, elected 2015)
- Jasmin Blanchette (elected 2016)
- Pascal Fontaine (elected 2014)
- Martin Giese (secretary)
- Jürgen Giesl (elected 2014)
- Laura Kovacs (elected 2016)
- Aart Middeldorp (elected 2015)
- Neil Murray (treasurer)
- Renate Schmidt (elected 2016)
- Stephan Schulz (IJCAR 2018 program co-chair)
- Geoff Sutcliffe (elected 2011, reelected 2014)
- Christoph Weidenbach (president, elected 2016)

The terms of Pascal Fontaine, Jürgen Giesl, and Geoff Sutcliffe end. There are thus *three* positions of elected trustees to fill.

The following candidates were nominated and there statements are below:

- Andrew Reynolds, nominated by Pascal Fontaine & Laura Kovacs
- Bruno Woltzenlogel Paleo, nominated by Geoff Sutcliffe & Chris Benzmüller
- Jürgen Giesl, nominated by Jasmin Blanchette & Christoph Weidenbach
- Marijn Heule, nominated by Armin Biere & Nikolaj Bjørner

CADE was the first conference I attended as a PhD student and is my favorite conference to attend. I have always found the CADE community to be great at stimulating collaboration and new ideas among a range of researchers within automated deduction. I have attended every CADE and IJCAR since 2012 (as well as in 2009 and 2010), have sub-reviewed numerous papers, and had the pleasure serve on the program committee and as the co-organizer of workshops and competitions for CADE 25 in Berlin.

My research has focused on developing techniques in Satisfiability Modulo Theories (SMT) solvers. I am one of the main developers of the SMT solver CVC4, which is a frequent participant in the CASC competition. While most of the SMT community focuses on quantifier-free reasoning, my research has focused on new approaches that combine background theories and quantified formulas, and hence often aligns closely with the research at CADE. In the coming years, more tools within the automated theorem proving community will benefit from SMT solver back ends, and conversely SMT solvers will learn from techniques that target other logics.

As a member of the steering committee, I would further emphasize putting foundational research into practice. I believe that the many great ideas that come out of the CADE community should be applied more actively in academia and industry. I believe that competitions like CASC and SMT-COMP are a great driving force in encouraging researchers to develop tools that are efficient, robust and trustworthy. Another initiative that other conferences have added recently is an optional artifact submission associated with each accepted paper. I have participated in artifact evaluation committees for the CAV and POPL conferences and found them encourage higher quality and robust tools. An artifact evaluation submission is something for CADE to consider in the future.

I believe the CADE community should actively seek cross-fertilization with related fields like software verification and automated synthesis. Automated theorem provers already can play a more active role in these areas. For instance, constrained Horn clause solving and syntax-guided synthesis are two application-inspired disciplines that are converging with techniques for automated theorem proving. CADE is potentially a great place to bring these communities together. In particular, I believe it is important to encourage a broad range of workshops at CADE, as this is great way to encourage researchers from neighboring fields to attend CADE.

I participated in CADE/IJCAR for the first time in 2010, within FLoC in Edinburgh. Since then, CADE has been one of my favorite conferences because it balances theory, implementation and applications.

This is a balance that I have tried to pursue in my own research as well. My recent achievements include: the Conflict Resolution calculus, which is a lifting of the proof-theoretical aspects of CDCL to first-order logic, implemented in the Scavenger theorem prover; algorithms for compressing propositional and first-order resolution proofs generated by sat-solvers, SMT-solvers and ATPs, implemented in Skeptik; formalization of ontological arguments by Gödel, Leibniz and others in Coq and Isabelle.

I have served the CADE community by: chairing the PxTP and the UITP workshops; organizing the APPA (All about Proofs, Proofs for All) tutorials at the Vienna Summer of Logic; and creating and maintaining the Encyclopaedia of Proof Systems.

Looking forward, one of CADE's main challenges is to deal with the fact that automated deduction is a mature field, where a lot of great work has already been done; the entrance barrier is high, and the rewards for overcoming it are low. As a consequence, participation and submission numbers seem to be struggling to remain stable, and are low compared to conferences in other more popular computer science fields. This situation is problematic, especially for early-career researchers.

There are also challenges faced by the academic world as a whole (e.g. transparency, reproducibility of results, objectivity, diversity and inclusion, relevance to society...), and I believe CADE is in a good position to take a leading role in tackling these challenges among computer science conferences.

I have thought of a few concrete ideas to address these challenges. As an elected trustee, I would pursue only those ideas approved by a majority in this survey.

You can learn more about me in my website.As a trustee, my goal would be to keep the scope of CADE as broad as possible. CADE should be open to any aspect of automated deduction and it should cover everything from theoretical results and practical contributions up to applications of automated reasoning. It is important to make clear that every sub-field of automated reasoning is highly welcome at CADE to ensure CADE's position as the leading main conference of the field.

I also think that it is very important to attract tool submissions, and to organize tool competitions co-located with CADE. (Since its foundation in 2004, I have been active in the termination competition, which took place during IJCAR/CADE several times.)

I think the current organization of CADE as a stand-alone event every second year, within IJCAR every other year, and within FLoC every four years is a very good solution to guarantee the visibility of CADE on its own, while keeping in close contact with neighboring meetings and fields.

To attract as many participants as possible and to allow students to attend the conference, I think CADE should aim at affordable conference fees and continue the very good tradition of Woody Bledsoe travel grants for students.

My own research is concerned with different aspects of automated deduction. Therefore, I have been attending and publishing papers at CADE since 1994. In particular, I am working on techniques and tools to analyze properties like termination or complexity of programs automatically.

I was one of the PC chairs of IJCAR 2010, PC chair of RTA 2005, steering committee chair of RTA (2005-2007), area editor of ACM TOCL (since 2013), and I served many times on the PCs of CADE, IJCAR, RTA, LPAR, and several other conferences in the field. I have been CADE trustee from 2010-2011 and from 2014-2017.

The focus of my research in recent years has been on two important challenges in automated deduction: 1) how to validate that the complex techniques developed by the community produce correct results; and 2) how to exploit the power of big computer clusters. Although my work has targeted mainly SAT and QBF solving, these challenges are also important for first-order logic and beyond. My first paper on validation of SAT techniques was presented at IJCAR 2012 and my recent paper in this direction received a best paper award at CADE 17. I have been participating in the CADE and IJCAR conferences since 2012 and I was a CADE PC member in 2015 and 2017.

Researchers in the CADE community have created very powerful tools from Lingeling to Vampire to Z3. These tools are successful in industry as well. I am supportive of attracting paper submissions that describe how these tools can make a difference in solving relevant problems. Such papers can have a broad impact. I am also supportive of the requirement that experimental evaluations must be reproducible by the reviewers and the community at large. Although most CADE attendees come from Europe, I would like to stimulate participation from researchers in North America. Organizing CADE regularly in the US or Canada should therefore be continued. Maybe CADE could come back to Austin.

It is with sadness that we note the passing of Mike Gordon, one of the inventors of the Edinburgh LCF system and a central figure in the HOL community, on August 22 2017.

Obituary of the University of Cambridge Computer Laboratory.

Computer Theorem Proving 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 brought 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. This call is open for everyone, also those who did not participate in the workshop.

**Topics 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.

**Important Dates:**

- Submission (full papers): 17 Nov 2017
- Notification of acceptance: 15 Dec 2017
- Revised papers due: 19 Jan 2018

For information about the submission process, see the workshop website.

The field of Symbolic Computation, and its implementation in Computer Algebra Systems, is concerned with the algorithmic determination of exact solutions to mathematical problems. More recent developments in the field of Satisfiability Checking are starting to tackle similar problems, through the use of Satisfiability Modulo Theory (SMT) solvers which exploit technology built for the Boolean SAT problem to other domains.

The two communities now share many central interests, but until recently there has been little interaction between them. Further, the lack of common or compatible interfaces is an obstacle to the fruitful combination of tools. Bridges between the communities in the form of common platforms and road-maps are needed to initiate exchange and support interaction. The aim of this special issue, along with the SC-square H2020 FETOPEN Coordination and Support Activity project, is to document progress, and share knowledge and experience across both communities.

The issue is open for submission and participation to everyone interested in the topics, whether they are members or associates of the SC-square project or not, and whether or not the contribution was discussed at the SC-square workshops.

**Important Dates:**

- Closing date for submissions: 15 February 2018

For information about the submission process, see the project website.

8-9 January, 2018, Los Angeles, USA

Certified Programs and Proofs (CPP) is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates.

**Topics:**
Submissions in research areas related to formal
certification of programs and proofs are welcome. The following is a suggested
list of topics of interests to CPP. This is a non-exhaustive list and
should be read as a guideline rather than a requirement.

- certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors;
- program logics, type systems, and semantics for certified code;
- certified decision procedures, mathematical libraries, and mathematical theorems;
- proof assistants and proof theory;
- new languages and tools for certified programming;
- program analysis, program verification, and proof-carrying code;
- certified secure protocols and transactions;
- certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest;
- certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification;
- certificates for program termination;
- logics for certifying concurrent and distributed programs;
- higher-order logics, logical systems, separation logics, and logics for security;
- teaching mathematics and computer science with proof assistants.

**Important Dates:**

- Abstract submission deadline: Fri 6 Oct 2017
- Full paper submission deadline: Wed 11 Oct 2017
- Notification: Tue 14 Nov 2017

For information about the submission process, see the conference website.

April 17-19, 2018, Newport News, VA, USA

The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.

**Topics include:**

- Formal verification, including theorem proving, model checking, and static analysis
- Advances in automated theorem proving including SAT and SMT solving
- Use of formal methods in software and system testing
- Run-time verification
- Techniques and algorithms for scaling formal methods such as abstraction and symbolic methods, compositional techniques, as well as parallel and/or distributed techniques
- Code generation from formally verified models
- Safety cases and system safety
- Formal approaches to fault tolerance
- Theoretical advances and empirical evaluations of formal methods techniques for safety-critical systems, including hybrid and embedded systems
- Formal methods in systems engineering and model-based development

**Important Dates:**

- Abstract Submission: November 10, 2017
- Paper Submission: November 20, 2017
- Paper notification: January 19, 2018

For information about the submission process, see the conference website.

May 9-11, 2018, Nagoya, Japan

Writing down detailed computational steps is not the only way of programming. The alternative, being used increasingly in practice, is to start by writing down the desired properties of the result. The computational steps are then (semi-)automatically derived from these higher-level specifications. Examples of this declarative style include functional and logic programming, program transformation and re-writing, and extracting programs from proofs of their correctness.

FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.

**Topics include:**

- functional, logic, functional-logic programming, re-writing systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers;
- foundations, language design, implementation issues (compilation techniques, memory management, run-time systems), applications and case studies.

**Important Dates:**

- Abstract Submission: 13 November 2017 (any time zone)
- Submission deadline: 20 November 2017 (any time zone)
- Author notification: 15 January 2018

For information about the submission process, see the conference website.

July 9 - 12th, 2018, Oxford, UK, affiliated with FLoC 2018

FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, proof theory and new emerging models of computation such as quantum computing or homotopy type theory.

**Topics include:**

- Calculi: Lambda calculus - Concurrent calculi - Logics - Rewriting systems - Proof theory - Type theory and logical frameworks
- Methods in Computation and Deduction: Type systems - Induction and coinduction - Matching, unification, completion, and orderings - Strategies - Tree automata - Model checking - Proof search and theorem proving - Constraint solving and decision procedures
- Semantics: Operational semantics - Abstract machines - Game Semantics - Domain theory and categorical models - Quantitative models
- Algorithmic Analysis and Transformations of Formal Systems: Type Inference and type checking - Abstract Interpretation - Complexity analysis and implicit computational complexity - Checking termination, confluence, derivational complexity and related properties - Symbolic computation
- Tools and Applications: Programming and proof environments - Verification tools - Libraries for proof assistants and interactive theorem provers - Case studies in proof assistants and interactive theorem provers - Certification - Applications to security, planning, data bases, etc.

**Important Dates:**

- Abstract Deadline: January 15th, 2018
- Submission Deadline: January 22nd, 2018
- Rebuttal: March 22 - 25th, 2018

For information about the submission process, see the conference website.

July 14-17 2018, Oxford, UK, affiliated with FLoC 2018

IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks.

IJCAR 2018 takes place as part of FLoC 2018 and is the merger of leading events in automated reasoning:

- CADE (Conference on Automated Deduction),
- FroCoS (Symposium on Frontiers of Combining Systems) and
- TABLEAUX (Conference on Analytic Tableaux and Related Methods).

**Topics include:**

- Logics of interest include: propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, type theory, etc.
- Methods of interest include: tableaux, sequent calculi, resolution, model- elimination, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, automated theorem provers, combination of decision procedures, SAT and SMT solving, etc.
- Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, etc.

**Important Dates (provisional):**

- Abstract submission: January 22nd 2018
- Paper submission: January 29th 2018
- Notification: March 29th, 2018

For information about the submission process, see the conference website.

July 14-17 2018, Oxford, UK, affiliated with FLoC 2018

CAV 2018 is the 30th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software 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. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as machine learning, autonomous systems, and computer security. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A selection of papers is expected to be invited to a special issue of Formal Methods in System Design and the Journal of the ACM.

**Topics include:**

- Algorithms and tools for verifying models and implementations
- Algorithms and tools for system synthesis
- Algorithms and tools that combine verification and learning
- 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
- Formal methods for cyber-physical systems
- 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

**Important Dates:**

- Paper submission: January 31st 2018

For information about the submission process, see the conference website.

July 15-17 2018, Oxford, UK, affiliated with FLoC 2018

FM 2018 is the latest in a series of symposia organized by Formal Methods Europe, an independent association that encourages the use of, and research on, formal methods for the engineering of computer-based systems and software. The symposia have been notably successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral work. FM 2018 will take place in Oxford, UK, 15-17 July 2018 as part of FLoC 2018, the Federated Logic Conferences.

FM 2018 will highlight the development and application of formal methods in a wide range of domains including software and integrated computer-based systems. In the latter field, cyber-physical systems, systems-of-systems, human-computer interaction, manufacturing, sustainability, power, transport, cities, healthcare, and biology are of particular interest. We also welcome papers on experiences of formal methods in industry, and on the design and validation of formal methods tools.

**The broad topics of interest for FM 2018 include, but are not limited to:**

- Interdisciplinary formal methods: Techniques, tools and experiences demonstrating formal methods in interdisciplinary frameworks.
- Formal methods in practice: Industrial applications of formal methods, experience with formal methods in industry, tool usage reports, experiments with challenge problems. Authors are encouraged to explain how formal methods overcame problems, led to improved designs, or provided new insights.
- Tools for formal methods: Advances in automated verification, model-checking, and testing with formal methods, tools integration, environments for formal methods, and experimental validation of tools. Authors are encouraged to demonstrate empirically that the new tool or environment advances the state of the art.
- Role of formal methods in software and systems engineering: Development processes with formal methods, usage guidelines for formal methods, and method integration. Authors are encouraged to evaluate process innovations with respect to qualitative or quantitative improvements. Empirical studies and evaluations are also solicited.
- Theoretical foundations: All aspects of theory related to specification, verification, refinement, and static and dynamic analysis. Authors are encouraged to explain how their results contribute to the solution of practical problems with methods or tools.

**Important Dates:**

- Abstract registration: 8 January 2018
- Full paper submission: 22 January 2018
- Notification: 9 April 2018

For information about the submission process, see the conference website.

September 29 - October 2, 2017, Vienna, Austria,
co-located with FMCAD 2017

Over the last decade, the boundaries between computer system components, such as hardware, software, firmware, middleware, and applications, have blurred. This evolution in system design and development practices led in 2014 to a change in the title and scope of the MEMOCODE conference from its original focus on hardware/software co-design to its new focus on formal methods and models for developing computer systems and their components. MEMOCODE's objective is to emphasize the importance of models and methodologies in correct system design and development, and to bring together researchers and industry practitioners interested in all aspects of computer system development, to exchange ideas, research results and lessons learned.

MEMOCODE'17 will be collocated with FMCAD'17, the 17th conference on Formal Methods in Computer-Aided Design, October 2-6, 2017. MEMOCODE'17 and FMCAD'17 will have joint tutorials on October 2.

For information about registration, see the registration website.

October 2-6 2017, Vienna, Austria,
co-located with MEMOCODE 2017

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 ground-breaking 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.

The program comprises presentations of 25 regular papers and 4 tool papers, 3 tutorials and 2 keynotes, a student forum, the Hardware Model Checking Competition, and a symposium in memoriam Helmut Veith.

**Important Dates:**

- Registration Deadline: September 29, 2017

For information about registration, see the conference website.

October 9-11 2017, Namur, Belgium, co-located with
LOPSTR 2017

PPDP 2017 is a forum that brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification.

For information about registration, see the conference website.

October 10-12 2017, Namur, Belgium, co-located with PPDP 2017

The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress. Formal proceedings are produced only after the symposium so that authors can incorporate this feedback in the published papers.

For information about registration, see the conference website.

October 18-22 2017, Miami, USA

The 3rd Global Conference on Artificial Intelligence (GCAI 2017) will be held in Miami, USA, at the Courtyard Marriott hotel in Coconut Grove, 18-22 October 2017. The conference, which addresses all aspects of artificial intelligence, is being organized by LRG and the University of Miami. The program chairs are Christoph Benzmüller, Christine Lisetti and Martin Theobald. The conference chair is Geoff Sutcliffe.

**Important Dates:**

- Early registration: October 1 2017

For information about registration, see the conference website.

November 13 - 15 2017, Haifa, Israel

HVC is an annual conference dedicated to advancing the state-of the art and state-of-the-practice in verification and testing. At the conference, researchers and practitioners from academia and industry network, share ideas, and ponder the future directions of testing and verification for hardware, software, and complex hybrid systems.

The common goal of the conference topics and participants is to ensure the correct functionality and performance of complex systems. HVC is the only conference that brings together experts from all verification and testing sub-fields, thereby encouraging the migration of methods and ideas among domains.

For information about registration, see the conference website.

June 11-13 2018, Cagliari, Italy

The last installment of AsubL (Algebra and Substructural Logics) took place in Melbourne in December 2014. AsubL Take 6 will take place in Cagliari, from the 11th to the 13th of June, 2018, as a workshop in the framework of SYSMICS: SYntax meets Semantics: Methods, Interactions, and Connections in Substructural logics. Further information concerning the webpage, the venue, a tentative programme, a list of invited speakers, and a call for papers will be circulated presently. Following the informality tradition that characterised all past editions of AsubL, there will be no officially appointed scientific committee or organising committee. Potential participants, however, can contact Francesco Paoli or Antonio Ledda for information.

December 17 - 21, 2017, Jerusalem, Israel

Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies have resulted in catastrophic failures. The goal of formal verification is to to improve the safety and reliability of such hardware and software systems.

Formal Verification is the study of algorithms and structures applicable to the verification of hardware and software designs. It draws upon ideas and results from logic, graph theory, and automata theory, and combines theoretical and experimental aspects. While 30 years ago this was a subject of academic interest only, today, many companies use formal verification as an integral part of the development process.

The IIAS Winter School on Formal Verification would bring together several leading researchers to cover the mathematicall and algorithmic foundations of the field, as well as to discuss its application in industry, and its impact on related areas in computer science.

**Confirmed speakers of the winter school:**

- Thomas A. Henzinger: Rabin Lecture
- Christel Baier: Probabilistic verification
- Javier Esparza: Linear-time verification
- Bernd Finbeiner: Temporal synthesis
- Orna Grumberg: SAT-based model checking
- Danny Dolev: Cybersecurity
- David Harel: Computational Biology
- Noam Nissan: Algorithmic Game Theory
- Industrial Formal Verification Panel: Shirit Schvartzblat (Mellanox), Cindy Eisner (IBM), Gila Kamhi (GM)
- Historical lecture by Moshe Vardi: From Aristotle to the iPhone

**Important Dates:**

- Application Deadline: October 1, 2017
- Notification of acceptance will be sent by email by November 1, 2017

For information about registration, see the registration website.

We are looking to fill two permanent (subject to a probation period) roles in the broad area of employing reasoning-based techniques directly to program analysis for security properties, or to the verification of security-related protocols or algorithms. The focus on reasoning-based methods is targeted to complement our world-leading status in automated reasoning. The two positions reflect our desire to establish a new research area.

For full details and how to apply see here (the closing date is 30th September). For any questions please contact Andrei Voronkov and Giles Reger.

(For non-UK readers: the position of Lecturer corresponds to Assistant Professor, but note that this is a tenured position.)

Computer Aided Verification(succeeding Helmut Veith) at TU Wien

The TU Wien (Vienna University of Technology) invites applications for a full professorship at the Faculty of Informatics. The position is affiliated to the Institute of Information Systems. The candidate will become the head of the already existing and valid established research group Formal Methods in Systems Engineering, previously headed by Helmut Veith. The estimated starting date is October 1, 2018.

Application deadline is **October 16, 2017.**
Further details on the position and requirements.

We are offering a PhD position on the integration of automated provers in proof assistants at the Laboratory on Specification and Verification (LSV) of the University Paris Saclay, supervised by Frederic Blanqui and Guillaume Burel.

To widen their use, proof assistants needs more automation. This can be performed by calling external automated theorem provers. Centered around Dedukti, a proof checker for the universal logical framework Lambda-Pi-calculus modulo theory, the objective is to design a proof environment that is able to call external provers to build part of the proof. The global architecture must emphasize the need to have a correct and exhaustive proof once the portions proved externally are glued together. From Dedukti to external provers, proof obligations in the Lambda-Pi-calculus modulo theory must be passed in an efficient way, either by encoding them or by extending the external prover to accept them. Reciprocally, proofs or proof traces produced by these tools needs to be reconstructed back into Dedukti.

- Deadline for application:
**29 October 2017**. - Deadline for PhD start: 1st January 2018.

Starting in October 2017, the programming languages group at University of Freiburg, Germany, has an opening for a research assistant to work with Prof. Dr. Peter Thiemann. This position can be filled with a graduate working towards a PhD or with a PostDoc and it involves a light amount of teaching. We welcome applications of either kind.

**Research**

The overall research theme of the group is to explore the boundaries
of static and dynamic checking of program properties.

- Theoretical and practical aspects of typed programming, for example session types, gradual typing, dependent types, type-based program analysis
- Language-based security, in particular hybrid information-flow enforcement
- Runtime verification and contract checking

We are working in the context of JavaScript, Haskell, OCaml, Scala, and admit the occasional excursion to Java and Go. We collaborate with leading researchers worldwide. Check our research webpage or DBLP publication profile for more information.

**Requirements**

- University degree in computer science or closely related field
- Motivation to work on abstract theories and put them in practical implementations
- Fluent English (speech and writing)

**Job Details and Application**

The salary is according to the TV-L E13 scale of German public service.

The university of Freiburg aims at increasing the number of female employees and thus especially welcomes applications of female candidates.

Applications of disabled candidates will be given priority, depending on their suitability.

Please send your application in PDF format by email to the leader of the programming languages group, Prof. Dr. Peter Thiemann. Applications will be considered until the position is filled.

Informal enquiries about the position may also be sent to Prof. Dr. Peter Thiemann (web page)

The Chair MAIS at TU Darmstadt, led by Heiko Mantel, is offering multiple Postdoc and Ph.D. positions. We are looking for researchers who are interested in addressing foundational problems that will be of practical relevance or in addressing practical problems based on formal methods. The research focus shall be on software security, concurrency, or their combination.

The research focus shall be on one of the following topics:

- modular reasoning about information-flow security
- sound program analysis under relaxed consistency guarantees
- sound re-engineering of code for more parallelism
- definition of security requirements and security policy languages

Your research shall be based on solid theoretical foundations and could result, e.g., in foundational insights, in program analysis and transformation techniques, in tools that are reliable and efficient, in instructive case studies, or in verified critical software systems.

For more information about the positions, about the four research topics and about how to apply, see this web page.