# Association for Automated Reasoning

October 2019

## From the AAR President, Larry Wos

I am occasionally asked whether many readers of the AAR Newsletter try to meet the various challenges I offer and whether areas of mathematics are more interesting than areas of logic.

The answer is, I don't have enough evidence immediately in hand. But sometimes, a reader does ask for what might be termed a follow-up to an earlier column I have written.

In particular, a recent column I wrote on Boolean algebra led to a reader's asking about circle of proofs. In response, I focus here on Moufang loops and equations that define that area of mathematics, and yes, the question about the finding of a circle of pure proofs.

As background, decades ago I was told by a colleague at Argonne National Laboratory, that three equations had the property that, adjoining each alone to some other axioms, produced an axiom set of Moufang loops. That colleague also informed me that a question regarding the three equations remained unanswered. When I told the mathematician Ken Kunen about my intention to address that question, he informed me -- or asked, actually -- about a fourth equation to consider. Specifically, a proof existed that the first equation sufficed to deduce the second and that the second sufficed to deduce the third, but -- and here was the problem -- in order to deduce the first from the third to complete this circle of proofs, two more proofs were needed: a proof deducing the second from the third and then a proof deducing the first from the second.

So, rather than the pleasing existence of the sought-after three proofs for the circle, I sought a circle of pure proofs for four equations, the following. (I include more information than needed, noting that the percent sign means that from there to the end of the line is comment.)

```x = x.
x * rs(x,y) = y.   %  right solvable
rs(x, x * y) y.  %  right solution is unique (implies left = cancellation)
ls(x,y) * y = x.   %  left solvable
ls(x * y , y) x. %  left solution is unique (implies right = cancellation)
%  identity:
1 * x = x .
x * 1 = x.
%  left cancellation
%  x*y != u  |  x*z != u  |  y = z.
%  right cancellation
%  y*x != u  |  z*x != u  |  y = z.
%  Axiom, Moufang 1:
%  (x * y) * (z * x) = (x * (y * z)) * x.
%  Axiom, Moufang 2:
%  ((x * y) * z) * y = x * (y * (z * y)).
%  Axiom, Moufang 3:
%  x * (y * (x * z)) = ((x * y) * x) * z.
%  Axiom, Moufang 4:
%  x * ((y * z) * x) = (x * y) * (z * x).
%  A consequence of left and right surjective:
%  It's all that is needed here.
%  x * R(x) = 1.
%  L(x) * x = 1.
%  The following negate left and right inverse.
%  y * e != 1.
%  actually, L and R turn out to be the same in a Moufang loop
```

Your challenge (in effect, four challenges) consists in finding four proofs. You might begin by seeking a proof that, from the basic axioms with the Moufang 1 adjoined, you can deduce Moufang 2, with no constraint. Let that be your first challenge.

For the next three challenges, find proofs of Moufang 3 from Moufang 2, Moufang 4 from Moufang 3, and Moufang 1 from Moufang 4, each proof with no constraint.

Then, for the more exciting set of challenges that are consistent with the questions that were open, find the given circle of proofs, but find pure proofs. In other words, the proof of the second from the first must avoid the use of Moufang 3 and Moufang 4 to be pure.

Depending on the program you use -- I had in mind that you would be using an automated reasoning program to meet the challenges -- the last line of each proof might be the so-called flip of the goal. In other words, rather than proving s = t, your program proves t = s. If such is the case, the further challenge -- and not trivial according to my research -- is to prove the various Moufang items as given.

If you have used a Knuth-Bendix approach, the final set of challenges asks for proofs that are free of demodulation and that are forward, rather than backward or bidirectional. If you succeed in finding the four proofs for the circle of pure proofs, you will discover, I feel rather sure, that their lengths differ sharply.

## Guest column: Report on the ARCADE workshop 2019

As a forum for discussions and for sharing new ideas centered on automated reasoning, the second ARCADE workshop was held as a satellite event of CADE-27 in Natal. Building on the success of the first ARCADE 2017 in Gothenburg, this workshop encouraged non-technical position statements of 2-4 pages revolving around challenges, applications, directions, and exemplary achievements in automated reasoning.

Out of 12 submitted abstracts, the program committee selected 11 for presentation and discussion at the event. With 33 registrations and even more attendees, ARCADE was one of the largest workshops at CADE. In fact, several people booked the flight to Brazil only or mainly to attend ARCADE.

The workshop was divided into five topic blocks, consisting of one or two talks each.

• The first session was devoted to semantic vs. syntactic inference, where Christoph Weidenbach posed the challenge of unifying these two paradigms, and John Hester presented his approach of using axiom schemata for automated reasoning in first-order set theory.
• In a session under the loose motto of machine learning applications in theorem proving, Claudia Schon presented a novel approach to common sense reasoning and raised questions about deduction vs. abduction and the presentation of knowledge bases in this setting. Sarah Winkler posed questions about the right granularity of features in machine learning for theorem proving.
• The automation of higher-order reasoning was the topic of the third session, where Sophie Tourret reported on the achievements and challenges in the ambitious Matryoshka project and raised the question on what level of higher-order is actually required in practice.
• The fourth session focused on ethical aspects of automated reasoning. Christoph Benzmüller proposed the quest of machine ethics as a new application area for automated reasoning and Matthew Peveler proposed the modelling of ethical principles as an application area for quantified modal logic.
• The fifth session circulated around the challenge to make AR tools useful in practice. Martin Riener argued that automated first-order theorem provers should be optimized for the use in tool chains like SAT solvers are, in order to enhance their versatility. Next, Martin Suda filled in for Giles Reger in making the point that tailoring AR tools to competitions like CASC does not necessarily maximize their applicability in real-world scenarios and that other measures than just the total number of solved problems from some benchmark should be taken into account.
• Finally, further new application areas were the topic of the last session. Pedro Quaresma presented challenges for automated reasoning tools within geometry software, while Alessandro Gianola pointed out that the verification of data-aware processes offers interesting new problems to the AR community.

All papers can be found on the ARCADE 2019 website. As organizers we are currently working on finding a platform to publish post-proceedings. To that end, authors will be invited to update and extend their original submissions while taking into account the feedback received during the event.

In summary, ARCADE 2019 offered a lively atmosphere for vivid discussions on a variety of current topics. We recommend to all of you readers to participate in the next edition of ARCADE - it’s exciting, fun, and there’s going to be a great dinner afterwards!

As organizers, we thank the authors for their interesting and thought-provoking input, and the audience for engaging in such animated and cheerful debates. We are, moreover, grateful to Pascal Fontaine, Christoph Weidenbach, and the local organizers for their great support in all kinds of organizational issues.

## Herbrand Award 2020: First Call for Nominations

Philipp Rümmer
Secretary of AAR and CADE Inc.
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)
• Lawrence C. Paulson (2017)
• Bruno Buchberger (2018)
• Nikolaj Bjørner and Leonardo de Moura (2019)

A nomination is required for consideration for the Herbrand Award. Nominations can be submitted at any time. The deadline for nominations to be considered for the Herbrand Award 2020 (which will be given at IJCAR 2020) will be in spring; however, we encourage people to prepare nominations early and not delay submission until the deadline! Nominations pending from previous years must be resubmitted in order to be considered.

For more details, please check the Herbrand Award webpage.

Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), 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.
with copies to
Philipp Rümmer, Secretary of AAR and CADE Inc.

## Announcement of CADE Trustee Elections

Philipp Rümmer, Secretary of AAR and CADE

The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand Award selection committee, instituting new awards, etc.

The current members of the board of trustees are (in alphabetical order):

The terms of Jasmin Blanchette, Laura Kovács, Renate Schmidt, and Christoph Weidenbach end.

We are therefore seeking to elect four trustees.

An election will be held soon and all CADE members will receive a ballot.

The following candidates were nominated and their statements, in alphabetic order, are below:

### Nominee statement of Maria Paola Bonacina

It is a pleasure and honor to be nominated for the CADE board of trustees. CADE is my home conference: I attended it for the first time right after receiving my undergraduate degree, and I attended most editions since then. Automated deduction is at the heart of my research programme on the concept, design, implementation, and evaluation, both empirical and machine-independent, of methods for automated theorem proving, satisfiability modulo theories, and their integrations.

I served as AAR Secretary (1997-2004), CADE Secretary (1999-2004), CADE trustee (2004-10 and 2013-16), IJCAR Steering Committee Chair (2002-04 and Dec. 2009-Dec. 2010), Program Committee Chair of CADE-24 (2013), and CADE President (Dec. 2009-Dec. 2010 and 2013-16). As President, I led the trustees in instituting the Thoralf Skolem award, the CADE Best Paper award, and the SAT/SMT/AR Summer School. Early on, I was involved with the democratic reform of CADE, and was a founder of IJCAR, writing the IJCAR 2001 and 2004 manifestos. I always supported funding for the Woody Blesdoe Student Travel Award and geographical balance of conference locations.

I am in favor of co-locations for both CADE and IJCAR, and for more events in IJCAR: I am thrilled that ITP rejoins IJCAR in 2020. I am in favor of instituting a CADE Student Best Paper award for papers whose authors are all students, of extending the Skolem award to IJCAR, and engaging CADE/IJCAR on climate change (e.g., SIGPLAN and Climate Change). My vision for our conferences is to strive for scientific excellence, nurturing creativity, cross-fertilization of ideas, openness to both new theoretical paradigms and new applications, preserving historical ties (e.g., FLoC) while being open to new ones. We need to keep working on the visibility, recognition, and attractiveness of our field.

Being a CADE trustee is about service and leadership, or leadership understood as service in the highest sense. It is about listening, remembering, foreseeing consequences, taking responsibilities, ensuring communication and transparency. If elected, I would bring to the board experience, institutional memory, and my unfaltering enthusiasm and energy for our ever fascinating research field. More information on my research and professional service can be found at http://profs.sci.univr.it/~bonacina/.

### Nominee statement of Pascal Fontaine

My research covers various aspects of automated deduction, both theoretical and practical, mostly focused around SMT. CADE is my home conference; I attend CADE and IJCAR whenever possible. I particularly like CADE's tradition to welcome results on both theory and practice of automated reasoning. It is most necessary to provide visibility to implementation works, since they are very time consuming and of uttermost importance to validate theory and for applications. CADE should also not overlook more theoretical aspects that may have a less immediate but a longer term impact on automation of logic. Finally, automated deduction should not be understood in too tight a sense, and CADE should continue encouraging submissions from all fields where logic-based computer assisted reasoning is of importance.

My impression is that CADE, while being the major forum on automated deduction, is a particularly friendly and open conference. CADE should remain so. This requires continuous efforts. Supporting the younger members of our community should be a major objective for the Board of Trustees. The Board of Trustees has had a positive influence in this direction in the past — by setting up or encouraging, e.g. the Woody Bledsoe Awards, tutorials, summer schools, and best student papers — and should continue to actively support younger scientists, and be attentive that CADE remains open and friendly.

The current cycle of conferences, CADE alternating with IJCAR, and IJCAR as a part of FLoC every four years, is, I believe, the right organization for the current situation, since it preserves the specificity of CADE and of the other compound conferences of IJCAR. I however firmly think that there should be a tighter coordination between CADE and the friend conferences like FroCoS, ITP, and Tableaux, e.g. to adjust dates and locations. This will benefit everybody.

### Nominee statement of Laura Kovács

My research focuses on the combination of automated reasoning and symbolic computation for automating program analysis. Since 2010, I became the co-developer of the first-order theorem prover Vampire, leading the development of Vampire to support applications of program analysis. Hence, my interest covers both theoretical and practical aspects of automated reasoning. My research is mainly supported by an ERC Starting Grant 2014, Wallenberg Academy Fellowship 2014 and ERC Proof of Concept 2018.

I have been regularly attending CADE since 2008 and I became really active in the organization of CADE since 2016. In 2016, I had the honor of becoming a CADE Trustees. In my years as a trustee, I was mainly focused on two activities:

