# Association for Automated Reasoning

April 2018

## From the AAR President, Larry Wos

In this column, logic is again in focus. Here I offer substantial challenges for you in the context of what I call proof elegance. Of course, as usual, books, papers, and the Web are off limits when attempting to meet a challenge.

As many of you know, I spend much of my time in the pursuit of elegant proofs, as evidenced by my frequent reference to the most obvious aspect of elegance -- proof length. The history of mathematics and of logic is peppered with studies by various mathematicians and logicians focusing on proof length. But many other aspects of proof elegance also merit study. For example, the avoidance of some lemma, the avoidance of some term, the identification of an axiom that is not needed because of being dependent on the remaining axioms -- each aspect offers challenging problems to solve. If you or a colleague find notions of proof elegance intriguing, you might browse in a book I coauthored with Gail Pieper, "Automated Reasoning and the Discovery of Missing and Elegant Proofs".

In this column, two aspects are in focus: axiom dependence and term avoidance. The area of concern is an old friend from a column from late 2013, namely, many-valued or infinite-valued sentential calculus.. Hyperresolution together with the following clause provides what is needed, where the function i denotes implication and the function n, found in the axioms for infinite-valued logic, denotes negation.

```      -P(i(x,y)) | -P(x) | P(y).
```

In other words, for the challenges that follow, the inference rule to be used is condensed detachment. The original axiom system for multivalued logic is the following.

```      %  Just the implicational axioms: A1-A3
P(i(x,i(y,x))).
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(i(x,y),y),i(i(y,x),x))).
%  Following is MV4.
P(i(i(n(x),n(y)),i(y,x))).
%  Following is MV5.
P(i(i(i(x,y),i(y,x)),i(y,x))).
```

Your first challenge is to prove that the last of the five given formulas is in fact unneeded in the sense that it is a dependent axiom, deducible from the first four. On May 27 2001, I found, with Bill McCune's OTTER, a proof one of whose steps relied on what I call double negation, the following.

```      146 (heat=1) [hyper,45,137,49] P(i(n(n(x)),i(y,x))).
```

And, you may have guessed, your second challenge is to prove the dependence of MV5 with a sequence of deduced steps none of which contains a double-negation term, a term of the form n(n(t)) for some term t. Proofs avoiding double-negation terms are more elegant, at least to some of us.

Your third challenge, if met, would answer a question I have been trying to answer for fifteen years or more. The challenge is to find a proof of the dependence of the fifth of the five axioms, relying on condensed detachment of length strictly less than 30, regardless of the presence of double-negation terms. If you meet this challenge, please send me such a proof. I have many proofs of the dependence of MV5 on the other four, each of which has length 30.

Some of you would enjoy other challenges whose answer I know not. I offer you the following. Does there exist a proof of the dependence of MV5 on the other four axioms such that its variable richness, to be defined, is 3? The variable richness of a proof, another aspect of elegance, equals the maximum, among the deduced steps, of the number of distinct variables in a formula or equation in the proof. I have a proof of variable richness 4.

For another challenge, one that is perhaps more familiar to you, I offer the challenge of what might be termed lemma avoidance. Specifically, at various occurrences in the literature, you can find a proof of the dependence of the fifth of the five axioms for infinite-valued logic where the proof relies on the following, sometimes named 2.22, 3.5, and 3.51.

```      P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))).
P(i(i(x,y),i(n(y),n(x)))).
P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))).
```

Your challenge is to find a proof of the cited dependence that avoids the use of all three lemmas; no constraint is placed in the context of double negation. If you decide to first prove the cited three lemmas, the last of the three, 3.51, may turn out to be quite difficult to prove.

The concern in the next challenge is a type of distributivity. For this challenge, I ask for a proof of a type of distributivity, called 43b, the following given in its negated form.

```      -P(i(i(i(n(i(a,n(b))),n(i(a,n(c)))),n(i(a,n(c)))),n(i(a,n(i(i(b,c),c)))))) | \$ANS(3_43b).
```

When I sought a proof of 43b, I had great difficulty avoiding double negation. So, the challenge is to find a proof of 43b that avoids double negation. I note that of the challenges issued in this column, this last one may be arduous.

## Guest Column: Mike Gordon and Hardware Verification

Lawrence Paulson
University of Cambridge

Mike Gordon, who died last summer, devoted his research career to hardware verification. According to former colleagues, his interest in that topic dates from the 1970s, when he was working with Robin Milner at the University of Edinburgh on the development of Edinburgh LCF (Logic for Computable Functions). Although LCF was to become the foundation of practically every subsequent interactive theorem prover, including Mike's HOL system, his early ideas on hardware verification represented a completely independent strand of work.

An Edinburgh technical report dated 1981 (revised 1982) gives the earliest comprehensive overview of Mike's ideas for hardware verification. He was already looking at register transfer systems and not merely at gates. He was certainly aiming for full functional verification of implementations against specifications, as opposed to some sort of bug finding. The report is 74 pages long and full of extended examples.

These ideas evolved considerably over time. That 1981 report envisaged specifying the semantics of hardware devices using Scott domains, reflecting Mike's background in denotational semantics. In 1982, Mike moved to the University of Cambridge as a Lecturer (equivalent to an Assistant Professor). I joined him there as a post-doc to work on the continued development of LCF. Within a year, a new and improved "Cambridge LCF" was available as a basis for building new tools, and Mike launched his LCF_LSM (Logic For Sequential Machines. LSM was based on Robin Milner's CCS (Calculus of Communicating Systems). Once again, Mike was applying tools from his Edinburgh background to the problem of hardware verification. CCS was generally applied to concurrent programming, but it could be applied to hardware as well. Already in 1983, Mike had specified and verified a microcoded computer using LCF_LSM. Avra Cohn, Mike's wife, joined in the research and by 1987 had formally verified substantial aspects of a real-world processor (the Viper microprocessor, designed at the UK's Royal Signals and Radar Establishment) using LCF_LSM.

Another milestone was Mike's 1988 adoption of higher-order logic as the specification language. Already with LCF_LSM, Mike had abandoned Scott domains with their troublesome and seemingly irrelevant undefined values and partial orderings. For a while, he may have believed that advanced examples might need this more sophisticated semantic basis, but higher-order logic represented a final break from that possibility. At a time when first-order logic was strongly preferred by both mathematicians and computer scientists (notably John McCarthy), the adoption of higher-order logic was a radical choice. Mike always gave credit for this idea to Keith Hanna of the University of Kent, but if so, it must be noted that Hanna soon came to prefer even richer formalisms based on dependent types.

The advantage of higher-order logic over first-order logic was that variables could range over predicates and functions. Predicates could denote hardware components, while functions could represent the signals on the wires connecting these components. Through existential quantification, internal wires could be hidden. Functions could represent signals indexed by time, families of wires or even families of components. Best of all, the process of hardware specification and verification was suddenly being done in a standard, if slightly esoteric, form of predicate logic. Specialised primitives did not require extending the formalism and were nothing but logical definitions, essentially abbreviations. And the theory of this formalism had been completely worked out by Alonzo Church already in 1940. Mike's HOL system closely followed Church's axioms and formal development.

Three years later, in 1991, Sara Kalvala could already write a paper entitled "HOL Around the World" listing research projects using HOL, mainly for hardware verification, at a great many institutes. And because higher-order logic is a general-purpose formalism, users were not confined to hardware verification and soon found a great variety of other applications. To mention just two early examples, John Harrison considered the problem of floating-point verification and was soon verifying numerical algorithms, while Joe Hurd tackled the verification of probabilistic algorithms. Such applications required formalising substantial chunks of mathematical analysis in HOL.

It's remarkable to consider that Mike focused on hardware verification during the 1970s because he thought that software verification was on the way to being solved. Four decades later, this still hasn't happened. Mike later explained that hardware designs are much cleaner than software, although they are extremely complex. Software designers are protected from their errors by warranty disclaimers and the ease of issuing patches over the Internet, while hardware must be right the first time. Hardware verification is now a reality; when will the software world catch up?

## Ulrich Furbach succeeds Hans Jürgen Ohlbach as Vice-president of AAR

Martin Giese
Secretary of AAR and CADE

Prof. Hans Jürgen Ohlbach has acted as vice-president of the Association for Automated Reasoning for over 20 years. He is now retiring, and has asked the board to elect a replacement. The board elected Prof. Ulrich Furbach as his successor.

We thank Hans Jürgen Ohlbach for his many years of service, and welcome Ulrich Furbach on the board.

## New AAR and CADE Secretary

Christoph Weidenbach
Larry Wos
(AAR President)

After seven years of excellent service, Martin Giese has resigned from the posts of AAR and CADE secretary. The AAR Board and the CADE Board of Trustees cannot express how valuable has been his service to the community. He will be missed in this capacity. Thank you, Martin, for everything; it was a pleasure to work with you.

Our new AAR secretary/treasurer and CADE secretary is Philipp Rümmer, starting May 1st. We welcome Philipp in his new role and look forward to working with him.

## Call for Nominations: CADE Trustees Election

Martin Giese
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, electing Herbrand award winners, instituting new awards, etc.

Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2018.

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

• Christoph Benzmüller (vice-president, elected 2015)
• Jasmin Blanchette (elected 2016)
• Pascal Fontaine (CADE-27 program chair)
• Martin Giese (secretary)
• Jürgen Giesl (reelected 2017)
• Marijn Heule (elected 2017)
• Laura Kovács (elected 2016)
• Aart Middeldorp (elected 2015)
• Neil Murray (treasurer)
• Andrew Reynolds (elected 2017)
• Renate Schmidt (elected 2016)
• Stephan Schulz (IJCAR 2018 program co-chair)
• Christoph Weidenbach (president, elected 2016)

The terms of Christoph Benzmüller and Aart Middeldorp end. Both of these may be nominated for a second term.

The term of office of Stephan Schulz as IJCAR 2018 program chair also ends; he is replaced by CADE-27 program co-chair Pascal Fontaine. As outgoing ex-officio trustee, Stephan Schulz is eligible to be nominated as elected trustee.

In summary, we are seeking to elect two trustees.

Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at IJCAR 2018 in Oxford. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be AAR members. For further details please see the CADE Inc. bylaws at the CADE web site.

E-mail nominations can be provided up to the upcoming CADE business meeting, via email to

Christoph Weidenbach, President of CADE Inc.
with copies to
Philipp Rümmer, new Secretary of CADE Inc.

## Herbrand Award: Call for Nominations

Martin Giese
Secretary of AAR and CADE
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)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at IJCAR 2018 is

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

Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's 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, new Secretary of CADE Inc. and AAR

## FLoC'18 Student Travel Support

FLoC has some funds to provide travel grants of up to \$1000 (USD) for student attendees of FLoC'18. Funds can be requested to cover airfare and lodging (registration fees and meals will not be funded). We expect to award about 100 grants. The application deadline is May 18, 2018, and recipients will be notified by June 1.

Funds will be provided after the conference, upon submission of receipts and a short report detailing the student's experience at and benefit from FLoC'18 (these reports will be used to compile a final report to our sponsors). Awardees are expected to spend up to one day during the meeting helping with logistics.

Applicants' advisors should send a brief statement certifying their educational status and describing their financial need, and merits.

Special efforts will be made to bring to FLoC students from under-represented groups. Applications must be received by the deadline.

Applicants are required to apply using the linked web form.

Advisor letters (plain text only) should be sent to this email address by May 18, 2018.

## Ackermann Award 2018 - The EACSL Outstanding Dissertation Award for Logic in Computer Science

Call for Nominations
Nominations are now invited for the 2018 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1.1.2016 and 31.12.2017 are eligible for nomination for the award. The deadline for submission is 4 April 2018. Submission details follow below. Nominations can be submitted from 1 January 2018 and should be sent to the chair of the Jury, Thomas Schwentick.

The Award
The 2018 Ackermann award will be presented to the recipient(s) at the annual conference of the EACSL, 4-7 September 2018, in Birmingham (UK).

The award consists of

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

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

Jury
The jury consists of:

• Christel Baier (TU Dresden);
• Mikolaj Bojanczyk (University of Warsaw);
• Anuj Dawar (University of Cambridge);
• Dexter Kozen (Cornell University);
• Dale Miller (INRIA and Ecole Polytechnique), ACM SigLog representative;
• Luke Ong (University of Oxford);
• Simona Ronchi Della Rocca (University of Torino), the vice-president of EACSL;
• Thomas Schwentick (TU Dortmund), the president of EACSL.

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

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

The submission should be sent by e-mail as attachments to the chairman of the jury, Thomas Schwentick With the following subject line and text:

• Subject: Ackermann Award 2018 Submission
• Text: Name of candidate, list of attachments
Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text.

## E. W. Beth Dissertation Prize, 2018: call for nominations

Since 2002, FoLLI (the Association for Logic, Language, and Information) has awarded the E.W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree awarded in 2017.

Who qualifies.
Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2017 and December 31st, 2017. Theses must be written in English; however, the Committee accepts submissions of English translations of theses originally written in other languages, and for which a PhD was awarded in the preceding two years (i.e. between January 1st, 2015 and December 31st, 2017). There is no restriction on the nationality of the candidate or on the university where the Ph.D. was granted.

Prize.
The prize consists of:

• a certificate
• a donation of 2500 euros provided by the E.W. Beth Foundation
• an invitation to submit the thesis (or a revised version of it) to the FoLLI Publications on Logic, Language and Information (Springer).

How to submit
Only electronic submissions are accepted. The following documents are required:

• The thesis in pdf format (ps/doc/rtf not accepted).
• A ten-page abstract of the dissertation in pdf format.
• A letter of nomination from the thesis supervisor (see below).
• Two additional letters of support, including at least one from a referee not affiliated with the academic institution that awarded the Ph.D. degree.
Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded. Nominations should contain the email contact details of the nominator.