1. I organized events to increase the participation of early-stage researchers, in particular master and PhD students, in CADE and related venues. I have initiated the deduction mentoring workshops, with the goal of giving career advices and encouraging students to pursue research in automated reasoning. In 2018 this workshop was organized together with the verification mentoring workshop of CAV 2018, and in 2019 as an affiliated workshop of CADE 2019. I also lectured at the SAT/SMT/AR summers schools in 2018 and 2019, motivating students and participants to engage more in the theory and applications of automated reasoning. Since 2014, we are organizing the Vampire workshop series, with a particular emphasis at finding synergies between reasoning approaches in various logical fragments - we especially encourage master/PhD students to present their work at these workshops!
2. I was involved in the working group re-shaping the process of deciding the winners of the Herbrand Award, the most prestigious award of our community. Our proposed change was accepted and used in 2019. While I agree that the proposal needs further refinements (just like any other process), I believe that our changes better serve the interest of our community.

If I am elected as a CADE trustee again, I would further be determined to organize events supporting the career development of early-stage researchers. I believe that having more PhD/master students attending CADE is crucial, allowing "fresh-(wo)men" in automated reasoning to interact with more senior researchers in the field. I am therefore committed to further continue the tradition of the Woody Bledsoe student travel grants at CADE. I also plan to turn the deduction mentoring workshops (DeMent) into a workshop series, regularly taking place at CADE/IJCAR.

CADE should further maintain the balance between theoretical work, applications and tools. I very much support the organization and maintenance of the CASC System Competition. I would further be committed to strengthen the relation between CASC and SMT-COMP, given that reasoning about theories and quantifiers is a common hot topic in both competitions.

Automated reasoning techniques and tools are increasingly used in related areas, such as systems security, software verification, symbolic computation, and machine learning. I would therefore pay a special attention in strengthening the connection to top conferences in related areas, such as ISSAC, CAV, POPL, CSF, to only name a few.

I would also try to organize other applications-oriented events affiliated with CADE, similar to the very successful industry session "Formal Methods in Industry" at FLoC 2018. My aim with such events would be to have leading experts discussing challenges of using automated reasoning in industry, while also covering business perspectives of automated reasoning.

### Nominee statement of Aart Middeldorp

I have been attending CADE since 1994. I presented several papers at CADE and IJCAR and served on many program committees. Together with Amy Felty, I served as PC chair of the highly successful 25th edition in Berlin.

After spending more than ten years in Japan, since 2003 I lead a research group on computational logic in Innsbruck, in which automated deduction plays an important role. System descriptions and competitions (CASC) are an essential part of CADE. Several software tools (on certification, confluence, theorem proving, to name a few) are developed in Innsbruck and we initiate/organize/host competitions (CoCo, TermCOMP) and workshops (IWC, WST) to advance the development of tools.

One of the most important topics that needs to be addressed by the CADE trustees is the publication forum of the proceedings. More and more national funding agencies insists on open access publications. The current situation is very unsatisfactory. Open access is essential to ensure that CADE stays an attractive conference in the future. Springer charged authors 806,40 euros for gold open access for a CADE-27 paper. If this is not immediately paid by a funding agency (FWF in my case), authors are at the receiving end of several aggressive if not threatening email messages by Springer. This has to stop! If CADE cannot get a deal with Springer like ETAPS, where all published papers appear in gold open access, then I will actively push for a change of publication forum if elected as CADE trustee.

I further think CADE should adopt ideas implemented in other conferences, like welcoming short papers that describe interesting ongoing research, shortening talks to have more papers presented and thus more people attending. Moreover, tool submissions should come with artifact evaluation and the tools should be made available to the community.

### Nominee statement of Renate Schmidt

I have had the privilege of serving on the board of trustees in 2008-2015 and 2016-2019. I was PC Chair of CADE-22, member of the Skolem award committee 2017 & 2019. I serve, or have served, on various other Steering Committees (TABLEAUX 2014-2019, FroCoS 2012-2019, BLC 2017-2019, PAAR since 2014). I therefore appreciate the important function of the board in securing good conference locations, appointing PC Chairs, constituting award committees, ensuring the success of various other activities in our area and providing leadership and representation for the area of automated reasoning.

If re-elected I will continue to focus my efforts in arguing for integrity, representativeness and responsibility in the workings of the board of trustees and the processes of all our various awards, and will continue to push for a review and revision of the new Herbrand Award process. In the interest of avoiding misunderstanding, there is no question the right persons have won the award and the working of the Herbrand Award Committee was beyond question. My issues relate to the timing of the appointment of the Herbrand award committee (after nominations have been received), the balance in the committee, its size, insufficient awareness and consideration of subtle conflicts and the creation of consequences, which carry the risk of diminishing the standing of the award and the credibility of the trustees (and would be detrimental for the community).

In this extraordinary time of blatant inaccuracy, positive misinformation and decline of moral frameworks, as academics and scientists we must defend basic scientific values and don't become complacent in upholding the interests and integrity of every member in every of the diverse subareas of automated deduction, awards winners, trustees, our conferences, the community as a whole and science in general.

My background
My main research involves the development and theoretical analysis of reasoning methodologies and automated reasoning tools as well as applying these in areas such as artificial intelligence, knowledge representation, agent-based systems and mathematics. At present a very strong focus of my work is the development of tools for transforming ontologies such as forgetting, abstraction, difference tracking, information hiding and hypothesis generation.

Other professional activities include (co-)chairing and (co-)organising various international conferences and workshops, and (co-)editing several books, conference/workshop proceedings, and special journal issues. I serve on the editorial boards of the Journal of Automated Reasoning, the Journal of Artificial Intelligence Research and the Journal of Applied Non-Classical Logic.

### Nominee statement of Christoph Weidenbach

I'm a long standing member of the CADE community and have been the elected CADE president for the past three years. During this time the trustees and I have initiated a number of actions to further strengthen the impact of the CADE community. In addition to the support of senior researchers through the Skolem and Herbrand award, we have started measures for young researchers. The new and successful ARCADE workshop series serves as a forum for discussion at a lightweight entry level. It also offers the possibility for young researchers to have their first appointment as a workshop chair, supported by the trustees. The trustees further decided that student fees for the conference will now always include all social events, there will always be a best paper and best student paper award at CADE, and we will announce an automated reasoning PhD award by end of this year. Finally, and in particular through great commitment by our treasurer Neil Murray, we have founded CADE Inc at the state of New York without disturbing any financial operations. This step was necessary after CADE Inc. was dissolved by the state of Illinois. In case I'm re-elected I will continue my work on strengthening CADE as the prime conference on automated deduction.

## Vote by CADE Members on a change to the CADE STV Algorithm

Christoph Weidenbach
Philipp Rümmer
Secretary of AAR and CADE Inc.

For both above reasons, the CADE trustees suggest to move from the CADE STV algorithm to a standard algorithm that is supported by automatic voting platforms. We do not want to include the new algorithm in the bylaws because it will make any future change as difficult as this one. Instead the used algorithm will be made public on the CADE homepage outside the bylaws.

A vote on this motion will be held in conjunction with the 2019 CADE trustee election, and all CADE members will receive a ballot.

Technically, the CADE trustees suggest to change the bylaws as follows:

1. Changing Article (IV) Section 2.3 of the bylaws from
(CURRENT)
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected via email by the entire CADE membership using the Single Transferrable Vote system. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
to
(NEW)
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected electronically by the entire CADE membership. The CADE trustees decide on a voting procedure for the trustee election. The procedure will be published on the CADE homepage. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
2. Remove the CADE STV algorithm from the bylaws.

## Proposals for Sites for CADE-28 in 2021 Solicited

Christoph Weidenbach
Philipp Rümmer

We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2021. 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.

The deadline for proposals is 30 November 2019.

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
• 2012: IJCAR 2012 in Europe
• 2013: CADE-24 in North America
• 2014: IJCAR 2014 as part of FLoC in Europe
• 2016: IJCAR 2016 in Europe
• 2018: IJCAR 2018 in Europe
• 2019: CADE-27 in South America

The upcoming CADE/IJCAR event will be:

• 2020: IJCAR 2020 in Europe

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 deadline.

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

1. National, regional, and local AR community support:
• CADE Conference Chair and host institution,
• availability of (and reward for) student-volunteers.
2. National, regional, and local government and industry support, both organizational and financial.
3. Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
4. 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).
5. 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.
6. 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.
7. 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.
8. Balance with regard to the geographical distribution of previous conferences.

Prospective organizers are encouraged to get in touch with the CADE Secretary and the CADE President 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 are encouraged.

## Journal Special Issues

### Special Issue on "Conceptual Structures 2019" in Information

The mission of ICCS is to harmonize the creativity of humans with the productivity of computers. The conference advances the theory and practice in connecting the user's conceptual approach to problem solving with the formal structures that computer applications need to bring their productivity to bear.
Simon Polovina

This Special Issue, which grew out of the International Conference on Conceptual Structures (ICCS 2019), focuses on the formal analysis and representation of conceptual knowledge, at the crossroads of artificial intelligence, human cognition, computational linguistics, and related areas of computer science and cognitive science. Recently, graph-based knowledge representation and reasoning (KRR) paradigms are getting more and more attention. With the rise of quasi-autonomous AI, graph-based representations provide a vehicle for making machine cognition explicit to its human users. Conversely, graphical and graph-based models can provide a rigorous way of expressing intuitive notions in computable frameworks. The aim of the ICCS 2019 conference is to build upon its long-standing expertise in graph-based KRR and focus on providing modeling, formal, and application results of graph-based systems. The Special Issue welcomes contributions from a modeling, application, and theoretical viewpoint:

• Modeling results will investigate concrete real world needs for graph-based representation, for example (but not exclusively) how human cognition can be mapped onto and facilitated by graphical representations, how certain use cases are of interest to the graph community, how using graphs can bring added (business) value, what kind of graph representation is needed for a given case, etc.;
• Papers reporting on application experience will be expected to demonstrate the benefits of the graph-based proposed solutions in the context of the use case studied. Where appropriate, the graph-based solutions are compared to other possible solutions;
• Technical results will include fundamental graph theory based results for novel structures for representation, extensions of existing structures for added expressivity, conciseness, optimization algorithms for reasoning, reasoning explanation, etc.

Topics:

• Graph-based models and tools for human reasoning
• Existential and conceptual graphs
• Formal concept analysis
• Philosophical, neural, and didactic investigations of conceptual, graphical representations
• Knowledge architecture and management
• Human and machine reasoning under inconsistency
• Human and machine knowledge representation and uncertainty
• Contextual logic
• Constraint satisfaction
• Decision making and argumentation
• Ontologies
• Semantic Web, Web of Data, Web 2.0
• Social network analysis
• Conceptual knowledge acquisition
• Data and text mining
• Conceptual structures in natural language processing and linguistics
• Metaphoric, cultural or semiotic considerations
• Resource allocation and agreement technologies

Submission Information:
Manuscripts should be submitted online at www.mdpi.com by registering and logging in to this website. Manuscripts can be submitted until the deadline. All papers will be peer-reviewed. Accepted papers will be published in the journal (as soon as accepted) and will be listed together on the special issue website. Research articles, review articles as well as short communications are invited. For planned papers, a title and short abstract (about 100 words) can be sent to the Editorial Office for announcement on this website. Submitted manuscripts should not have been published previously, nor be under consideration for publication elsewhere (except conference proceedings papers). All manuscripts are thoroughly refereed through a single-blind peer-review process. The submissions must contain at least 30% new material for being accepted in this journal. Please visit the link in the beginning of the email for further details.

Deadline for manuscript submission: 31 January 2020

## Conferences: call for workshops

### FSCD-IJCAR - call for workshop proposals

29 June, 4-5 July 2020, Paris, France

FSCD 2020 will be the fifth edition of the International Conference on Formal Structures for Computation and Deduction. IJCAR 2020 will be the tenth International Joint Conference on Automated Reasoning.