All documents must be submitted electronically (preferably as a zip file) to Ian Pratt-Hartmann. Hard copy submissions are not allowed. In case of any problems with the email submission or a lack of notification within three working days, nominators should write to Ian Pratt-Hartmann.

The prize will be awarded at the ESSLLI summer school in Sofia. The current (tentative) date for the presentation ceremony is August 17th, 2018.

More information is available on the FoLLI website. Queries: Ian Pratt-Hartmann

Important dates:

• Deadline for Submissions: April 23rd, 2018.
• Notification of Decision: July 2nd, 2018.
• ESSLLI summer school (Sofia): August 6th--17th, 2018.

## Call for Bids to Host TABLEAUX 2019

Jens Otten
President of, and on behalf of, the TABLEAUX Steering Committee

The TABLEAUX Steering Committee is now calling for bids to host the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") in 2019. TABLEAUX typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years. Previous TABLEAUX/IJCAR conferences took place in Brasília/Brazil (TABLEAUX 2017), Coimbra/Portugal (IJCAR 2016), Wroclaw/Poland (TABLEAUX 2015), Vienna/Austria (IJCAR 2014), Nancy/France (TABLEAUX 2013), Manchester/UK (IJCAR 2012), Bern/Switzerland (TABLEAUX 2011), Edinburgh/UK (IJCAR 2010), and Oslo/Norway (TABLEAUX 2009). Complete list of previous conferences.

A bid should cover at least the following aspects:

• contact person: name and email address
• names of other people involved in the local organization
• experience, if any, of organizing previous similar events
• planned venue, accessibility and transportation
• suggested dates of the conference
• plans, if any, for co-location with other meetings, conferences and/or workshops
• available accommodation, e.g., hotels and/or dormitory rooms
• catering arrangements
• any relevant plans for social events, e.g., excursions
• a list of potential national and local sponsors
• expected expenses and expected registration costs

Bids that consider co-locating TABLEAUX with other conferences, such as FroCoS or ITP, are strongly encouraged. In 2013 and 2015 TABLEAUX was co-located with FroCoS (the International Symposium on Frontiers of Combining Systems) and in 2017 TABLEAUX was co-located with FroCoS and ITP (the International Conference on Interactive Theorem Proving).

The leader or leaders of the winning bid will become the conference chair or co-chairs of TABLEAUX 2019. The TABLEAUX Steering Committee will decide if they also become the PC Chair or Co-Chairs. The PC Chair or Co-chairs will create a PC in consultation with the TABLEAUX Steering Committee and will also be expected to edit the conference proceedings.

The bid should be limited to 10 pages and should be submitted as PDF file to Jens Otten.

The deadline for submissions is May 5th, 2018.

The TABLEAUX Steering Committee will decide which bid to accept and announce a decision as soon as possible after the deadline.

Perspective organizers are encouraged to register their intention informally and to get in touch with the TABLEAUX Steering Committee for informal discussion.

## Conferences: Call for Participation

### NFM 2018:Tenth NASA Formal Methods Symposium

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

Celebrating 30 years of formal methods research at NASA Langley, the Tenth NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.

Keynote speakers:

• Ricky Butler (NASA, USA)
• Gilles Dowek (INRIA, CNRS, École Normale Supérieure Paris-Saclay, France)

The program of the symposium is available.

### FLOPS 2018: 14th International Symposium on Functional and Logic Programming

May 9-11, 2018, Nagoya, Japan

Registration is now open for FLOPS 2018. Deadline for early registration is 20 April, 2018.

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

The list of accepted papers is available here.

Invited Speakers

• William E. Byrd (University of Alabama at Birmingham, USA)
• Zhenjiang Hu (National Institute of Informatics, SOKENDAI, Japan)
• Cédric Fournet (Microsoft)

### From the Fundamental Lemma to Discrete Geometry, to Formal Verification

June 18-22, 2018, University of Pittsburgh, USA

The conference is held in honor of Thomas C. Hales on the occasion of his 60th birthday.

The conference will feature talks on representation theory, discrete geometry, and formal verification, with 1.5 days dedicated to each of these topics and with broadly accessible public lectures at the interfaces.

Details are available on the conference website.

## Conferences: Call for Papers

### CSL 2018: Computer Science Logic 2018

September 4-7, 2018, Birmingham, United Kingdom

The Conference
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science. CSL 2018 will be the 27th edition in the series. It will be organised by the School of Computer Science of the University of Birmingham.

Important Dates

• Abstract Submission: 7 April 2018 (AoE)
• Paper Submission: 14 April 2018 (AoE)
• Notification: 14 June 2018

Submission
Submissions will be through EasyChair.

Proceedings will be published in the Leibniz International Proceedings in Informatics. After the conference, selected papers will be invited to a special issue of the online open access journal Logical Methods in Computer Science.

### iFM 2018: 14th International Conference on integrated Formal Methods

September 5-7, 2018, Maynooth, Ireland

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

Areas of interest include but are not limited to:

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

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

Submissions should be made using the iFM 2018 Easychair site.

Important dates

• Abstract submission: Monday, 16 April 2018
• Paper submission: Friday, 20 April 2018
• Notification: Thursday, 14 June 2018
• Camera-ready copy: Tuesday, 1 July 2018
• Conference: 5-7 September 2018
Deadlines expire at 23:59 anywhere on earth on the dates displayed above.

### CICM 2018: 11th Conference on Intelligent Computer Mathematics

August 13-17, 2018, RISC, Hagenberg, Austria

CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration.

CICM 2018 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to

• theorem proving and computer algebra
• mathematical knowledge management
• digital mathematical libraries

CICM appreciates the varying nature of the relevant research in this area and invites submissions of very different forms:

1. Formal submissions will be reviewed rigorously and accepted papers will be published in a volume of Springer LNAI:
• regular papers (up to 15 pages) present novel research results
• project and survey papers (up to 15 pages + bibliography) summarize existing results
• system and dataset descriptions (up to 5 pages) present digital artifacts
2. Informal submissions will be reviewed with a positive bias and selected for presentation based on their relevance for the community.
• informal papers may present work-in-progress, project announcements, position statements, etc.
• posters and system demos will be presented in parallel in special sessions
3. The doctoral programme provides PhD students a forum to present early results receive constructive feedback and mentoring.
4. Workshops allow smaller groups to self-organize focused discussions.
5. Tutorials allow presenting a particular system in depth.

Important Dates
Formal submissions

• Abstract deadline: April 15
• Full paper deadline: April 22
• Reviews sent to authors: May 21
• Rebuttals due: May 27
• Notification of acceptance: June 4
• Camera-ready copies due: June 8
• Conference: August 13-17
Informal submissions and doctoral programme
Two separate submission rounds are offered so that some authors can make early travel plans while other authors submit spontaneously.
• First round submission deadline: April 22
• Second round submission deadline: July 31
All submissions should be made via easychair.

### AISC 2018: 13th International Conference on Artificial Intelligence and Symbolic Computation

September 16-19, 2018, Suzhou, China

AISC is a forum for the exchange of ideas and the presentation of new tools and solutions at the intersection of Artificial Intelligence and Symbolic Computation. It aims to foster contacts and collaborations among researchers from different fields related to AI and Symbolic Computation. The conference is concerned with all aspects of research, including theory, implementations, and applications.

AISC 2018 takes a broad view of AI that includes non-traditional areas such as machine/deep learning and their interactions with logic and symbolic reasoning. It will also have a special track on Collective Intelligence.

Specific topics for AISC 2018 include, but are not limited to:

• Cognitive modelling and symbolic AI
• Machine learning and computational intelligence
• Data modelling and analysis
• Knowledge representation and symbolic computing
• Knowledge acquisition, search, verification, and interoperation
• Automated reasoning and knowledge discovery
• Causal inferences, uncertainty reasoning, and decision support
• Cross-disciplinary knowledge management
• Mechanization of mathematics
• Mechanized program verification and debugging
• Combination of logics and computations
• Integration of logical reasoning and computer algebra
• Symbolic computations for expert systems and machine learning
• Computer vision and computer-aided geometric design
• Computer algebra systems and automated theorem provers
• Computer-based mathematics teaching and didactics
• Programming languages and systems for symbolic computation
• Emerging fields of computational AI

Topics for the special track on Collective Intelligence include, but are not limited to:

• Human computation and collective intelligence
• Game theory and crowdsourcing computation
• Crowdsourcing software engineering
• Crowdsourcing publishing, reviewing, and competition systems

Electronic submission as PDF should be via EasyChair. More information on the submission is available on the conference website.

Important Dates

• Abstract submission deadline: April 27, 2018
• Short/Regular paper submission deadline: May 4, 2018
• Author notification: June 29, 2018
• Camera-ready submission: July 11, 2018
• Early registration: August 18, 2018
• Conference: September 16-19, 2018

### PPDP 2018: 20th International Symposium on Principles and Practice of Declarative Programming

September 3-5, 2018, Frankfurt am Main, Germany

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

Submissions are invited on all topics related to declarative programming, from principles to practice, from foundations to applications. Topics of interest include, but are not limited to

• Language Design: domain-specific languages; interoperability; concurrency, parallelism, and distribution; modules; probabilistic languages; reactive languages; database languages; knowledge representation languages; languages with objects; language extensions for tabulation; metaprogramming.
• Implementations: abstract machines; interpreters; compilation; compile-time and run-time optimization; memory management.
• Foundations: types; logical frameworks; monads and effects; semantics.
• Analysis and Transformation: partial evaluation; abstract interpretation; control flow; data flow; information flow; termination analysis; resource analysis; type inference and type checking; verification; validation; debugging; testing.
• Tools and Applications: programming and proof environments; verification tools; case studies in proof assistants or interactive theorem provers; certification; novel applications of declarative programming inside and outside of CS; declarative programming pearls; practical experience reports and industrial application; education.
The PC chair will be happy to advise on the appropriateness of a topic.

PPDP will be co-located with the 28th Int'l Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR 2018).

Submission Categories
Submissions can be made in three categories: regular Research Papers, System Descriptions, and Experience Reports.

Important dates

• paper submission 23.04.2018
• rebuttal period (48 hours) 14.06.2018
• final papers 16.07.2018
• conference starts 03.09.2018

### RuleML+RR 2018: 2nd International Joint Conference on Rules and Reasoning

18-21 Sep 2018, Luxembourg

RuleML+RR 2018 aims to bring together rigorous researchers and inventive practitioners, interested in the foundations and applications of rules and reasoning in academia, industry, engineering, business, finance, healthcare and other application areas. It will provide a forum for stimulating cooperation and cross-fertilization between the many different communities focused on the research, development and applications of rule-based systems.

RuleML+RR 2018 will take place in Luxembourg on September 18th-21th 2018 and will be part of the Luxembourg Logic for AI Summit (LuxlogAI), "Methods and Tools for Responsible AI", bringing together RuleML+RR 2018, DecisionCAMP 2018, the 14th Reasoning Web Summer School (RW 2018), and the 4th Global Conference on Artificial Intelligence (GCAI 2018).

RuleML+RR welcomes original research from all areas of Rules and Reasoning.

Important Dates:

• Title and Abstract submission: 20 Apr 2018
• Full papers submission: 27 Apr 2018
• Notification of acceptance: 1 June 2018

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

September 24-27, 2018, Catholic University of Milan, Milan, Italy

In the last few decades an impressive amount of foundational research in philosophical logic has been devoted to the development of semantical tools which provide sufficiently fine-grained semantics to deal with important topics of pure and applied modal logic, such as the representation of situations, states of affairs, structured contents, hyperintensional contexts, and agent-related attitudes, like epistemic and prohairetic attitudes. A number of different modal frameworks have emerged to tackle these themes such as:

• explicit semantics (developing syntactic approaches)
• situation semantics (developing possible worlds semantics)
• topological semantics (developing neighborhood semantics)
• truthmaker semantics (developing algebraic and states semantics)

The aim of this conference is to study the potential of these approaches and to explore new connections between them, by providing a forum to present new ideas and analytical methods. We welcome both logical contributions, providing novel solutions to crucial problems in the field, and foundational contributions, focusing on the conceptual frameworks underlying these approaches and the possibility of combining them.

Submission:
We invite submissions for 30 minute presentations, with 10 additional minutes for discussion. Please send a 1000-word abstract in PDF prepared for blind review. All abstracts should be submitted electronically using the EasyChair submission page.

Important dates:

• Deadline for submission: May 30, 2018
• Notification of acceptance: June 30, 2018

More information is available on the conference website.

### ISMIS 2018: 24th International Symposium on Methodologies for Intelligent Systems

October 29 - 31, 2018, St. Raphael Resort, Limassol, Cyprus

ISMIS is an established and prestigious conference for exchanging the latest research results in building intelligent systems. Held twice every three years, the conference provides a medium for exchanging scientific research and technological achievements accomplished by the international community.

Formal Methods for Intelligent Systems
This special session aims at bringing together academic and industrial leaders who will present and discuss the results that combine Formal Methods to solve problems in different areas related to Intelligent Systems. The topics include, but not limited to:

• Intelligent Information Systems
• Autonomic and Evolutionary Computation
• Logic for Artificial Intelligence
• Knowledge Integration and Aggregation
• Intelligent Agent Technology
• Intelligent Data Processing and Analytics

Paper Submission
Authors are invited to submit their manuscripts (maximum 10 pages) electronically in Springer's LNCS/LNAI style. For detailed instructions see the conference homepage ; any necessary information concerning typesetting can be obtained directly from Springer's webpage. All submissions will be subject to review by the ISMIS 2018 program committee in consultation with the special session organizers.

Important Dates

• Paper submission: May 10, 2018
• Notification of accept/reject: July 10, 2018
• Camera-Ready: July 31, 2018
• Author Registration Deadline: July 31, 2018

### LC18: Logic Colloquium 2018

July 23-28, 2018, University of Udine, Italy