We invite proposals for workshops, tutorials or other satellite events, on any topic to related formal structures in computation, deduction and automated reasoning, from theoretical foundations to tools and applications.

Satellite events will take place on the 29 June and 4-5 July, before and after the main conference (30 June - 5 July). It is expected that satellite events would run for 1 or 2 days, and be open to participants of parallel events.

Proposals
Proposals must be limited to three pages and should be submitted by email to the workshop chairs. Each proposal should consist of the following two parts.

1. A description part including:
• a short scientific justification of the proposed topic, its significance, and the particular benefits of the workshop to the community, as well as a list of previous or related workshops (if relevant);
• a brief description (up to 120 words) of the event for the website and publicity material.
2. An organisational part including:
• contact information for the workshop organizers;
• proposed affiliated conference;
• estimate of the number of workshop participants;
• proposed format and agenda (e.g. paper presentations, tutorials, demo sessions, etc.)
• potential invited speakers;
• procedures for selecting papers and participants;
• tentative schedule for paper submission and notification of acceptance;
• plans for dissemination, if any (e.g. a journal special issue);
• duration (which may vary from one day to two days);
• preferred period (pre, or post main conferences);
• any other special requirements.
The Organizing Committee of FSCD-IJCAR will determine the final list of accepted workshops based on the recommendations from the Workshop Chairs of the hosting conferences and availability of space and facilities.

The organizers of satellite events are expected to create and maintain a website for the event; handle paper selection, reviewing and acceptance; draw up a tentative programme of talks; advertise their event through specialist mailing lists; prepare the informal pre-proceedings (if applicable) in a timely fashion; and arrange any post-proceedings. Some amount of financial support may be offered to workshops, depending on the number of participants.

The FSCD-IJCAR organizing committee will handle promotion of the event on the main conference website; integration of the event's programme into the overall timetable; registration of participants; arrangement of an appropriate meeting room; and provision of lunch and coffee breaks for participants.

Important Dates

• Submission of workshop proposals: 15 November, 2019
• Notification of success of proposals: 1 December, 2019
• Main conference: 30 June - 3 July 2020
• Workshop dates: 29 June, 4-5 July 2020

### ICALP-LICS 2020 Call for Workshops

July 6-7, 2020, Beijing, China

ICALP 2020 and LICS 2020 will take place in co-location from 8th till 12th of July 2020. The conferences will be preceded by two days of joint workshops, held on July 6th and 7th. We invite proposals of workshops affiliated with ICALP-LICS 2020 on all topics covered by ICALP and LICS, as well as other areas of theoretical computer science.

Proposals should be submitted no later than November 30th, 2019 by sending an email to Frederic Blanqui. Due to limited space of the venue we might not be able to accommodate all the proposed workshops. You should expect notification on the acceptance of your proposal by mid December 2019.

A workshop proposal submission should consist of:

• workshop's name and URL (if already available)
• workshop's organizers together with their email addresses and web pages;
• short description of the area covered by the workshop and the motivation behind it;
• expected number of participants (if available, please include the data of previous years);
• planned format of the event;
• date preference (July 6th or 7th).

As for the format, a standard option is a one-day workshop consisting of invited talks by leading experts and of shorter contributed talks, either directly invited by the organizers or selected among submissions. Deviations from this standard are also warmly welcome, including a shorter or a longer time span than a full day, or other elements of the schedule like open problem sessions, discussion panels, or working sessions.

If you plan to have invited speakers, please specify their expected number and, if possible, tentative names. If you plan a call for papers or for contributed talks followed by a selection procedure, the submission date should be scheduled after ICALP 2020 and LICS 2020 notification, while the notification should take place considerably before the early registration deadline. In your submission please include details, in particular the time schedule, of the planned procedure of selecting papers and/or contributed talks. If you plan to have published proceedings of your workshop, please provide the name of the publisher. Please be advised that ICALP-LICS 2020 is not able to provide any financial support for publishing workshop proceedings.

We expect the workshops to be financially independent. The expenses related to the participation of invited speakers, production of workshop materials, etc. should be covered from independent sources. On top of standard ICALP/LICS registration fee there will be a moderate registration fee for the workshops that will cover coffee breaks. This workshop fee will be waived for maximum two invited speakers for each workshop.

## Conferences: call for papers

### IJCAR 2020: 10th International Joint Conference on Automated Reasoning, call for papers

June 29-July 2, 2020, Paris, France

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

IJCAR 2020 will be co-located with the conference FSCD.

IJCAR 2020 is the merger of leading events in automated reasoning:

• CADE (Conference on Automated Deduction),
• FroCoS (Symposium on Frontiers of Combining Systems)
• ITP (Interactive Theorem Proving)
• TABLEAUX (Conference on Analytic Tableaux and Related Methods)

Topics:
IJCAR 2020 invites submissions related to all aspects of automated or interactive reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems or proof assistants are solicited.

IJCAR topics include the following ones:

• - 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 or proof procedures, SAT and SMT solving, integration of proof assistants with automated provers and other symbolic tools, etc.
• - Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, education, formalization of mathematics etc.
The proceedings of IJCAR 2020 will be published by Springer in the LNAI/LNCS series.

Best paper award:
IJCAR 2020 will recognize the most outstanding submission with a best paper award at the conference.

Student travel awards:
Woody Bledsoe Travel Awards will be available to support selected students in attending the conference.

Important dates:

• Abstract submission: January 16 2020
• Paper submission: January 23 2020
• Rebuttal: March 6-10 2020
• Final version of papers due: April 10 2020
• IJCAR Conference: 29th June - 2nd July 2020

### FSCD 2020: 5th International Conference on Formal Structures for Computation and Deduction, call for papers

June 29 – July 5, 2020, Paris, France

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, models of computation, semantics and verification in new challenging areas. The suggested, but not exclusive, list of topics for submission is:

1. Calculi: Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.); Lambda calculus; Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.); Proof theory (natural deduction, sequent calculus, proof nets, etc.); Type theory and logical frameworks; Homotopy type theory; Quantum calculi.
2. Methods in Computation and Deduction: Type systems (polymorphism, dependent, recursive, intersection, session, etc.); Induction, coinduction; Matching, unification, completion, orderings; Strategies (normalization, completeness, etc.); Tree automata; Model building and model checking; Proof search and theorem proving; Constraint solving and decision procedures.
3. Semantics: Operational semantics and abstract machines; Game Semantics and applications; Domain theory and categorical models; Quantitative models (timing, probabilities, etc.); Quantum computation and emerging models in computation.
4. 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.
5. Tools and Applications: Programming and proof environments; Verification tools; Proof assistants and interactive theorem provers; Applications in industry; Applications of formal systems in other sciences.
6. Semantics and Verification in new challenging areas: Certification; Security; Blockchain protocols; Data Bases; Deep learning and machine learning algorithms; Planning.

Important Dates
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.

• Abstract: February 6, 2020
• Submission: February 9, 2020
• Rebuttal: March 27-29, 2020
• Final version: April 27, 2020

### GCAI 2020: 6th Global Conference on Artificial Intelligence, call for papers

April 6-9, 2020, Hangzhou, China

With its special focus theme on "Explainable AI and Responsible AI", the summit intends to promote the interplay between logical approaches and machine learning based approaches in order to make AI more transparent, responsible and accountable.

List of Topics
Submissions in all areas of artificial intelligence are welcome. Suggested topics include, but are not limited to:

• Foundations
• Knowledge representation
• Cognitive modeling
• Perception
• Search
• Reasoning and programming
• Machine learning
• Constraints and uncertainty
• Architectures
• Agents and distributed AI
• Intelligent user interfaces
• Natural language systems and linguistics
• Information retrieval
• Case-based reasoning
• Hierarchical and deep representations
• Affective computing
• Applications
• Aviation and aerospace
• Education and tutoring systems
• Games and entertainment
• Law and machine ethics
• Mathematics and the sciences
• Medicine and healthcare
• Management and manufacturing
• World Wide Web
• Robotics
• Security
• Implications
• Philosophical foundations
• Social impact and ethics
• Evaluation of AI systems
• AI education

Key Dates

• Abstract submission deadline: 23 November 2019
• Paper submission deadline: 30 November 2019
• Acceptance notification: 20 January 2020
• Camera ready copy due: 3 February 2020
• Conference: 6-9 April 2020

### ETAPS 2020: 23rd European Joint Conferences on Theory and Practice of Software, joint call for papers

April 25-30, 2020, Dublin, Ireland

ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of four annual conferences, accompanied by satellite workshops.

Main Conferences (27-30 April)

• ESOP: European Symposium on Programming (PC chair: Peter Müller, ETH Zürich, Switzerland)
• FASE: Fundamental Approaches to Software Engineering (PC chairs: Heike Wehrheim, Universität Paderborn, Germany, and Jordi Cabot, Universitat Oberta de Catalunya, Spain)
• FoSSaCS: Foundations of Software Science and Computation Structures (PC chairs: Barbara König, Univ Duisburg-Essen, Germany, and Jean Goubault-Larrecq, LSV, ENS Paris-Saclay, France)
• TACAS: Tools and Algorithms for the Construction and Analysis of Systems (PC chairs: Armin Biere, Johannes-Kepler-Univ Linz, Austria, and David Parker, University of Birmingham, United Kingdom)

TACAS '20 will host the 9th Competition on Software Verification (SV-COMP).

POST, which was an ETAPS conference 2012-2019, has been discontinued.

Important Dates

• Papers due: 24 October 2019 23:59 AoE (=GMT-12)
• Rebuttal (ESOP, FoSSaCS and, for selected papers, TACAS): 9 December 00:01 AoE - 10 December 23:59 AoE
• Camera-ready versions due: 22 February 2020

Satellite Events (25-26 April)
A number of satellite workshops will take place before the main conferences.

• 25-26 April (two days): CMCS, GALOP, SynCoP, VerifyThis, VPT, WADT, WRLA
• 25 April: CREST, InterAVT, MSFP, TEASE-LP
• 26 April: HCVS, MARS, MeTRiD, PLACES, RW

### ECAI 2020: 24th European Conference on Artificial Intelligence, call for papers

June 8-9, 2019, Santiago de Compostela

The Program Committee of the 24th European Conference on Artificial Intelligence (ECAI 2020) invites the submission of papers for the technical programme of the Conference. High-quality original submissions are welcome from research results and applications of all areas of AI. The following list of topics is indicative; other topics are welcome.

• Agent-based and Multi-agent Systems (MAS)
• Computational Intelligence (CI)
• Constraints and Satisfiability (CS)
• Games and Virtual Environments (GAME)
• Heuristic Search (HEU)
• Human Aspects in AI (HAI)
• Information Retrieval and Filtering (IRF)
• Knowledge Representation and Reasoning (KRR)
• Machine Learning (ML)
• Multidisciplinary Topics and Applications (MULT)
• Natural Language Processing (NLP)
• Planning and Scheduling (PLAN)
• Robotics (ROB)
• Safe, Explainable, and Trustworthy AI (XAI)
• Semantic Technologies (SEM)
• Uncertainty in AI (UAI)
• Vision (VIS)

The Call for Papers is available here.

Workshops, tutorials and other events
In addition to its full programme of technical papers, ECAI2020 will feature many AI-related events for researchers, students and all attendants who are interested on contemporary AI. Separate calls have been issued for:

• Workshop proposals, CFP available here.
• Tutorial proposals, CFP available here.
• PAIS 2020, the Prestigious Applications of Intelligent Systems conference, CFP available here
• STAIRS 2020, the Starting AI Researcher Symposium, CFP available here.
In addition, other AI-related events will be announced, specially addressing the role of AI in Europe (and vice-versa) with special focus on the Conference general theme. Among these, The Frontiers in AI track sessions, the Lab To Market event, the Women in AI Breakfast and the EU Challenges forum.

Futhermore, ECAI2020 will have a special focus on Starting Researchers, who will be able to participate in an specific program including the Doctoral Consortium, the Three Minutes Thesis Competition, the Lunch with an EurAI Fellow and the Job Fair.