The Logic Colloquium 2018 is the annual European summer meeting of the Association of Symbolic Logic (ASL). The Association for Symbolic Logic (ASL) is an international organization supporting research and critical studies in logic. Its primary function is to provide an effective forum for the presentation, publication, and discussion of scholarly work in this area of inquiry. The Association holds two major annual meetings to present current research in all aspects of logic in a way that is accessible to all logicians.

Special Sessions:
6 special sessions with topics:

• Descriptive set theory and dynamical systems
• Model theory
• Proof theory and constructivism
• Temporal and multivalued logics
• Computability theory
• Philosophy of Logic and Mathematics

Submissions:
Abstracts of contributed papers must be submitted as LaTeX source code, via EasyChair.

More information on the submission process is available on the conference website.

Applications For Student Grants:
The ASL, the NSF, and the local organizing committee will make available modest awards to graduate students in logic and to recent PhDs to attend the meeting. For more details, see the student grants webpage.

Important Dates:

• Deadline for abstract submission: April 27, 2018
• Deadline for grant applications: May 4, 2018
• Deadline for early registration: May 23, 2018
• Main event: July 23 (9am)- July 28 (1pm)

### ADG 2018: 12th International Conference on Automated Deduction in Geometry

in memory of Wen-tsün Wu, September 11-14, 2018, Nanning, China

ADG is a forum dedicated to the exchange of ideas and views, to the presentation of research results and progress, and to the demonstration of software tools on the intersection between geometry, computation, and automated reasoning.

Aim and Scope
ADG 2018 aims at gathering researchers, engineers, and others interested in exploring methods for automated reasoning and symbolic computation in geometry, to discuss theoretical and practical challenges, and to present recent research progress and results dedicated (not exhausted) in

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

Important Dates

• Deadline for extended abstract/full paper submission May 25, 2018
• Notification on all papers July 15, 2018
• Camera-ready submission July 31, 2018
• Early registration deadline August 1, 2018
• Conference taking place September 11-14, 2018

### The Ninth Conference on Non-Classical Logic. Theory and Applications

September 24-27th, 2018, Torun, Poland

The conference is devoted to non-classical logics: modal, many-valued, temporal, paraconsistent, epistemic, deontic, substructural, and nonmonotonic logic, and their applications in computer science, artificial intelligence, formal linguistics, cognitive studies, as well as the deeper analysis of traditional philosophical problems.

This is the ninth edition, under the title: "The origins of philosophical logic: 70 years of Jaskowski's and Los' contributions". We will also celebrate the 25th anniversary of the journal Logic and Logical Philosophy published by the Nicolaus Copernicus University in Torun and edited by the Department of Logic.

Important dates

• Deadline for submissions: May, 31
• Acceptance and notification: June, 15
• Deadline for registration: June, 30
• Deadline for payment: July, 15
• Conference: September 24-27, 2018

Submissions to the conference should be made via easychair. More information is available on the conference website.

### RV 2018: 18th International Conference on Runtime Verification

November 10-13, 2018, Limassol, Cyprus

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

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

• specification languages
• monitor construction techniques
• program instrumentation
• logging, recording, and replay
• combination of static and dynamic analysis
• specification mining and machine learning over runtime traces
• monitoring techniques for concurrent and distributed systems
• runtime checking of privacy and security policies
• statistical model checking
• metrics and statistical information gathering
• program/system execution visualization
• fault localization, containment, recovery and repair
• dynamic type checking
Application areas of runtime verification include cyber-physical systems, safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.

Information on the submission process are available on the conference website.

Related Events
The RV conference also includes an RV tool contest as well as an exhibition of industrial-strength runtime verification tools and approaches. Separate calls for contribution to these events will be issued soon.

Important Dates
Papers as well as tutorial proposals will follow the following timeline (Anywhere on Earth):

• Abstract deadline: June 18, 2018
• Paper deadline: June 25, 2018
• Paper notification: September 10, 2018
• Conference: November 10-13, 2018

## Workshops: Call for Papers

### Workshops at FLoC 2018

July 7-19, Oxford, UK

In conjunction with FLoC in Oxford, a total number of 79 workshops will be held, many of which will be of interest to readers of the newsletter.

NB: Check the workshop websites for up-to-date information about submission deadlines.

### WADT 2018: 24th International Workshop on Algebraic Development Techniques

July 2-5, 2018, Royal Holloway University of London, Egham, UK

The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends.

Typical, but not exclusive topics of interest are:

• Foundations of algebraic specification
• Other approaches to formal specification, including process calculi and models of concurrent, distributed, and cyber-physical systems
• Specification languages, methods, and environments
• Semantics of conceptual modelling methods and techniques
• Model-driven development
• Graph transformations, term rewriting, and proof systems
• Integration of formal specification techniques
• Formal testing and quality assurance, validation, and verification
• Algebraic approaches to cognitive sciences, including computational creativity

More information, including submission process available on the conference website.

Important Dates

• Submission deadline for abstracts: April 27th, 2018
• Notification of acceptance: May 18th, 2018
• Early registration: June 1st, 2018
• Final abstract due: June 1st, 2018
• Workshop: July 2-5, 2018

## Spring and Summer Schools

### EPIT 2018: Software Verification Spring School

May 7-11, Aussois, France

EPIT is a long series of Spring schools in theoretical computer science, initiated by Maurice Nivat in 1973 to bring together researchers in a friendly, intensive atmosphere.

The 2018 edition will take place on May 7-11 in Aussois, on the topic of software verification. The need for software verification in our information society has been recognized as early as in the ’70s and it is an ever-more-important concern today. Over the past decades, it has driven exciting research in various fields of theoretical computer science such as logic, automata, type systems, algorithms and complexity. Recently, verification techniques have seen rapid development and industrial adoptions, notably following the SMT revolution.

Speakers and courses:

• SMT solvers, by Pascal Fontaine (LORIA)
• Program verification with F*, by Cătălin Hriţcu (Inria Paris)
• Bounded model-checking, by Gennaro Parlato (University of Southampton)
• Concurrent program logics, by Viktor Vafeiadis (MPI Kaiserslautern)
• SMT, Strings and Security by Philipp Rümmer (Uppsala University)
• Verification of invariants for convergent replicated data types by Gustavo Petri (Université Paris Diderot)
• A talk on Ultimate Automizer by Matthias Heizmann (University of Freiburg)
• A talk on F* and security, TBA

Important Dates:

• Pre-registration: before April 9th

For information about application and registration, see the registration webpage.

### SSFT 2018: Eighth Summer School on Formal Techniques

May 19 - May 25, 2018, Menlo College Atherton, California

Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the sixth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.

Speakers and courses:

• Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole Polytechnique):
Speaking Logic
• Emina Torlak (University of Washington):
Solver-Aided Programming
• Mooly Sagiv (Tel Aviv University):
Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems
• Nikhil Swamy and Jonathan Protzenko (Microsoft Research):
Programming and Proving in F* and Low*
• Andreas Abel (Chalmers/Gothenburg University):
Introduction to Dependent Types and Agda
• Dirk Beyer (Ludwig Maximilian University, Munich, Germany)
Software Model Checking
• Nina Narodytska (VMWare Research):
Verifying Properties of Binarized Deep Neural Networks
• Gordon Plotkin (U. Edinburgh, UK):
Some Principles of Differentiable Programming Languages Research Papers
• Edward A. Lee (UC Berkeley):
Plato and the Nerd - The Creative Partnership of Humans and Technology

Important Dates: Applicants are urged to submit their applications before April 30, 2018, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early.

For information about application and registration, see the school webpage.

### SAT/SMT/AR 2018: International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning

3-6 July 2018, Manchester, UK

We are pleased to announce that the next edition of the SAT/SMT/AR Summer School will take place in Manchester, UK on 3-6th July 2018. Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR) continue to make rapid advances and find novel uses in a wide variety of applications, both in computer science and beyond.

The SAT/SMT/AR Summer School aims to bring a select group of students up to speed quickly in this exciting research area. The school continues the successful line of Summer Schools that ran from 2011 to 2015 as SAT/SMT Summer Schools and added AR in 2016. There will also be a special session on computer algebra to continue the activity of the SC2 summer school in 2017.

Lecturers for this year's summer school have been announced on the school's website and detailed programme of topics will appear soon.

Early registration (£100) has been extended to 20th April. After this the regular rate of £200 will apply. A small number of grants are still available to subsidise registration fees and accommodation costs. Applicants should indicate on the application form whether they wish to be considered for a grant. Grants will be awarded based on need but those applying earlier will be prioritised. Note that we have separate application and registration phases and deadlines apply to application rather than registration.

Applications can be made via this following form. For more information about application and registration, see the registration webpage.

### FOPSS Logic and Learning School

July 1-6, Oxford, UK

The Logic & Learning School is an opportunity to learn from, and interact with, the world's experts leading recent progress in understanding the relationships between logic and learning. These experts come from both academia and some of the leading industrial research labs (Amazon Research and DeepMind).

In the last few decades, logic has emerged as a fundamental paradigm for understanding complex systems. It has turned out to be instrumental in formal methods such as program verification, reasoning about hardware, reasoning about real-time systems and, more recently, probabilistic systems. Machine learning has recently had spectacular successes in fields such as image recognition, game playing, and many areas that involve the extraction of information from large datasets. The use of statistical approaches yields practical solutions to problems that seemed out of reach just a few years ago. The understanding of why these approaches are so successful has lagged behind the empirical successes. Using logic as the foundation to understand machine learning to obtain the best of both worlds is a major challenge.

Complete list of speakers

• Borja Balle (Amazon Research Cambridge) Spectral algorithms for automata learning
• Richard Evans (DeepMind) Inductive logic programming and deep learning
• Nina Gierasimczuk (Technical University of Danemark) Learning and epistemic modal logic
• Varun Kanade (University of Oxford) Statistical learning theory
• Guy Katz (Stanford University and Hebrew University of Jerusalem) Verification of machine learning programs
• Jan Kretínský (Technical University of Munich) Learning for verification
• Stephen H. Muggleton (Imperial College London) Inductive logic programming
• Doina Precup (McGill University and DeepMind) Reinforcement learning
• Dan Roy (University of Toronto) Bayesian learning
• James Worrell (University of Oxford) Computational learning theory

Students and postdocs may also be interested in the FLOC Volunteer Programme.

For registration and further information about the Logic & Learning School (opens early February) see here.

### RW 2018: 14th Reasoning Web Summer School

22-25 Sep 2018, Luxembourg

The research areas of Semantic Web, Linked Data and Knowledge Graphs have received a lot of attention in academia and industry recently. Since its inception in 2001, the Semantic Web has aimed at enriching the existing Web with meta-data and processing methods, so as to provide Web-based systems with intelligent capabilities such as context-awareness and decision support. Over the years, the Semantic Web vision has been driving many community efforts which have invested a lot of resources in developing vocabularies and ontologies for annotating their resources semantically. Besides ontologies, rules have long been a central part of the Semantic Web framework and are available as one of its fundamental representation tools, with logic serving as a unifying foundation. Linked data is a related research area which studies how one can make RDF data available on the Web, and interconnect it with other data with the aim of increasing its value for everybody. Knowledge Graphs have been shown useful not only for Web search (as demonstrated by Google, Bing etc) but also in many application domains. Many advanced capabilities required by Semantic Web, Linked Data and Knowledge Graph application scenarios call for reasoning. Thus, a perspective centered on the reasoning techniques complementing other research efforts in this area is desirable. The Reasoning Web series of annual Summer Schools is devoted to this perspective, and gives insight into the Semantic Web, Linked Data, Knowledge Graph, Ontologies, Rules, and Logic. It was started in 2005 on behalf of the work package " Education and Training (ET) " of the Network of Excellence REWERSE, and since then it has been established as a major annual event in the above mentioned research areas. It is primarily intended for postgraduate (Ph.D. or M.Sc.) students, postdoctoral researchers, young researchers, and senior researchers wishing to learn about Reasoning on the Semantic Web and related issues.

Lecturers of the school:

• Hannah Bast (University of Freiburg)
• Philipp Cimiano (University of Bielefeld)
• Emanuele Della Valle (Politecnico di Milano)
• Guido Gorvernatori (CSIRO)
• Heiko Pauleim (University of Mannheim)
• Steffen Staab (University of Koblenz-Landau)
• Daria Stepanova (Max Planck Institute for Informatics)

For information about the schools, see the website.

## Open Positions

### Data61 Seeking Proof Engineers, Sydney, Australia

If only there were a place where I could prove theorems for money, change the world, and have fun while doing it...

Sounds too good to exist?

In the Trustworthy Systems team at Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities.

We are looking for 3 motivated proof engineers who want to join our team in Sydney, move things forward, and have global impact.

To apply for this position, you should possess a significant subset of the following skills.

• functional programming in a language like Haskell, ML, or OCaml
• first-order or higher-order formal logic
• basic experience in C
• ability and desire to quickly learn new techniques
• undergraduate degree in Computer Science, Mathematics, or similar
• ability and desire to work in a larger team

We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer.

If you additionally have experience

• in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, or Coq, and/or
• with operating systems and microkernels
you should definitely apply!

Apply online at the following links:

This round of applications closes 15 April 2018.

Still studying? We also have internship opportunities!

### PhD scholarships at ANU, Canberra, Australia

The Logic and Computation Group at the Research School of Computer Science, The Australian National University has a number of PhD scholarship available for bright, enthusiastic doctoral students in the following fields:

• Logic and Linguistics (Ekaterina Lebedeva)
• Logic in Computer Science (Rajeev Gore, Dirk Pattinson, Alwen Tiu)
• Non-Classical Logics (Rajeev Gore, John Slaney, Dirk Pattinson)
• Proof Theory (Rajeev Gore, Dirk Pattinson, Alwen Tiu)
• Automated Reasoning (Peter Baumgartner, Rajeev Gore)
• Computer Aided Verification (Sergiy Bogomolov, Michael Norrish, Dirk Pattinson)
• Interactive Theorem Proving (Michael Norrish, Dirk Pattinson)
• Verification of Computational Complexity (Abdallah Saffidine)
• Computer Security Foundations (Alwen Tiu)
• Electronic Voting and Social Choice Theory (Rajeev Gore, Dirk Pattinson)