Some Important Dates

• ECAI2020 Abstract submission: November 15, 2019
• ECAI2020 Paper submission: November 19, 2019
• ECAI2020 Notification of acceptance/rejection: January 15, 2020
• WORKSHOP Proposal submission: October 30, 2019
• WORKSHOP Proposal notification: November 28, 2019
• TUTORIAL Proposal Submission: February 20, 2020
• TUTORIAL Acceptance Notification: March 20, 2020
• PAIS Abstract submission: November 21, 2019
• PAIS Paper submission: November 26, 2019
• PAIS Notification of acceptance/rejection: January 20, 2020

### CiE 2020: 16th Computability in Europe - Beyond the horizon of computability, call for papers

June 29 - July 3, 2020, Salerno, Italy

CiE 2020 is the 16th conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.

Special Sessions

:
• Algorithmic Learning Theory
• Combinatorial String Matching
• Computable Topology
• History and Philosophy of Computing
• Large scale Bioinformatics and Computational Sciences
• Modern aspects of Formal Languages

Important Dates:

• Deadline for abstract registration: 3 January 2020 AOE
• Deadline for article submission: 17 January 2020 AOE
• Notification of acceptance: 29 February 2020
• Final versions due: 15 March 2020
• Deadline for informal presentations submission: 10 April 2020 (The notifications of acceptance for informal presentations will be sent a few days after submission.)
• Early registration before: 1 May 2020

### LICS 2020: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, call for papers

July 8-12, 2020, Beijing, China

The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric.

Suggested, but not exclusive, topics of interest include:

• 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
• games and logic
• 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
• verification.

Important Dates
Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by anywhere on earth (AoE).

• Titles and Short Abstracts Due: 6 January 2020
• Full Papers Due: 10 January 2020
• Author Feedback/Rebuttal Period: 16–20 March 2020
• Author Notification: 10 April 2020
Deadlines are firm; late submissions will not be considered.

### LATA 2020: 14th International Conference on Language and Automata Theory and Applications, call for papers

March 2-6, 2020, Milan, Italy

LATA is a conference series on theoretical computer science and its applications. LATA 2020 will reserve significant room for young scholars at the beginning of their career. It will aim at attracting contributions from classical theory fields as well as application areas.

Scope:
Topics of either theoretical or applied interest include, but are not limited to:

• algebraic language theory
• algorithms for semi-structured data mining
• algorithms on automata and words
• automata and logic
• automata for system analysis and programme verification
• automata networks
• automatic structures
• codes
• combinatorics on words
• computational complexity
• concurrency and Petri nets
• data and image compression
• descriptional complexity
• foundations of finite state technology
• foundations of XML
• grammars (Chomsky hierarchy, contextual, unification, categorial, etc.)
• grammatical inference, inductive inference and algorithmic learning
• graphs and graph transformation
• language varieties and semigroups
• language-based cryptography
• mathematical and logical foundations of programming methodologies
• parallel and regulated rewriting
• parsing
• patterns
• power series
• string processing algorithms
• symbolic dynamics
• term rewriting
• transducers
• trees, tree languages and tree automata
• weighted automata

• Paper submission: October 26, 2019 – EXTENDED
• Notification of paper acceptance or rejection: November 25, 2019
• Final version of the paper for the LNCS proceedings: December 2, 2019
• Early registration: December 2, 2019
• Late registration: February 17, 2020
• Submission to the journal special issue: June 6, 2020

### TYPES 2019: 25th International Conference on Types for Proofs and Programs, post-proceedings call for papers

TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2019 was held 11-14 June in Oslo, Norway. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings.

Submission to this post-proceedings volume is open to everyone, also to those who did not participate in the conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, not overlapping with published or simultaneously submitted work to a journal or a conference with archival proceedings.

The scope of the post-proceedings is the same as the scope of the conference: the theory and practice of type theory. In particular, we welcome submissions on the following topics:

• Foundations of type theory and constructive mathematics;
• Homotopy type theory and univalent mathematics;
• Applications of type theory;
• Dependently typed programming;
• Industrial uses of type theory technology;
• Meta-theoretic studies of type systems;
• Proof assistants and proof technology;
• Automation in computer-assisted reasoning;
• Links between type theory and functional programming;
• Formalizing mathematics using type theory.

Important Dates

• Abstract submission: 4 November 2019
• Paper submission: 11 November 2019
• Author notification: 25 March 2020

Details

• Papers have to be formatted with LIPIcs style (currently lipics-v2019.cls) and adhere to the style requirements of LIPIcs.
• The upper limit for the length of submissions is 20 pages
• Papers have to be submitted in pdf through EasyChair.
• Authors have the option to attach to their submission a zip or tgz file containing code (formalized proofs or programs), but reviewers are not obliged to take the attachments into account and they will not be published.
• In case of questions, e.g. on the page limit, contact one of the editors.

Editors

### TYPES 2020: 26th International Conference on Types for Proofs and Programs, call for papers

March 2-5, 2020, Torino, Italy

The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming.

The TYPES areas of interest include, but are not limited to:

• foundations of type theory and constructive mathematics;
• applications of type theory;
• dependently typed programming;
• industrial uses of type theory technology;
• meta-theoretic studies of type systems;
• proof assistants and proof technology;
• automation in computer-assisted reasoning;
• links between type theory and functional programming;
• formalizing mathematics using type theory.

We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress.

Important dates:

• submission of 2 pp abstract: 10 January 2020, anywhere on Earth
• notification of acceptance/rejection: 1 February 2020
• camera-ready version of abstract: 15 February 2019

## Workshops

### AITP 2020: Artificial Intelligence and Theorem Proving, call for papers

March 22-27, 2020, Aussois, France

Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.

Topics

• AI, machine learning and big-data methods in theorem proving and mathematics.
• Collaboration between automated and interactive theorem proving, in particular their AI/ML aspects.
• Common-sense reasoning and reasoning in science.
• Alignment and joint processing of formal, semi-formal, and informal libraries, Formal Abstracts.
• Methods for large-scale computer understanding of mathematics and science.
• Combinations of linguistic/learning-based and semantic/reasoning methods
• Formal verification of AI and machine learning algorithms, explainable AI .

Dates

• Submission deadline: December 3, 2019
• Author notification: January 10, 2020
• Conference registration: January 21, 2020
• Camera-ready versions: March 1, 2020
• Conference: March 22 - 27, 2020

May 13-15, 2020, Kyiv, Ukraine

Reasoning is at the very heart of logic, constituting its subject matter. I n the last few decades, there has been considerable progress both in the pu rely logical analysis of reasoning and in applied logical investigations of various concrete subject domains, such as philosophical and scientific dis course, logic programming and everyday communication. Reasoning has been st udied from proof-theoretical as well as semantic standpoints. Along with fu rther elaboration of standard techniques (axiomatic systems, sequent calcul i and natural deduction) a range of other approaches (such as display calcu li, tableaux methods, hypersequent systems, etc.) and semantic modeling of logical systems are being developed. Moreover, there is a powerful traditio n of analyzing and evaluating reasoning patterns by means of informal logic and argumentation theory. Recent advances in these fields, in particular c onstructing theoretical models of argumentation and dialectical systems, ha ve proved promising. The aim of the conference is to bring together scholar s working in various areas of proof-theoretic, semantic, argumentative and informal logic analysis. The topics of interest may include, but are not li mited to:

• modern approaches to proof theory;
• structural proof theory and structural reasoning;
• proof-theoretic methods in non-classical logics;
• proof-theoretic semantics;
• Kripke models and algebraic methods in semantics;
• semantic analysis of non-classical logics;
• semantic modelling of knowledge representation and reasoning;
• provability logic;
• description logic, defeasible reasoning and non-monotonic logic;
• inductive reasoning and probabilistic logic;
• automated reasoning;
• formal models of argumentation;
• abstract argumentation systems;
• argumentation schemes and patterns;
• practical reasoning and argumentation, argumentation in interpersonal communication;
• argumentation in special contexts: finance, medicine, law, policy making, academy, (social) media, etc.;
• dialogue logic, empirical logic, informal logic;
• informal fallacies and cognitive biases in relation to reasoning.

Important dates

• Abstract submission deadline: 06 January, 2020
• Notification of acceptance: 01 February, 2020
• Registration opens: 10 February, 2020
• Early registration closes: 16 March, 2020

### ADSL 2020: 2nd Workshop on Automated Deduction for Separation Logics, call for papers

January 20, 2020, New Orleans, USA

In recent times, the verification of heap-manipulating programs, and static analyses in particular, has seen substantial success, largely due to the development of ‘Separation Logics’ (SLs). SLs provide embedded support for ‘local reasoning’ : reasoning about the resource(s) being modified, instead of the state of the entire system. This form of reasoning is enabled by new syntax (dedicated atomic proposition and separating connectives) and corresponding semantics. Such expressivity comes with the inherent difficulty of automating these logics. Combining this power with induction/recursion allows to concisely specify a large class of recursive data structures and programs, but further increases the computational burden.

The goal of this workshop is to bring together academic researchers and industrial practitioners focused on improving the state of the art of automated deduction methods for Separation Logics. We will consider technical submissions presenting work on the following topics (the list is not exclusive):

• the integration of Separation Logics with SMT,
• proof search and automata-based decision procedures for Separation Logics and sister logics such as Bunched Implication Logic;
• computational complexity of logical problems such as satisfiability, entailment and abduction;
• alternative semantics and computation models based on the notion of resource;
• application of separation and resource logics to different fields, such as sociology and biology.

The workshop is affiliated with the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).

Important dates (AoE):

• Papers due: November 1st
• Workshop: January 20th

### Postproceedings for ThEdu'19 by EPTCS, call for papers

ThEdu's programme comprised one invited contribution and four regular contributions, whose abstract are in the workshop web-page. Now postproceedings are planned to collect the contributions upgraded to full papers. The contributions' topics are diverse according to ThEdu's scope, and this is a call open for everyone, also those who did not participate in the workshop. All papers will undergo review according to EPTCS standards.

THedu'19 Scope:
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 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.

Important Dates

• Submission (full papers): 18 Nov 2019
• Notification of acceptance: 16 Dec 2019
• Revised papers due: 20 Jan 2020

### Formal Methods in Mathematics / Lean Together 2020, call for participation

January 6-10, 2020, Carnegie Mellon University, Pittsburgh, Pennsylvania

The meeting is a successor to Lean Together 2019.

The first three days will focus on formal methods in pure and applied mathematics, including interactive theorem proving, automated reasoning, verification of symbolic and numeric computation, and general mathematical infrastructure.

The last two days will be devoted to specifically to the Lean Theorem Prover and its core library, mathlib. Users and library developers will have opportunities to present work in progress and discuss plans for the future.

Attendance is free and open to the public, but we ask you to let us know by December 6 if you plan to come. If you are tentatively planning to attend, please tell us now and update us if your plans change. You register via the web page above, or contact the organizers, Jeremy Avigad and Robert Y. Lewis.

The meeting is supported by grant FA9550-18-1-0325 from the Air Force Office of Scientific Research. The contents do not necessarily reflect the views of the AFOSR.

## Open Positions

### Postdoc position on Theory reasoning (in Vampire), Manchester, UK

We are welcoming applications for a Postdoc to join the Vampire team in Manchester to work on theory reasoning. There are a number of interesting possible research directions including, but not limited to, extending current successful work on theory instantiation and integration of SMT solvers into proof search. An ideal candidate would have some experience with developing or using theory reasoning techniques.

This role is suitable for those who have recently obtained (or are about to obtain) a PhD as well as those with more experience.

Full job details (and the link to apply) are available here (the job details are found by following a non-obvious link at the bottom of the page)

### Tenure Track Position in Formal Methods at TU Graz, Austria

Graz University of Technology, Department of Computer Science and Biomedical Engineering invites applications for a Tenure Track Professorship in Formal Methods for Dependability.

We are looking for an excellent researcher with a background in formal methods for dependable secure systems. She or he is expected to carry out basic research in formal modeling, analysis, verification and synthesis and is interested in applications to security and/or artificial intelligence.

The professorship will be part of the Institute of Applied Information Processing and Communications and the research focus of the candidate should complement the current faculty positions of the institute.

With 30 years of research in information security, the Institute of Applied Information Processing and Communications (aka IAIK) is a well-established player in the field. More than 60 researchers work on topics like security architectures, side channels, cryptography, formal methods, identity management, and e-government.

Among the recent sparkling highlights of IAIK's research are the processor vulnerabilities known as "Meltdown" and "Spectre". IAIK cryptographers have contributed to major competitions in cryptography, like AES, SHA-3, and CAESAR; these contributions were always shortlisted or even won the competition. IAIK has built a strong presence in formal methods with a focus on reactive synthesis and, more recently, verification of security constructs.

The institute collaborates closely with research groups and industry partners around the globe. The recently announced Cybersecurity Campus Graz also creates a unique local environment. This new hub for information security unites basic research, education, technology transfer, and industry partners all under one roof.

The courses of IAIK typically are among the best evaluated of the computer science curricula. At bachelor's level, these courses are computer organization, operating systems, computer networks, systems programming, logic and computability, and information security.

Requirements
A relevant national or international university education with a completed doctoral/PhD degree.

Expected Qualifications

• Outstanding achievements and potential in research, excellent publication activity and international reputation.
• International experience in the form of a PhD or PostDoc position at an internationally recognized university or research center.
• Experience in the design and implementation of international research projects as well as willingness and ability to establish and lead a research group.
• Enthusiasm for excellent teaching, teaching experience or a teaching concept as well as the ability and willingness to teach in all curricular stages (Bachelor, Master, Doctorate), supervise theses and promote young scientists.

To ensure effective international representation of the research group and its work, excellent spoken and written competence in English is required. Specifically, willingness to teach courses in English is expected. Fluency in German or the willingness to acquire it is also required. The successful candidate is also expected to transfer her/his residence to the area of Graz.

Graz University of Technology aims to increase the proportion of women, in particular in management and academic staff, and therefore qualified female applicants are explicitly encouraged to apply. Until a balanced ratio of men and women has been achieved at the university, preference will be given to women if applicants are equally qualified.

Graz University of Technology actively promotes diversity and equal opportunities. Applicants are not to be discriminated against in personnel selection procedures on the grounds of gender, ethnicity, religion or ideology, age, sexual orientation (Anti-discrimination). People with disabilities and who have the relevant qualifications are expressly invited to apply.

Our Offer
The advertised position is a tenure-track career position for an initial period of 6 years. (pursuant to § 99 para. 5 of the Universities Act) After the conclusion of a qualification agreement, the job holder is appointed as Assistant Professor. After a positive evaluation of the qualification agreement, the position will be turned into a permanent position as Associate Professor. After a further competitive procedure, the promotion to Full Professor is possible. Graz University of Technology provides excellent working conditions in a lively scientific community combined with the outstanding living quality of the Graz area.

We offer an internationally competitive salary based on the profile of the applicant. The formal minimum annual gross salary for the position is € 59.003,00 per year, including social and health insurance. This corresponds to category B1 of the collective agreement for employees of Austrian universities.

Interested applicants are requested to send a detailed application in electronic form, and should quote the position identification number 7050/19/021:

• using the application form,
• including a resume (with copies of diplomas),
• a list of publications with copies of their 5 most important publications,
• a research statement describing past and planned research activities (5 pages max.),
• a teaching statement (5 pages max.) and evaluations of past teaching activities (if available),
in electronic form at the latest by 26 November 2019 (date of email) to the Dean of the Department of Computer Science and Biomedical Engineering of the Graz University of Technology, Roderick Bloem.

The interviews for the position are expected to take place in the week from 27 January 2020. Candidates are asked to be available in this period. For further questions, please contact the Dean’s office.

### PhD and Postdoc positions at Aarhus University (DK)

The Department of Computer Science at Aarhus University, Denmark, offers a considerable number of PhD and PostDoc positions in the areas of Logic, Semantics and Programming Languages. Our research spans a wide spectrum of topics concerning models and logics for programming languages and type theories, language-based security, blockchains, theoretical foundations and practical tools for program analysis, formal verification and model checking.

Aarhus University admits PhD students on the basis of a bachelor's degree (for 5 year PhDs) or a master's degree (for 3 year PhDs). If admitted, all tuition is covered, and a generous stipend is provided. Postdoc positions can be for 1 or 2 years, and with the possibility of renewal (depending on the individual projects and sources of funding).

Interested applicants at all levels are encouraged to contact the respective faculty for details, enclosing a CV and a short description of interests.

• Aslan Askarov (language-based security, web security, type systems, program analysis)
• Lars Birkedal (higher-order concurrent separation logic, type theory, program verification)
• Bas Spitters (computer aided proofs in cryptography, homotopy type theory, formal verification of blockchains)
• Jaco van de Pol (parallel & symbolic model checking, synthesis, graph games)

• Magnus Madsen (programming language design, functional and logic programming, type systems)
• Anders Møller (static & dynamic program analysis, program analysis and automated testing for web and mobile software)
• Andreas Pavlogiannis (algorithmic & computational foundations of model checking, quantitative verification, static & dynamic analysis, concurrency)

Aarhus University is realizing an ambitious multi-phase digitalization initiative which will help prepare researchers, students and the labour force for the digital transition of the future. The initiative aims at significant expansion of the Department of Computer Science for faculty and students.

Information about the PhD program: here.

### Postdoc and PhD positions - Center for Advanced Software Analysis, Aarhus University, Denmark

Several postdoc positions and PhD stipends are available at the Center for Advanced Software Analysis (CASA) at Aarhus University, Denmark, funded by the European Research Council.

The CASA center covers research in program analysis, type systems, testing, language design, and programming tools, with a particular focus on static analysis and automated testing for web and mobile apps.

The postdoc positions are at the level of Research Assistant Professor of Computer Science and are initially for one year, but they can be extended by mutual consent. We welcome researchers with clearly demonstrated experience and skills in one or more of the research areas mentioned above.

The PhD positions include full tuition waiver and a very competitive scholarship. Applications are welcomed from students with either a BSc or an MSc degree. Students with a strong background in Programming Languages will be preferred.

Interested candidates should send an email containing a brief letter of interest and a CV. Applications will be considered until the positions are filled.

### Postdoc Opportunity at Augusta University, Georgia, USA

Ms. Regina White

The formal methods group is led by Paul Attie, Clement Aubert, Harley Eades, and Alexander Schwarzmann. We are interested in state of the art theory and its application. Among our envisaged directions is the application of formal methods to cybersecurity and sophisticated distributed systems (both hardware and software). PhD students who expect to graduate within a year are encouraged to apply.

The formal methods group is located in the Georgia Cyber Center a \$100 M facility which is ``the single largest investment in a cybersecurity facility by a state government to date.'' The Georgia Cyber Center seeks to prove the USA with a ``decisive advantage in cyberspace,'' by means of a unique industry-government-academia partnership. The Georgia Cyber Center hosts companies involved in cybersecurity work, and together with the US Army Cyber Command headquartered in Fort Gordon, Augusta, and local academia, provides a unique ecosystem where challenge problems from military and industry feed into academic research, and research results feed back into industry and government practice.

Please include in your application a CV, a statement of purpose, and contact information for at least three referees.

### 2-year postdoc position on type theory in Birmingham (UK)

Benedikt Ahrens

Benedikt Ahrens would like to invite applications for a 2-year postdoctoral position at the University of Birmingham, School of Computer Science. The postdoctoral researcher will work with Paige Randall North (Ohio State University) and him on a topic in the area of (homotopy) type theory; details can be discussed.

The position is funded by the EPSRC grant "A theory of type theories", PI Benedikt Ahrens.

The starting date of the position is somewhat flexible; it should be between late 2019 and mid 2020.

How to apply
There is no official job opening yet. Interested people are encouraged to contact Benedikt Ahrens by email in the first instance to discuss their research interests and details of the position.

The School of Computer Science has a large and thriving Theoretical Computer Science research group, with a particular focus on category theory and its applications to the logical foundations of computer science. Among our research interests are:

• category theory and higher category theory;
• type theory;
• homotopy type theory and univalent foundations;
• formal proof;
• lambda-calculus and computational effects;
• topology and domain theory;
• constructive mathematics;
• quantum computing;
• semantics;
• program compilation.

The group currently has 12 permanent staff and more than a dozen PhD students. They have a weekly seminar, as well as more informal meetings and reading groups. Information on all of this can be found on their webpage. They are regularly hosting international events in theoretical computer science in general and type theory in particular; recently, this included CSL 2018, 6WFTop, School and Workshop on Univalent Mathematics, and Midlands Graduate School.

### PhD opportunities in formal foundations and verification of distributed systems at the University of Birmingham, UK

The School of Computer Science at the University of Birmingham, UK, is continuously looking for strong PhD candidates. One particular field of interest is formal methods applied to distributed systems. Students broadly interested in this field of research are strongly encouraged to apply. Topics of particular interest are, for example:

• Formal verification of Byzantine fault-tolerant systems
• Probabilistic formal verification of distributed real-time systems
• Using knowledge reasoning to verify distributed systems
• Using type theory to verify distributed systems
• Logical foundations of distributed systems

Applicants must hold (or be about to obtain) a Masters or Bachelor degree in Computer Science. In addition, they must have a strong background in one of the following areas:

• Formal methods
• Distributed systems
• Programming languages
• Type theory

PhD positions are typically for 3.5 years and are fully funded, covering tuition fees and a bursary.

Please, do not hesitate to contact Vincent Rahli for further details. In addition, feel free to browse his webpage for more information on my research interests. The two following papers are especially relevant:

Additionally, the following page contains useful information regarding our lively theory group, which the successfully candidate would be part of.

### PhD position at University of Birmingham, UK

Benedikt Ahrens would like to invite applications for a fully-funded PhD position in the School of Computer Science at the University of Birmingham, UK. The PhD student will work with him on topics related to categorical semantics of programming languages and computer theorem proving. Students broadly interested in these fields of research are strongly encouraged to apply. Topics of particular interest are:

• Syntax and semantics of type theory
• Formalisation of mathematics in univalent foundations
• Directed type theory
• Algebraic specification of programming languages

Applicants should hold, or be about to obtain, a Masters or Bachelor degree in Computer Science or Mathematics.

The PhD position is fully funded, covering tuition fees and a tax-free scholarship. Healthcare is provided for free.

Please, do not hesitate to contact Benedikt Ahrens by email for further details. In addition, feel free to browse Benedikt Ahrens's webpage for more information on his research interests.

The theory group at Birmingham's School of Computer Science is very active, organising regular seminars and informal meetings. Many relevant international events frequently take place in Birmingham such as YaMCATS category theory seminar, Midlands Graduate School, and Workshops on Univalent Mathematics. For more information see here.

Information on how to apply is given here. However, interested candidates are strongly encouraged to contact Benedikt Ahrens in the first instance.

### PostDoc/Engineer at UCLouvain, Belgium, in assistive code repair

Universite Catholique de Louvain is seeking to recruit a PostDoc/Research engineer position in a full time position to work on a project on assistive code repair. The post is initially offered for one year, with options to extend for up to three years (project duration is three years from October 2019).

The main responsibilities of the successful candidate will be to:

1. implement program transformation from source code to a formal model suitable for analysis,
2. implement and refine analysis techniques to find program flaws, and
3. to automatically generate program repairs for the flaws found.

The post holder will be working closely with researchers within the group at UCLouvain and industrial partners. The post holder will benefit from a strong research environment provided at UCLouvain and within the team. There will also be opportunities to collaborate on other related projects in the domains of security and verification.

The ideal candidate will hold a PhD or other significant experience in one or more of the following areas:

• program analysis
• (statistical) model checking
• program verification
• automatic program repair
• programming languages/transformation.

Information enquiries are welcome and should be directed to Dr Thomas Given-Wilson or Prof. Axel Legay.

Net salary is 2200-2500 euro per month (after taxes and social security).

Applications should be sent to both Dr Thomas Given-Wilson or Prof. Axel Legay.

### Researcher positions (postdoc/phd) within the ERC Consolidator grant “Certified Quantum Security”, Tartu, Estonia

Below is the description of postdoc positions. Phd positions are similar and can be found here.

This call can also be found here.

As part of the ERC Consolidator Grant "Certified Quantum Security" and the US Airforce project "Verification of Quantum Cryptography", we are looking for postdocs to work on verification of quantum cryptography (or more generally on quantum cryptography).

We will develop methods for the verification of proofs in quantum cryptography. Similar to what the EasyCrypt tool does in classical cryptography. The scope of the project covers everything from the logical foundations, through the development of tools, to the verification of real quantum protocols.

The ideal candidate would have experience in:

• Semantics
• Theorem proving
• Verification of classical cryptography
• Quantum cryptography
• Quantum computation / communication

Of course, expertise in all those areas is very rare, so candidates who are strong in some of those areas and are interested in the others are encouraged to apply!

Please contact Dominique Unruh if you have more questions about the project, the required background, Estonia, the position itself, or the application process. I can also provide a detailed description of the overall research project.

The salary range is 30000-36000 Euro per year (depending on experience), which is highly competitive in Estonia due to low costs of living and low income tax rate (20%). Pension contributions and health insurance are covered by the employer.

Applications are accepted at any time (until all positions are filled), and positions can start as soon as possible. Positions are typically for 2-3 years (up to negotiation).

To apply, please send the following documents to Dominique Unruh:

• List of publications
• Research plan (i.e., how do you think you could contribute to the topic)
• At least two letters of reference (please ask for the letters to be sent directly to us)
• Phd degree
Please apply as soon as possible.

### PhD and postdoc positions at Schaffhausen Institute of Technology, Switzerland

The Chair of Software and Security (Prof. Bertrand Meyer) at the newly created Schaffhausen Institute of Technology has open positions for both PhD students and postdocs. We are looking for candidates with a passion for reliable software and a mix of theoretical knowledge and practical experience in software engineering. Candidates should have degrees in computer science or related fields: a doctorate for postdoc positions, a master’s degree for PhD positions. Postdoc candidates should have a substantial publication record. Experience in one or more of the following fields is a plus:

• Software verification (axiomatic, model-checking, abstract interpretation etc.).
• Advanced techniques of software testing.
• Formal methods, semantics of programming languages, type theory.
• Design by Contract, Eiffel, techniques of correctness-by-construction.
• Cybersecurity.

Compensation at both levels is attractive. Note that the PhD program is conducted in cooperation with partner universities.

Interested candidates should send a CV and relevant documents or links to Prof. Bertrand Meyer. They are also welcome to contact Prof. Bertrand Meyer for details.

### Senior Lecturer/Associate Professor in Software Engineering (Software Verification), Brisbane, Australia

The position is part of a new initiative in verified software supported by generous funding from Oracle. Initially, this will involve playing a leading role in research on verifying optimization passes of compilers. For the first three years, the position will have half the standard teaching duties allowing a greater focus on research and support for two PhD student scholarships and travel for research collaboration.

The primary purpose of this positions is to engage in teaching and research activities in Software Engineering, and play a pivotal role in developing software verification technology in the context of programming language implementation and to contribute to teaching, in Software Engineering and other related areas, course coordination and student supervision.

This position is located at our picturesque St Lucia campus, renowned as one of Australia’s most attractive university campuses, and located just 7km from Brisbane’s city centre. Bounded by the Brisbane River on three sides, and with outstanding public transport connections, our 114-hectare site provides a perfect work environment – you can enjoy the best of both worlds: a vibrant campus with the tradition of an established university.

Our Ideal Candidate
You should possess a PhD in Computer Science or Software Engineering, or a related field. You should have significant experience and a successful record of research achievements in areas including compilers, in particular, their optimization techniques, program analysis, semantics of programming languages, formal verification methods in programming, and the semantics of programming languages.

You should also possess a demonstrable capacity for teaching at both the undergraduate and postgraduate level, experience in postgraduate supervision and experience liaising with industry and external partners.

We value diversity and inclusion, and actively encourage applications from those who bring diversity to the University. Our Diversity and Inclusion webpage contains further information if you require additional support. Accessibility requirements and/or adjustments can be directed to recruitment@uq.edu.au.

What We Can Offer
This is a full-time continuing position at Academic level C/D. The full-time equivalent base salary will be in the range \$117,319 – 135,276 for Level C and \$141,261 – 155,627 for Level D plus super of up to 17%.

For further information see the following link.

### Upcoming Phd/postdoc openings at TU Dresden, Germany

Markus Kroetzsch and his colleages are looking towards a number of new job openings in their group at TU Dresden, in several projects. If you are seeking a fully funded research position in knowledge representation, AI, databases, or related areas, please feel free to contact him informally for further details. See here for more of their work and people.

Specifications:

• Up to three PhD students or postdocs
• English-speaking team
• Research-oriented environment (low project duties, no teaching obligations)
• Teaching possible
• Fully funded (German pay grade E-13), initially for three years
• Timing: as soon as possible, but there is flexibility

Official, university-stamped job adverts will appear in due course.

### Postdoctoral Opportunity at the University of Minnesota, USA

Applications are invited for a postdoctoral position at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and is expected to be of duration of one to two years. Applications will be reviewed and acted upon as soon as they are received.

The project within which the appointment is to be made concerns the further development of a proof environment for reasoning about relational specifications that supports the so-called higher-order abstract syntax approach. A key component of this environment is the Abella proof assistant, which is based on a logic that incorporates a treatment of fixed-point definitions. One thrust for ongoing work is the enhancement of the underlying logic, for example through the addition of predicate quantification. The research group is also interested in building into the Abella system the capability to reason about specifications written in linear logic and dependently typed lambda calculi, and in investigating the benefits of the system in tasks such as compiler verification.

To participate successfully in the research described above, you would need to be broadly conversant with the areas of computational logic and programming languages and to have the mathematical and programming skills necessary for conducting original work in these areas. Prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and other similar logical systems would help in engaging immediately with the research problems of interest.

To view the official announcement for this position, please visit this URL. This site also provides details such as the required qualifications for the position and serves as the portal for applications. To complete an application, you would need to submit a letter indicating your interest in the position, a current CV, one or two papers broadly related to the topics of research and the names and contact details of two people who are willing to serve as your references in the review process.

Please do not hesitate to contact Gopalan Nadathur if you have an interest in the position but would like answers prior to applying to questions related to matters such as the expectations, possible projects, and the suitability of your qualifications for the position.

### Multiple PhD and Postdoc positions in Information Security and Program Verification at ETH Zurich, Switzerland, available immediately

The Institute of Information Security (the groups of Prof. Adrian Perrig and Prof. David Basin) and the Programming Methodology Group (Prof. Peter Müller) at ETH Zurich have multiple open positions for PhD students and Postdocs in a research project in the area of digital trust. The goal of this project is to develop a comprehensive, formally verified security architecture for communication in the physical and digital world. In particular, the project will develop protocols to transfer physical trust relationships into the digital world and store, manage, and use them. The design will take into account human (mis-)behavior from the outset. A particular emphasis is on the formal verification of the architecture both at the design and implementation level to rule out any undesired behavior.

We are looking for enthusiastic and outstanding Computer Science or Mathematics students and postdoctoral researchers with a strong background in some of the following topics:

• formal modeling and verification,
• program verification,
• theorem proving, model checking,
• cryptographic protocols,
• public-key infrastructure, identity management, authentication,
• networking and distributed systems, and
• design and implementation of security architectures.

ETH Zurich regulations require PhD students to hold a Masters or equivalent degree (e.g., Diplom). All candidates matching the profile above are encouraged to apply as soon as possible. We will process applications until all positions are filled. Successful candidates are expected to start soon after acceptance, but the starting date is negotiable.

Applications should include:

• a curriculum vitae,
• a brief description of research interests,
• letters of recommendation from teachers or employers, and,
• if possible, the Master's or Bachelor's thesis and publications.
Applications and inquiries should be sent to Christoph Sprenger and Sandra Schneider at this email address and this email address.

PhD students and Postdocs are paid employees of ETH Zurich. Salary and employment conditions are attractive. Zurich is a diverse and multicultural city which is consistently rated among the best cities in the world in which to live.

### Two post-doctoral positions at ENS de Lyon, France

This is an announcement for two postdoctoral positions at ENS de Lyon, France.

These positions are funded by the ERC project CoVeCe.

This project covers fields such as

• automata theory (from algorithms to Kleene algebra and cyclic proof theory)
• relation algebra, graphs of bounded tree-width, logics with few variables
• theories and tactics for the Coq proof assistant.
Applicants should hold a PhD in theoretical computer science, have a strong background in one of the above fields, and a desire to work at their frontier.

To apply, send an email to Damin Pous with your motivations (which part(s) of the project you would like to be involved in, why...), a brief CV, and the names of two persons who could recommend you. Please feel free to engage into a scientific discussion, or to ask me for more details about the project, the surrounding team (Plume), the lab (LIP), or Lyon's city.

### Tenure track position, programming language design, Bucknell University, Pensilvania, USA

The Department of Computer Science at Bucknell University seeks applications for two tenure-track positions at the Assistant Professor level in computer science beginning August 2020. We are interested in applicants working in any area of computer science, most particularly in those with research areas that expand the range of expertise in the department or that may lead to interdisciplinary collaborations. A PhD is required for this position. Candidates in the final stages of completing their doctoral work will be considered.

We seek candidates who will contribute to the teaching of courses in theoretical aspects of computer science or programming languages design, and core courses in our degree programs. Candidates will have opportunities to develop elective courses in their areas of expertise. We expect that candidates will develop a vigorous scholarly program that creates opportunities for student participation.

The department offers a BA and two ABET accredited BS programs, one in Computer Science and another in Computer Science and Engineering. We have a firm commitment to diversity, equity, and inclusion and to student-centered teaching. Our computing environment is Linux/Unix-based. More information about the department can be found here.

Review of applications will begin on November 1 and continue until the positions are filled. Candidates are asked to submit a cover letter, CV, a statement of teaching philosophy, a statement of research interests, a statement describing any past experience, training, or engagement with issues of diversity, equity, and inclusion, and three confidential letters of recommendation. Applications are only accepted through http://jobs.bucknell.edu. Questions should be directed to Professor L. Felipe Perrone, Chair of Computer Science (perrone@bucknell.edu).

Bucknell University is a private, highly ranked, primarily undergraduate, national liberal arts institution that also offers strong professional programs in engineering, management, education, and music.

Bucknell University is an Equal Opportunity Employer. The university believes that students learn best in a diverse, inclusive community and is therefore committed to academic excellence through diversity in its faculty, staff, and students. Applications from members of groups that have been historically underrepresented in higher education are encouraged.

Bucknell is committed to creating a climate that fosters inclusion, growth, and development for a diverse student body, and seeks candidates who are also committed these goals.

Bucknell is committed to supporting the teacher-scholar model of faculty development. The teaching load is 5 courses per year. With a student-faculty ratio of about 9:1, small class sizes are a hallmark of the Bucknell educational experience. The university sponsors a range of activities to support the development of its faculty, including a Teaching-Learning Center and generous research support and leave policies.

Bucknell is located in Lewisburg, Pennsylvania, on the banks of the Susquehanna River. The Lewisburg area offers a combination of outdoor recreation opportunities and small-town amenities. In addition to the cultural and athletic events offered at the University and in town, the region offers strong schools and medical facilities, and an affordable cost of living. Bucknell is about three hours from Philadelphia, New York, Baltimore, and Washington, D.C.