Potential applicants are encouraged to consult the group's web pages and make direct contact with potential supervisors.

Students will be based at the Research School of Computer Science within the Australian National University. The studentship is a tax-free allowance of A\$ 27,082 (2018 rate) per year, tenable for a maximum of 3.5 years.

Applications are to be submitted electronically here before the closing date, April 20, 2018. Further information about graduate research within Computer Science at ANU, are available here.

The scholarships are open to individuals of any nationality. We are based in Canberra, Australia, the top-ranking region of the 2014 OECD quality of life survey.

The ANU actively seeks to promote diversity in the workplace.

### Postdoc Position VirginiaTech, Blacksburg, Virginia, USA

A postdoctoral position is available with the Systems Software Research Group at Virginia Tech on a project that is investigating verification of x86 machine code. The project vision involves formalizing x86-64 semantics, decompiling program binaries, and investigating techniques to reason about program behaviors, all inside a theorem-prover.

Recent computer science or computer engineering PhD graduates with background and expertise in theorem provers such as Isabelle/HOL, Coq, or ACL2, and with an affinity for defining the formal semantics of languages is sought. We seek candidates with a solid background in at least one of the following topics:

• Theorem proving / formal semantics
• x86 architecture
• Concurrency
• Floating point semantics

Interested candidates should send a CV and cover letter to Dr. Freek Verbeek. Please indicate in your email that you are applying for a postdoc position. The position is for one year, with strong possibilities for additional years. The start date is flexible, but we aim to fill the position as soon as possible. Please also contact Dr. Verbeek for any questions.

### Assistant professorship position, TU Darmstadt, Germany

Software Factory 4.0 project, coordinated by Prof. Dr. Heiko Mantel

The department of Computer Science of Technische Universität Darmstadt invites applications for an assistant professorship "Semantics and Verification of Parallel Programs".

Candidates should have a strong research and publication background in the area of semantics and verification of parallel software systems, and should strive to extend and deepen their research profile in this area. Examples for relevant topics are

• Concurrency Theory
• Construction and Validation of Weak Memory Models
• Formal Modeling of Concurrent Systems
• Program Analyses for Multi-threaded Programs
• Semantics of Concurrent languages
• Separation Logic
• Verification of Efficiently Parallelized Programs

Application deadline: April 22, 2018

More information and details on the application process are available here.

### Post-doctoral position, Loria Nancy, France

Paul Zimmermann

A post-doctoral position will be available in my group (starting October 2018) on the formal proof of the GNU MPFR library. Candidates should have experience with a least one formal proof assistant, for example Isabelle. (Experience with computer arithmetic and/or MPFR is welcome but not required.)

### 16 PhD Positions on Logical Methods in Computer Science, Vienna, Graz, Linz, Austria

TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program on Logical Methods in Computer Science (LogiCS). The doctoral positions are funded for a period of 4 years according to the funding scheme of the Austrian Science Fund.

The Program
LogiCS focuses on logic and its applications in computer science. Successful applicants will work on interdisciplinary research topics covering

• computational logic,
• databases and artificial intelligence,
• computer-aided verification, and
• emerging application domains, such as cyber-physical systems,distributed systems, and security & privacy.

Faculty Members
Austria has a vibrant and highly active and successful logic in computer science community.

Positions and Funding
We are looking for 16 doctoral students, where 30% of the positions are reserved for highly qualified female candidates. The doctoral positions are funded for a period of 4 years according to the funding scheme of the Austrian Science Fund. Additional positions will be available through other funding.

How to Apply
Detailed information about the application process is available on the LogiCS web-page.

The applicants are expected to have completed an excellent master's degree in computer science, mathematics, or a related field. Candidates with comparable achievements (e.g., bachelor of honors) may be considered on a case-by-case basis. Applications by the candidates need to be submitted electronically. The positions will be filled on continuous basis till October 2018. The evaluation of applications will start on 1st of March, 2018.

For further information please write to this address.

### PhD/Post-doc Positions I, Uppsala University, Sweden

Uppsala University announces

• 1 Post-Doctoral Position
• 3 PhD positions
on Techniques for Detecting and Removing Security Vulnerabilities in Software.

The topic for the positions is to develop techniques for detecting and removing security vulnerabilities in software, and applying these techniques in software for IoT devices and for the Web. Techniques that the positions will focus on include program analysis, verification, symbolic execution, testing using fuzzing, taint analysis, model learning; supported by constraint solving and SMT. Among the goals is to significantly extend the power and scalability of such techniques to real-world code bases; in particular, to analyse the widely-used Contiki OS for IoT, and to efficiently and precisely analyse JavaScript code implementing client-side or server-side functionality.

The positions are funded by recent five-year grants from SSF (the Swedish Foundation for Strategic Research) that bring together several research groups at Uppsala University (Bengt Jonsson, Parosh Abdulla, Mohammed Faouzi Atig, Philipp Ruemmer, Kostis Sagonas, Wang Yi) that are world-renowned in the fields of automated verification, programming language implementation, and testing. The work is performed in collaboration with partners at RISE SICS (Simon Duquennoy, Luca Mottola, Shahid Raza, Thiemo Voigt) including developers of the Contiki OS, and the SICS Security lab, as well as the language-based security group at Chalmers (Andrei Sabelfeld).

Application deadline: April 23 2018

For more details and instructions on how to apply see

For more information on what support you can expect see here.

### PhD/Post-doc Positions II, Uppsala University, Sweden

The department of Information Technology, Uppsala University, announces

• 1 Post-doctoral position (2 years, including at most 20% teaching)
• 1 fully-paid PhD position (5 years, including 20% teaching)
on Program Analysis and Code Optimisation using Machine Learning.

The subject of the post-doc position is to develop more powerful techniques for code optimization or code analysis, by applying machine learning techniques (e.g., deep learning) in new ways to extract features from program code. The project will use the result of learning in several possible ways, such as code optimisation that cannot be achieved by applying standard compile-time optimizations, or the automatic verification of correctness properties.

The goal of the PhD position is to find new ways of using machine learning (in particular, methods based on deep neural networks) to improve, extend or replace classical program analyses. Two focus areas are model checking (algorithms that can automatically prove the absence of bugs in programs) and defect prediction (methods that can predict the likelihood of defects in given code segments). The PhD work will be carried out in the context of a collaboration between Uppsala University and Microsoft Research Cambridge. The position is partly funded through a Microsoft Research PhD scholarship, and includes benefits such as summer schools organised by Microsoft Research Cambridge.

Application deadline: April 30 2018

For more details and instructions on how to apply see

For more information on what support you can expect see here.

### Postdoctoral opening at the Università degli Studi di Verona, Italy

The Department of Computer Science of the Università degli Studi di Verona in beautiful Verona, Italy, EU, has an opening for a postdoctoral researcher position in automated reasoning. The position is for two years, it is full-time on research (no teaching duties), and it is flexible in terms of research topic. The candidate is expected to start in September 2018 the latest. Recent PhD graduates in Computer Science or related fields with a thesis in any topic in automated reasoning, broadly meant, are invited to get in touch by e-mail with Maria Paola Bonacina. Applications will be considered as soon as received.

### PhDs and postdocs, Inria Rennes, France

CELTIQUE is looking for PhD candidates and postdocs!

The IRISA/Inria Celtique group in Rennes (France) has several open PhD and post-doctoral position. The positions are funded by David Pichardie's European ERC VESTA project (2018-2023). Postdoc applicants must have a PhD in Computer Science. PhD applicants must have a Master in Computer Science. We seek candidates with a solid theoretical background in Computer Science, in at least one of the following topics:

• formal semantics of programming languages
• compiler implementation
• abstract interpretation
• Coq proof assistant

Postdoc positions are one year, with the possibility of extension to a second year. All position may start after September 1st 2018.

Candidate that are specially interested by compiler verification will also be considered for a postdoc in the national ANR project Discover, and can negotiate a starting time earlier than September.

The working language is English, knowledge of French is not required. The successful candidate will join the Celtique team at IRISA, INRIA Rennes.

Applicants should send their curriculum vitae, cover letter and names/contact information of two references to David Pichardie. Recommendation letters should be sent to David Pichardie directly.

Potential research projects

• Verification of static analysis with the Coq proof assistant
• Formal verification of abstract interpreters using the Galois connection framework inside Coq
• Formal verification of state-of-the-art SSA-based compiler optimisations
• Advanced abstract interpretation for software security (Java, C, or assembly programs)
• Innovative techniques for extraction of efficient code with Coq

### Assistant Professor Position (tenured), University of Rennes, France

As a pillar of the French Cybersecurity Excellence Cluster based in Rennes, the University of Rennes is opening an Assistant Professor Position (tenured) in Software Security for its , with teaching in our newly open EIT Digital Cybersecurity Master.

Rennes is the Capital of Brittany, located close to the sea and 1 hour 25' West of Paris through a new dedicated High Speed Train line. Economically attractive, Rennes has a growing research and higher education activity (63000 students, 5000 researchers), a vibrant cultural life and a widely acknowledged quality of life.

The recruited person will join one of the IRISA teams working in cybersecurity, such as CAIRN, CELTIC, CIDER, DIVERSE, DRUID, EMSEC, MYRIADS or TAMIS. The main research topics addressed by the teams involved in this area are the security of information systems including intrusion detection, cryptographic protocols, privacy protection, security of embedded and communicating security policies, database security or the security of distributed systems such as cloud computing, computing grids or peer-to-peer networks, security of micro-architecture and compilation.

More information for applying can be obtained with the leaders of these teams.

The successful candidate will have a PhD in Software Security, a track record of international publications in leading conferences and journals, and motivation for and experience with teaching and student supervision.

Since teaching within the context of EIT Digital is fully in English, and the working language at IRISA is also English, it is not mandatory for the candidate to speak French. An excellent command of the English language is however required.

The University of Rennes is an equal opportunity employer and we value the diversity of our staff and students. We particularly welcome applications from female candidates who are currently under-represented in the academic staff.

### Formal verification jobs, Apple Austin, USA

Positions for formal verification engineers are available at Apple in the Austin FV team.

If you might be interested, you can check out our listings:

• Choose Austin as the location
• Search for the keywords "Formal Verification"

See in particular:

• "Formal Verification Engineer" (#113447713)
• "Processor Formal Verification Engineer" (#33077581)

Also feel free to contact Jared C. Davis or Jim Grundy if you'd like to know more.

### Postdocs in assurance research, Silicon valley, USA

We are seeking postdoctoral researchers to work in a small, agile team at NASA Ames Research Park in Silicon Valley on the multi-year QUASAR project (Quantifiable Assurance Cases for Trusted Autonomy), part of the US Defense Advanced Research Projects Agency (DARPA) Assured Autonomy research program.

The successful candidates will undertake fundamental research into the foundations of 'Dynamic Assurance Cases' (DACs), which aim to provide quantified assurance of trustworthiness in the design and operation of learning-enabled autonomous systems.

Individual positions are available on foundations, quantification, and assurance aspects for DACs:

The foundations postdoc, in particular, is relevant to Isabelle proof engineers as we anticipate extensive formal verification of the mathematical characterization and operational semantics of DACs.

Please contact Iain Whiteside directly if you have any questions,

## Obituaries

### Prof. Wen-Tsun Wu

by Xiao-Shan Gao
KLMM, Chinese Academy of Sciences

Professor Wen-Tsun Wu passed away on May 7, 2017, a few days ahead of his 98th birthday. Wu is one of the most influential Chinese mathematicians and computer scientists. In his early years, he made fundamental contributions to algebraic topology. In the late 1970s, Wu proposed the Wu's method of geometric theorem proving and founded the school of Mathematics Mechanization. His study on the ancient Chinese mathematics opened a new era in the field of history of Chinese mathematics. He also made contributions in the area of algebraic geometry, invariant theory, complex geometry, and game theory. Professor Wu was awarded the Herbrand Award for Distinguished Contributions to Automated Reasoning in 1997 for his work on automated geometry theorem proving. An eulogy for Professor Wen-Tsun Wu can be found here.

## The Editor's Corner

Philipp Rümmer
(now former) co-editor of the AAR newsletter

After a bit more than one year as co-editor of the newsletter (the first newsletter that Sophie and I edited together was the March 2017 edition, after taking over from Jasmin), it turns out that it is already time again for a change of organisation. I am grateful for the offer of the AAR Board and the CADE Board of Trustees to take over the role of AAR and CADE secretary from May 1st, and am happy to accept! Since my time is limited (and getting more and more scarce it feels) the immediate consequence is, however, that I will have to step down as co-editor and fully hand over those duties to Sophie, starting with the next newsletter.

Getting the five newsletters out was certainly a lot of fun, though sometimes quite a bit of work as well. After a while, everything might start to look like a call for papers. I would like to thank Sophie for the good collaboration, and wish her all the best for the next newsletters!

* * *

This brings me to a point that I experienced as frustrating during my time as editor: the second a newsletter is released, it is already outdated! This can be for several reasons: besides the many conferences and workshops listed, there were always a few that we managed to miss; dates and submission deadlines get extended all the time, and the newsletter is not updated; or there simply turn out to be mistakes in a newsletter. The moment we send out the mail with the newsletter, we usually start getting requests for changes, last-minute additions, etc.; unless factual errors are reported, we normally have to decline, and refer to the next newsletter.

As a result, I am wondering whether some sections of the newsletter (the ones listing calls for papers) should be turned into a "living" document to which new events can be added continuously, old events are removed automatically, and updates can be made at any point. I imagine a system similar to the confsearch web page, but maintained centrally and focusing on CADE and AAR events. Generating the corresponding sections of the newsletter would then boil down to extracting a snapshot at a particular point in time. Thoughts?