### PhD position in Coalgebraic Model Checking at FAU Erlangen-Nürnberg, Germany

There is an opening for a fully funded three-year PhD position (E-13 on the German TV-L scale, full time, no teaching obligation) at Friedrich-Alexander-Universität Erlangen-Nürnberg, located at the Chair of Theoretical Computer Science. The position is within the new DFG project "Coalgebraic Model Checking", with Stefan Milius and Lutz Schröder as PIs and with Daniel Hausmann collaborating on a second project position. The aim of the project is to develop a generic framework for model checking a wide variety of logics beyond the standard relational setting, such as probabilistic, graded, or alternating-time logics, based on the successful paradigm of coalgebraic logic.

The position is embedded into a large and active research group with a highly collaborative spirit. Erlangen's technical campus is situated within pleasant Franconia, and close to the vibrant city of Nuremberg. Please send applications or further inquiries to the PIs, Stefan Milius or Lutz Schröder.

### Research Assistant Position in Verification at Royal Holloway, University of London, UK

Royal Holloway, University of London is looking for a postdoctoral research assistant to work on the EPSRC-funded project "String Constraint Solving with Real-World Regular Expressions" (EP/T00021X/1).

• Term: fixed, 3 years
• Expected start date: Oct 2019 - Jan 2020
• Salary: £35,931 to £42,456 per annum - including London Allowance

Project and Application Background
The successful applicant will contribute to the development of constraint satisfaction algorithms for string constraints using "real-world" regular expressions. That is, regular expressions using features such as capture groups and back-references that are not normally considered by theoretical research. In addition, the handling of length constraints represents a significant challenge.

The work will build upon the OSTRICH tool, which will be integrated with the JavaScript symbolic execution framework ExpoSE.

Ideal applicants will have a strong background in computer science or related areas and experience in at least one of logic, algorithms, programming language theory/implementation, formal language theory, and formal verification.

Research Environment
The project is led by Dr. Matthew Hague in the Department of Computer Science. It will proceed in close collaboration with Prof. Dr. Johannes Kinder (Bundeswehr University Munich), Prof. Dr. Anthony W. Lin (Kaiserslautern), and Dr. Philipp Rümmer (Uppsala). In addition, we will also collaborate with Prodo.dev in London.

### Tenure-track Faculty Positions at School of Computing, Queen's University, Canada

• Software Engineering, Security, and HCI
• Assistant and Associate Professor ranks
• For all ads, see here.

The School of Computing in the Faculty of Arts and Science at Queen's University invites applications for a Tenure-track faculty position at the rank of Assistant or Associate Professor in Software Engineering with a preferred starting date of July 1, 2020. In the case of an exceptional candidate, a tenured appointment at the rank of Associate Professor would be considered. All areas of Software Engineering are welcome. The following areas are of particular interest: Software Engineering with and for AI and Machine Learning, DevOps, Performance Engineering, Program Analysis, Testing and Software Quality.

The successful candidate must have a PhD or equivalent degree in Computer Science, Software Engineering or a related discipline completed at the start date of the appointment. The successful candidate is expected to play a major role in the delivery of graduate and undergraduate programs at the School of Computing. The main criteria for selection are academic and teaching excellence. The successful candidate will provide evidence of high quality scholarly output that demonstrates potential for independent research leading to peer-assessed publications and the securing of external research funding, as well as strong potential for outstanding teaching contributions at both the undergraduate and graduate levels, and an ongoing commitment to academic and pedagogical excellence in support of the School's programs. Candidates should demonstrate an ability to work collaboratively in an interdisciplinary and student-centred environment. The successful candidate will be required to make substantive contributions through service to the School, the Faculty, the University, and/or the broader community. Excellent interpersonal skills and exceptional oral and written communication proficiency are required. Salary will be commensurate with qualifications and experience. This position is subject to final budgetary approval by the University.

Queen's University is one of Canada's leading research-intensive universities. We are focused on being the quality leader in Canadian higher education and are dedicated to promoting research and scholarship of national and international distinction. The School of Computing has 29 full-time and 20 cross-appointed faculty, over 500 undergraduate students, and over 140 graduate students. The School offers undergraduate programs in Computer Science, Software Design, Biomedical Computing, Computing and Mathematics, Computing and the Creative Arts and Cognitive Science. The School also offers Master’s and Doctoral programs in Computer Science.

Queen's University is one of the oldest universities in Canada and has a global reputation for teaching and research excellence. The main campus is located within walking distance to the vibrant downtown area. Kingston is on the shore of Lake Ontario and near the Thousand Islands region of south-eastern Ontario. Kingston and the surrounding region boast a wide range of recreational opportunities and a rich arts and cultural community. In addition to Queen's University, Kingston is home to St. Lawrence College and the Royal Military College of Canada.

Additional information about Queen’s University, which may be of interest to prospective faculty members, can be found here.

The University invites applications from all qualified individuals. Queen's is committed to employment equity and diversity in the workplace and welcomes applications from women, visible minorities, Aboriginal peoples, persons with disabilities, and LGBTQ persons. All qualified candidates are encouraged to apply; however, in accordance with Canadian immigration requirements, Canadian citizens and permanent residents of Canada will be given priority.

To comply with federal laws, the University is obliged to gather statistical information as to how many applicants for each job vacancy are Canadian citizens / permanent residents of Canada. Applicants need not identify their country of origin or citizenship; however, all applications must include one of the following statements: "I am a Canadian citizen / permanent resident of Canada"; OR, "I am not a Canadian citizen / permanent resident of Canada". Applications that do not include this information will be deemed incomplete.

A complete application consists of:

• a cover letter (including one of the two statements regarding Canadian citizenship / permanent resident status specified in the previous paragraph);
• a current Curriculum Vitae (including a list of publications);
• a statement of research interests;
• a statement of teaching interests and experience (including teaching outlines and evaluations if available); and,
• three letters of reference to be sent directly by email

The deadline for applications is October 31, 2019.

Applicants are encouraged to send all documents in their application packages electronically as a single PDF, to the Chair of Faculty Search Committee; alternatively, hard copy applications may be submitted to:

```    Faculty Search Committee Chair
The School of Computing
557 Goodwin Hall
Queen’s University
Kingston, Ontario K7L 3N6

The University will provide support in its recruitment processes to applicants with disabilities, including accommodation that takes into account an applicant’s accessibility needs. If you require accommodation during the interview process, please contact Tom Bradshaw in the School of Computing.

### 1 month Programming Internship - Algorithms Group - University of Bergen - Norway

Applications for a short-term programming internship at the University of Bergen are sought. The internship will happen in the context of the project "Automated Theorem Proving from the Mindset of Parameterized Complexity Theory".

The internship is open for students enrolled in a Master's or Ph.D. program in computer science, anywhere on earth.

Prospective applicants should have excellent programming skills in C++ and an excellent background in algorithms. Proficiency in automata theory is a great advantage.

Main activity:
The main activity will be the implementation of new parameterized algorithms in the field of automata theory. The language of use is C++.

Depending on your interests, you may also choose to be involved in the process of writing research papers related to the topics of the internship. Applicants with interest in writing scientific work will be given preference.

Requirements:

1. You need to be enrolled in a Master's or Ph.D. program in computer science (anywhere on earth).
2. Excellent programming skills in C++
3. Excellent background in algorithms.
4. Proficiency in Automata theory is an advantage.
5. The ability to work independently and in a structured manner is a strong requirement.

Financial support: We will reimburse expenses with the following:

1. return flight/train tickets between your location and Bergen.
2. accommodation.
Note: Travel arrangements and search for accommodation should be done by the student. The reimbursement of expenses only occurs at the end of the internship.

Duration:
The ideal duration of the internship is 1 month. Slightly longer stays are also possible.

Starting-Finishing Dates:
Flexible. Two ideal periods are specified below. But feel free to suggest other dates, if the suggested ones do not work for you.

• 18/Nov - 20 December.
• 13/Jan - 07 February.
• Later dates.

Application: If the internship described above sounds interesting to you, please send the following information, in a single PDF file, to Mateus Oliveira. Please write INTERNSHIP in the subject field.

1. A short application letter. At most one page.
4. Specification of your level of expertise in C++.
5. Specification of your level of expertise in Algorithms.
6. Specification of your level of expertise in Automata Theory.
7. Estimated starting-finishing dates.
8. A cost estimate, including the cost for a return ticket between your location and Bergen, and the cost for 1 month of accommodation in Bergen.

Deadline: We will start to review applications on 15 October. But applications will be accepted on a continuous base until the internship positions are filled.

For further questions, get in touch with Mateus Oliveira.

### Full Professor of Artificial Intelligence Techniques at TU Wien, Austria

We invite applications for this full-time professorship until December 1. This full-time, permanent position is affiliated to the Institute of Logic and Computation at the Faculty of Informatics. The estimated starting date is in October 2020.

Research Area
The focus of this professorship lies on techniques and tools for Artificial Intelligence systems. Potential research topics include:

• Heuristic problem solving and search
• Algorithmic Decision Making
• Probabilistic Models and Reasoning
• Planning and Scheduling
• Natural Language Understanding
• Engineering of Intelligent Systems

Profile
The successful candidate will have an outstanding academic record in Artificial Intelligence, in particular techniques and tools of AI Systems.

Essential Qualifications

• PhD or doctoral degree in Computer Science or Business Informatics
• Post-doctoral experience at a university or other research institution
• An outstanding research and publication record
• An excellent reputation as an active member of the international scientific community
• Experience in raising research funds and managing scientific research projects
• Experience in university teaching
• Pedagogic and didactic skills
• Gender sensitivity and social skills

Desirable Qualifications

• Habilitation or equivalent qualification
• Proficiency in German, or willingness to learn
• Willingness to promote young scientists
• Gender sensitivity and social skills

We offer

• Excellent working conditions in an attractive research environment
• An attractive salary, including additional contributions to a pension fund
• Additional financial research support during the first years (e.g. equipment)
• Relocation assistance
• Dual career Service
• A position in a city with an exceptional quality of life

Salary
In accordance with the Austrian Collective Agreement for University Staff, this position offers an annual minimum salary of € 71,822.80. The actual salary will be negotiated between the successful candidate and TU Wien and commensurate to his or her qualifications.

Application
Applications have to be addressed to Prof. Dr. Hannes Werthner, Dean of the Faculty of Informatics, sent as a single PDF and include:

• A detailled curriculum vitae
• A list of publications
• A positioning statement describing the applicant’s vision on how to position and advance the field within the Faculty of Informatics in the areas of research and teaching, in particular in connection to the four research foci.
• Copies of the applicant’s five most important publications related to the position together with an explanation of their relevance

TU Wien is committed to increasing female employment in leading scientific positions. Female applicants are explicitly encouraged to apply. Preference will be given to female applicants when equally qualified. People with special needs with appropriate qualifications are encouraged to apply. In case of queries, please contact the representative of people with disabilities of TU Wien, Mr. Gerhard Neustätter. Child care breaks will be handled in the same manner as in the ERC regulations for principal investigators applying to the Starting Grant.

Please note that the legally binding announcement of this position can be found in TU Wien’s University Gazette.

### post-doc positions in Oxford and Cambridge, UK

Two three-year post-doc positions in Semantics and Descriptive Complexity at Oxford and Cambridge.

There are two post-doctoral research positions open, one at Oxford and one at Cambridge, to work on a new EPSRC-funded project on "Resources and co-Resources: A junction between semantics and descriptive complexity" which is jointly led by Prof. Samson Abramsky FRS at Oxford, and Prof. Anuj Dawar at the University of Cambridge.

The positions are available to start as soon as possible, and are funded for 36 months.

The project seeks to explore ways in which methods from the study of logic and algorithms (specifically finite model theory and descriptive complexity) can be combined with methods from semantics (such as category theory) to build a cohesive algebraic theory of resources. This builds on recent work obtaining categorical accounts of essential constructions in finite model theory (by Abramsky, Dawar and Wang and Abramsky and Shah), as well as categorical accounts of quantum resources (by Abramsky, Barbosa, de Silva and Zapata). This work made essential use of monads -- seen as encapsulating quantum and other resources -- and of comonads, which encapsulate “coresources”, i.e. ways of limiting access to a structure corresponding to definability in various logics. The project will seek to apply these new tools to major results in descriptive complexity, to expand them to cover other important constructions, to find ways of combining accounts of quantum resources and logical co-resources, and to build a general theory of these.

There are separate application processes for applying for the two positions. Details of these and further information may be found at these webpages here and here.

For further questions or enquiries, contact Prof. Samson Abramsky or Prof. Anuj Dawar.

### PhD position in Theoretical Computer Science at the VU Amsterdam, Netherlands

We are seeking applications for a fully-funded, 4-year PhD position in the Section of Theoretical Computer Science of the Vrije Universiteit Amsterdam (VUA). The goal of the project is the development of techniques for reasoning about automata that transform finite and infinite words (also known as transducers). For more details about the project, please check out here, and here. In this project, we will use and extend techniques from automata theory, combinatorics on words, logic, coalgebra and term rewriting.

Embedding
The principal investigator of this project is Joerg Endrullis with a background in term rewriting and automata theory. We will collaborate with Helle Hansen from Delft University of Technology (TU Delft) having expertise in logic and coalgebra. At the Vrije Universiteit Amsterdam we will collaborate with Femke van Raamsdonk with a background in higher-order rewriting, and Jasmin Blanchette working on formal verification and theorem provers.

Qualifications
Applicants should have a masters degree in computer science, mathematics, logic, or a closely related area. Knowledge of automata theory, coalgebra, logic, term rewriting or lambda calculus is considered an advantage. Fluency in English is important. Dutch language proficiency is not required.

Application
Please send applications by email to dr. Joerg Endrullis (+31 (0)20 5989886)

For more details on the salary and employment conditions, see the full vacancy text. Feel free to contact us for further information about the project and the position.

Formal applications must include:

• A motivation letter
• A curriculum vitae, including a list of courses with grades
• A copy of the master's thesis (if already available)
• The name of at least one scientist able and willing to provide a reference

Review of applications will begin on December 1, 2019, and will continue until the position is filled.

### PhD and postdoctoral positions in Formal Methods and Decompilation at Open University of The Netherlands / VirginiaTech (USA)

Multiple positions are available at the Open University of The Netherlands and the Systems Software Research Group at Virginia Tech on projects on formal methods and reverse engineering of binaries. We are interested in decompilation: retrieving source code from a binary while maintaining a formal correctness proof that everything is sound. This will make bottom-up formal verification possible: applying formal verification to binaries, instead of to source code. If you have an interest in one of the fields of formal methods, (de)compilation, low-level assembly code or reverse-engineering, then you must certainly apply. We can hire both ''promovendi'' (PhD students) and postdocs on this project. Unique about the project is:

• The project has close ties to interested parties with relevant case studies.
• It is a close collaboration between a Dutch and a US university and if requested there is the possibility of extended visits to the US.
• You can choose your own work location in The Netherlands (Amsterdam, Utrecht, Nijmegen, Eindhoven, ...)

Applications can be done by sending your CV and a short application letter indicating your interest in the project via e-mail. For more information, see here.

### Associate/Assistant Professor in Formal Methods for Safe and Secure Systems at DTU Technical University of Denmark

The Section on Formal Methods for Safe and Secure Systems at the Department of Applied Mathematics and Computer Science (DTU Compute) of the Technical University of Denmark invites applications for an Associate/Assistant Professor in Formal Methods for Safe and Secure Systems.

Apply online and find details.

Starting date: The position is available from July 1, 2020 or according to mutual agreement.

### PhD Position in Formal Methods for Biology at DTU Technical University of Denmark

The section for Formal Methods of DTU Technical University of Denmark offers a PhD position funded by the Danish project ‘REDUCTO: A novel approach for the reduction of Boolean networks’.

The student will be supervised by PI of the project, Associate Professor Andrea Vandin, and by the head of section Alberto Lluch Lafuente in collaboration with

• Luca Cardelli (University of Oxford, UK),
• Claudine Chaouiya (I2M, Aix Marseille Univ, CNRS, Centrale Marseille, Marseille, France & Instituto Gulbenkian de Ciência, Portugal), and
• Lars Keld Nielsen (Novo Nordisk Foundation Center for Biosustainability, Denmark).

Apply online here

Project Description
Boolean networks (BN) are a graph-based well-established method to model biological systems. In order to accurately model systems, we often face models too complex to be interpreted or analyzed. Several reduction techniques exist to mitigate this problem. Our crucial hypothesis is that novel approaches to the reduction of BNs are needed, and that those can be developed by using a theoretical computer science approach. The project aims at developing novel mathematically-grounded techniques and tools to reduce and simplify complex BNs. The starting point will be recent work of the PI, presented e.g. in:

• Maximal aggregation of polynomial dynamical systems, L Cardelli, M Tribastone, M Tschaikowski, A Vandin, Proceedings of the National Academy of Sciences 114 (38), 10029-10034, https://doi.org/10.1073/pnas.1702697114
• Symbolic computation of differential equivalences, L Cardelli, M Tribastone, M Tschaikowski, A Vandin, Proceedings of POPL 2016, https://doi.org/10.1145/2837614.2837649
Tool support will be based on the tool ERODE, maintained by the PI.

### Postdoc positions in the CertiChain project, Singapore

Several postdoc positions available in Sergei Ilya's group at School of Computing of National University of Singapore in the new project CertiChain, funded by NSOE-TSS. The positions are initially for two years with a possibility of extension.

The CertiChain project focuses on mechanising safety, liveness, and probabilistic security properties of distributed protocols, with a specific focus on Nakamoto-style consensus. I am looking for motivated candidates with a strong, internationally competitive research track record and research expertise in:

• distributed systems and consensus protocols
• formal verification using program logics
• mechanised proofs and proof automation

More details on the project can be found by this link below.

The NUS School of Computing is one of the world-leading departments in the areas of programming languages, software engineering, distributed systems, security and privacy. It provides a diverse and welcoming environment. Salaries at NUS are internationally competitive.

Do not hesitate to get in touch with Sergey Ilya if you are interested.

### Tenure-track assistant professor position in Software Engineering (formal methods), York University, Toronto

The Department of Electrical Engineering and Computer Science, Lassonde School of Engineering invites applications for a tenure track, professorial stream position in Software Engineering at the rank of Assistant Professor. The appointment will commence on July 1, 2020, subject to budgetary approval. We look for outstanding candidates in any area within Software Engineering, with a preference for those with expertise in formal method.

### Tenure-Track Faculty Positions at the MPIs for Informatics, Software Systems, and Security & Privacy, in Germany

The Max Planck Institutes for Informatics (Saarbruecken), Software Systems (Saarbruecken and Kaiserslautern), and Security and Privacy (Bochum) invite applications for tenure-track faculty in all areas of computer science. Pending final approval, we expect to fill several positions.

A doctoral degree in computer science or related areas and an outstanding research record are required. Successful candidates are expected to build a team and pursue a highly visible research agenda, both independently and in collaboration with other groups.

The institutes are part of a network of over 80 Max Planck Institutes, Germany's premier basic-research organizations. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. The institutes offer a unique environment that combines the best aspects of a university department and a research laboratory: Faculty enjoy full academic freedom, lead a team of doctoral students and post-docs, and have the opportunity to teach university courses; at the same time, they enjoy ongoing institutional funding in addition to third-party funds, a technical infrastructure unrivaled for an academic institution, as well as internationally competitive compensation.

We maintain an international and diverse work environment and seek applications from outstanding researchers worldwide. The working language is English; knowledge of the German language is not required for a successful career at the institutes.

Qualified candidates should apply on our application website. To receive full consideration, applications should be received by December 15th, 2019.

The Max Planck Society wishes to increase the number of women in those areas where they are underrepresented. Women are therefore explicitly encouraged to apply. The Max Planck Society is also committed to increasing the number of employees with severe disabilities in its workforce. Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended to seven years based on a midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

### Open faculty positions at the Instituto Superior Técnico, Lisbon, Portugal

The Computer Science and Engineering Department of the Instituto Superior Técnico (ULisboa) is carrying out an open search process for possible candidates to future openings for faculty career positions. This open search is targeted at possible candidates who have an interest in enrolling at the base level of the university professional career (assistant professor), in all scientific areas of the Department, namely:

• Artificial Intelligence
• Computer systems, architecture, and networking
• Graphics and Interaction
• Information Systems
• Programming Methodology and Technology

Possible candidates should send to this email address a zip file containing the following materials:

• Curriculum Vitae
• Teaching and research statement
• Contact (including email address) of three researchers or professionals from the area who can be contacted to provide reference letters, attesting to the scientific, pedagogical, and professional qualities of the possible candidate.
For full consideration we recommend sending your materials by November 15, 2019, though we continue to review the materials we receive past that date, until the end of February 2020. For any additional questions please contact the Department.

## Others

### The TPTP Problem Library, Release v7.3.0

Geoff Sutcliffe
Dep't of Computer Science, University of Miami, USA

The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with:

• A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism.
• A comprehensive list of references and other interesting information for each problem.
• Arbitary size instances of generic problems (e.g., the N-queens problem).
• A utility to convert the problems to existing ATP systems' formats.
• General guidelines outlining the requirements for ATP system evaluation.
• Standards for input and output for ATP systems.

The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.

This is the first release with polymorphic THF (TH1) problems. There are 644 polymorphic TH1 problems in 14 domains.

TPTP v7.3.0 is now available here. The TPTP-v7.3.0.tgz file contains the library, including utilities and basic documentation. Full documentation is online.

The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user, and be kept informed of such developments, please email Geoff Sutcliffe.

What's New in TPTP v7.3.0 Release v7.3.0, Fri Aug 2 16:17:10 EDT 2019

Changes from v7.2.0 to v7.3.0 for THF problems

• 8 bugfixes done, in the domains LCL.

Changes from v7.2.0 to v7.3.0 for TFA problems

• 6 new abstract problems, in the domains PLA.
• 7 new problems, in the domains PLA.

Changes from v7.2.0 to v7.3.0 for FOF problems

• 286 new abstract problems, in the domains CSR NUN SEV SWW.
• 458 new problems, in the domains CSR NUM NUN SEV SWW.
• 247 bugfixes done, in the domains CSR NUN SET.

Changes from v7.2.0 to v7.3.0 for CNF problems

• 45 new abstract problems, in the domains SYO.
• 196 new problems, in the domains AGT ALG ANA BOO CAT COL CSR GRP HEN KLE LAT LCL MSC NLP NUM PLA PUZ REL RNG ROB SEU SWB SWV SYN SYO.
• 16 bugfixes done, in the domains SET.

In SyntaxBNF

• Added semantic rules for <thf_unitary_type>.
• Split into <tff_atomic_type> and <tff_non_atomic_type>, and added (<tff_atomic_type>) to <tff_atomic_type>.

### VerifyThis Collaborative Long-Term Challenge!

VerifyThis is a program verification competition, which is annually held at ETAPS. During the competition, participants work for 90 minutes on relatively small but intriguing verification challenges.

With the VerifyThis Long-Term Challenge we would like to see how far the formal verification community can get within 6 months if they collaborate to verify a real-world software application.

The VerifyThis Long-Term Challenge is starting now, and it will be open until 29th of February, 2020. We would like to encourage everybody in the formal verification community to participate in this challenge, and to use their tools and technique to tackle parts of the challenges.

On this page, you can register your team, and subscribe to our mailing list. The mailing list will be used to for communication and collaboration between the participants, and it will allow you to stay up to date with the other teams' progress.

The results of the challenge will be presented during VerifyThis@ETAPS2020. In addition, we plan to prepare a special results with (individual and collaborative) solutions.

Sophie Tourret