# Association for Automated Reasoning

July 2018

## From the AAR President, Larry Wos

In contrast to the focus in many of the columns I have written, a focus on proving one or more theorems, I suspect at least some of you would like a challenge that is of a more general nature. I have in mind a challenge that would, if met, have a possibly dramatic effect on the performance of automated reasoning programs. If you glance at an experiment with such a program, an experiment that did reach the goal but took considerable CPU time to reach the goal, you might discover that many, many conclusions were drawn and then discarded because of being identical to or an instance of a conclusion already retained. In other words, both forward and back subsumption (so-to-speak) wasted much time, perhaps a rather large fraction of the time the program took to return the desired answer to the question under consideration. Information that is subsumed is (in effect) redundant information. In the presence of reflexivity, `x = x`, almost never is it of use to learn that `a = a` and `b = b`, for example. In a problem in group theory, instances of the axiom of left identity are seldom edifying, instances of (where e denotes the identity) `e+x = x`.

In general, the challenge offered here asks for a way to avoid deducing most or all of the so-called redundant information. Since I am often preoccupied with various types of strategy, the challenge here asks for the formulation of a strategy to be employed to save the CPU time spent on deducing and discarding redundant information. I have no idea how to address the challenge, and I suspect an understandable immediate reaction is that no appropriate strategy can be formulated. But, especially for those who might enjoy history, and also to show how apparently formidable obstacles were overcome, I turn to the early 1960s.

Let us look at a different aspect of time that can be wasted. Generally speaking, if a program spends huge amounts of time deducing conclusions that have no relevance to the theorem to be proved, that time is wasted. Such was the case in the early 1960s; indeed, a simple theorem in group theory was in focus with the obvious objective of finding a proof. The theorem asserted that commutativity holds (is provable) for groups in which the square of every element `x` is the identity `e`. The proof eluded us, even when using a fine program designed and implemented by Dan Carson at Argonne National Laboratory. The attempt ran out of memory -- specifically because too many clauses were deduced before a proof was found. That simple exercise in group theory was the wellspring for the formulation of the set of support strategy.

In the set of support strategy, the program is prevented from applying the inference rule(s) in use to a set of clauses none of which are in a list designated as the set of support list. The recommendation for the use of the strategy, in general, is to place all of the axioms of the area under study outside of the set of support list, list(sos) for Bill McCune's OTTER. Typically, one places in the set of support list the so-called special hypothesis, if such exists, and possibly the denial of the conclusion of the theorem. For example, in the context of the cited simple exercise from group theory, you would place `xx = e` and, possibly, `ab != ba` in the set of support list. With such a placement, the program would not be able, while using the set of support strategy, to apply an inference rule to a set, say, consisting of left identity and associativity. In other words, the program would not be exploring group theory as a whole. For McCune's OTTER, the axioms of a group would be placed on list(usable) and used only to complete the application of an inference rule. Among conclusions not drawn would be various lemmas about group theory, most or all would not be useful if, for example, trying to prove commutativity for groups in which the square of `x`, for all `x`, is the identity `e`.

But, you might well argue, isn't such a lemma essential? And the surprising answer is no. Intuition might suggest the need for such a lemma, but such is not the case -- provided, in general, that the complement of the chosen set of support is itself satisfiable. Indeed, without this lemma, a proof is guaranteed to be found when the complement of the chosen set of support is satisfiable -- quite intriguing! No wonder, then, that McCune considered this strategy to be very deep.

And with the use of the strategy, which restricts the actions of an automated reasoning program, the simple exercise was crushed. For one aspect, many conclusions were not drawn that otherwise would have been drawn, using up too much time. The use of the set of support strategy requires no CPU time (except in rather bizarre cases). This characteristic of the strategy is critical especially for much, much harder theorems.

As for the approach or strategy I have challenged you to develop, one that avoids generating redundant conclusions, some CPU time most likely will be required for its use. The aim is, of course, to minimize that time.

To further set the stage for the challenge I am issuing, I return to a study I made with my colleague D. Ulrich in 2006. The area of logic concerned the formulas known, respectively, as `B`, `C`, and `I`. The goal was to deduce from the following proposed single axiom the axiom system consisting of `B`, `C`, and `I`, but to find a very short proof, if such existed; the function `i` denotes implication.

```P(i(i(i(x,x),i(y,z)),i(i(i(i(z,u),u),v),i(y,v)))).
```

The theorem to prove is the following in negated form.

```%  negation of the join of B, C, and I.
-P(i(i(a1,i(b,a2)),i(b,i(a1,a2)))) | -P(i(a1,a1)) | -P(i(i(a1,b),i(i(a2,a1),i(a2,b)))).
```

The only inference rule in use was hyperresolution, coupled with the following clause for condensed detachment.

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

Although a proof of length 20 was found in less than 2 CPU-seconds, far more CPU time was used to find a marvelous 16-step proof. More piquant, the 16-step proof happens to be level 10, not so deep a proof.

```-----> EMPTY CLAUSE at 65197.30 sec ----> 1324675 [hyper,2,1321737,9972,1322447].
```

But what took so much time? Well, the following statistic sheds some light.

```clauses forward subsumed  880401
```

Since the number of clauses forward subsumed is more than half of the number retained when a 16-step proof was found, this data suggests that much CPU time was consumed in the generation and then discarding of redundant information. Additional clauses were back subsumed, more than 200,000. The computer time it takes to deduce and retain a clause is not much more than the time it takes to deduce and discard a clause. Can you formulate a strategy that enables a program to avoid the generation of such a huge amount of useless information, useless because of being redundant, as established by being subsumed?

Similarly, at least for OTTER, clauses are discarded if one of their properties yields a value larger than assigned in the input, such as assigned with `max_weight` or with `max_distinct_vars`. What about finding a strategy to quickly predict such occurrences and avoid deducing such clauses? I have proofs found after five days in real time. If that time could be reduced to three, what an improvement!

Perhaps for a beginning, if you study the clauses discarded by, say, subsumption during a long experiment and if you view those discarded clauses in relation to the retained item that enabled the discarding, can you identify properties of the retained clause that can be used ahead of time to save most of the time used in discarding redundant information?

Note that I say "save most of the time": recall that employing the set of support strategy costs no time -- yours or the program's.

## Announcement of the 2017 Herbrand Award

Christoph Weidenbach, President of CADE Inc.

The 2018 Herbrand Award for distinguished contributions to automated reasoning will be presented to Bruno Buchberger for the invention, implementation, and analysis of the Gröbner-basis method, resulting in the reshaping of symbolic computation towards comprehensive and widely applicable tools.

Christoph Weidenbach, President of CADE Inc.

We welcome all participants of IJCAR 2018 to join the CADE business meeting on Tuesday, July 17th at 4pm. The agenda includes the following topics:

• trustee nominations
CADE membership currently coincides with membership in the Association of Automated Reasoning (AAR). Membership in the Association of Automated Reasoning has so far been interpreted as including all persons who have attended at least one CADE or IJCAR in the past. Over the decades this has resulted in a huge number of members who are either no longer active in automated reasoning or have even retired. The CADE trustees, in agreement with the AAR board, suggest splitting AAR and CADE membership and limiting CADE membership to all persons registered for at least one the last three CADEs (including IJCAR).

## Conferences, call for participation

### FLoC 2018: The Seventh Federated Logic Conference, Call for Participation

July 6-19, 2018, Oxford, England, UK

During the past forty years there has been extensive, continuous, and growing interaction between logic and computer science. In many respects, logic provides computer science with both a unifying foundational framework and a tool for modeling. In fact, logic has been called "the calculus of computer science", playing a crucial role in diverse areas such as artificial intelligence, computational complexity, distributed computing, database systems, hardware design, programming languages, and software engineering.

The Federated Logic Conference brings together several international conferences related to mathematical logic and computer science.

You are warmly invited to participate in FLoC 2018. Registration is now open and we remind speakers and participants to book accommodation as soon as possible, as Oxford is popular in the summer.

Conferences
FLoC 2018 brings together nine major international conferences related to mathematical logic and computer science:

Please refer to the individual websites for conference-specific information.

Workshops
In addition to conferences, FLoC 2018 will also feature 70+ workshops (7-8 July, 13 July, and 18-19 July).

Events
Other events are also planned, such as a public lecture or a public debate.

Late registration is open until June 25th, 2018. On site registration will be possible during the conference.

## Conferences, call for papers

### MIWAI 2018: the 12th Multi-disciplinary International Conference on Artificial Intelligence, call for papers

November 18-20th, 2018, Hanoi, Vietnam

The theme for this year's event is "Intelligent World". The main objective of the conference is to present the latest research and results of scientists related to AI topics. MIWAI 2018 provides opportunities for the delegates to exchange new ideas and establish future collaborations. This year the conference is organized by Mahasarakham University, with association of Vietnam Academy of Science and Technology and University of Science and Technology of Hanoi, Vietnam.

MIWAI aims to promote AI research in both theoretical and applied research addressing real-world applications. We encourage researchers to submit their unpublished papers in the following areas, but not limited to:

• Theoretical Foundation: Cognitive Science; Computational Philosophy; Game Theory; Graphical Models; Knowledge Representation and Reasoning; Logic; Fuzzy Logic; Multi-agent Systems; Neurosciences; Probabilistic Reasoning; Qualitative Reasoning; Uncertainty.
• Cognitive Computing: Affective Computing; Computer Vision; Natural Language Processing; Self-aware Systems; Speech Recognition; Social Cognition
• Computational Intelligence: Artificial Intelligence; Deep Learning; Evolutionary Computing; Machine Learning; Pattern Recognition; Planning and Scheduling; Social Computing; Swarm Intelligence
• AI Applications: Ambient Intelligence; Big Data Analysis; Biometrics; Bioinformatics; Brain Machine Interface; Chatbots; Creative Computing; Decision Support Systems; E-commerce; Energy Management; Health Assessment; Industrial Applications of AI; Intelligent Information Systems; Knowledge Management; Telecommunications and Web Services; Security and Privacy Management; Surveillance; Spam Filtering; Software Engineering; Social Networking Security; Semantic Web; Robotics; Recommender Systems; Sport and Rehabilitation; Virtual Reality & Augmented Reality.

Important Dates:

• Conference dates: November 18-20, 2018
• Submission deadline: July 11, 2018 (11:59PM UTC-10)
• Notification release: August 5, 2018
• Camera-ready and early bird registration due: August 20, 2018.

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

### LPAR-22: Logic for Programming, AI & Reasoning, call for papers

November 16-21, 2018, Awassa, Ethiopia

The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices.

Topics of interest include, but are not limited to:

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

Important Dates:

• Abstract submission 6th August 2018
• Paper submission 13th August 2018
• Final version 15th October 2018
• Early registration 15th October 2018
• Workshops 16th November 2018
• Conference 17-21st November 2018

Information about the submission process are available on the conference web page.

## Workshops

### LuxLogAI 2018: Luxembourg Logic for AI Summit, call for posters and abstracts

September 17-26, 2018, Luxembourg, Luxembourg

The Luxembourg Logic for AI Summit (LuxLogAI 2018) brings together the 2nd International Joint Conference on Rule and Reasoning (RuleML+RR 2018), the Reasoning Web Summer School (RW 2018), the Global Conference on Artificial Intelligence (GCAI 2018), DecisionCAMP 2018 and the annual meeting of the Deduction Systems group (Deduktionstreffen 2018) of the German Gesellschaft für Informatik (GI).

With its special focus theme on methods and tools for responsible AI, a core objective of LuxLogAI is to present the latest developments and progress made on the crucial question of how to make AI more transparent, responsible and accountable.

First Call For Posters
RuleML+RR 2018 calls for additional short poster papers related to theoretical advances, novel technologies, and innovative applications concerning knowledge representation and reasoning with rules. A Best Poster Award will be given to the best poster presentation.

The full Call for Posters, including submission details, is available here.

Important dates:

• Poster paper submission: 1 August 2018
• Author notification: 15 August 2018
• Camera-ready submission: 31 August 2018

First Call For Abstracts
The annual meeting Deduktionstreffen (Deduktionstreffen 2018) is the prime activity of the Interest Group for Deduction Systems (FGDedSys) of the German Informatics Society (Gesellschaft für Informatik). It is a meeting with a familiar, friendly atmosphere, where everyone (not only the German community) interested in deduction can report on their work in an informal setting. The Deduktionstreffen will also host the annual general meeting of the members of FGDedSys. Contributions on all theoretical, experimental and application aspects of deduction are welcome.

Important dates:

• Early bird submission: 5 July 2018 (Notification: 15 July 2018)
• Standard submission: 5 August 2018 (Notification: 15 August 2018)
• Deduktionstreffen: 21 September 2018

First Call For Applications
In order to give PhD students and Postdocs (with limited funding) the opportunity to attend LuxLogAI, the organizers are awarding a number of grants to motivated applicants. In return, successful applicants are asked to assist the local organization team during the conference.

For further details, including how to submit your application, visit this web page.

Important dates:

• Early bird application deadline: 30 June 2018
• Successful applicants will be notified before: 15 August 2018
• Second round application deadline: 20 August 2018
• Successful applicants will be notified on: 1 September 2018

### ACL2 2018: 15th International Workshop on the ACL2 Theorem Prover and Its Applications, call for papers

November 5-6, 2018, Austin, Texas, USA

The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.

Topics include:

• Software or hardware verification with ACL2
• Formalizations of mathematics in ACL2
• Libraries and tools for ACL2
• User interfaces for ACL2
• Novel uses of ACL2
• Experiences with ACL2 in the classroom
• Reports of and proposals for improvements of ACL2
• Comparisons with other theorem provers
• Comparisons with other programming or specification languages
• Challenge problems and their solutions
• Foundational issues related to ACL2
• Implementations connecting ACL2 with other systems

Important Dates (extended):

• Abstract submission: July 7, 2018
• Paper submission: July 14, 2018
• Author notification: August 25, 2018
• Camera ready: September 25, 2018
• Workshop: November 5-6, 2018

### CCC 2018: Continuity, Computability, Constructivity? From Logic to Algorithms, call for papers

September 24-28, 2018, Faro, Portugal

CCC is a workshop series bringing together researchers from exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation.

Scope: The workshop specifically invites contributions in the areas of

• Exact real number computation,
• Correctness of algorithms on infinite data,
• Computable analysis,
• Complexity of real numbers, real-valued functions, etc.
• Effective descriptive set theory
• Scott's domain theory,
• Constructive analysis,
• Category-theoretic approaches to computation on infinite data,
• Weihrauch degrees,
• And related areas.

Information about the submission process is available on the workshop web page.

## Summer schools

### VTSA 2018: UniGR Summer School on Verification Technology, Systems and Applications

August 27-31, 2018, Nancy, France

The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organized by Inria Nancy, the Max-Planck-Institut für Informatik in Saarbrücken, and the Universities of Liège and of Luxembourg, and will take place at the research center Inria Nancy - Grand Est in Nancy, France, from August 27 to 31, 2018.

The following speakers have agreed to lecture at the school:

• David Basin: Formal Methods for Security Protocols
• Jean-Christophe Filliâtre: An Introduction to Deductive Program Verification
• Peter Lammich: Algorithm Verification with the Isabelle Refinement Framework
• Anca Muscholl: Distributed Synthesis
• Carsten Sinz: Bounded Model Checking of Software for Real-World Applications

Participation to the school is free to anybody holding at least a bachelor degree or equivalent; it includes the lectures, coffee and lunch breaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to Stephan Merz including

• a one-page CV,
• an application letter explaining your interest in the school and your experience in the area, and
• a copy of your bachelor (or equivalent or higher) certificate.
The deadline for application is July 8, 2018. Notification of acceptance will be given by July 11, 2018.

Full details can be found on the school Web page.

### ISSISP 2018: the 9th International Summer School on Information Security and Protection

July 9-13, 2018, the Australian National University, Canberra

There is an increasing need for Software Security and Protection due to the growing sensitivity of user data coupled with the ubiquitous nature of computing systems ranging from tiny embedded devices to powerful data centres.

The International Summer School on Information Security and Protection (ISSISP) highlights this need by bringing internationally renowned speakers from diverse fields in Computer Science such as Software Engineering, Formal Methods, Computer Architecture, Operating Systems, and Programming Languages.

In particular, topics to be covered include vulnerability detection and analysis, software forensics, and information flow control. The summer school caters towards students and professionals from academia, government, and industry. Courses will include both lectures and hands-on sessions.

ISSISP is open to students, academics, and professionals from academia, government, and industry. The number of attendee places is strictly limited. Prospective attendees should submit an expression of interest here. Expressions of interest will continue to be reviewed until the first day of the School (9th July). Please contact this address with any specific questions regarding registration.

### 1st International Summer School on Proof Theory

September 2-5, 2018, Ghent, Belgium

The aim of the summer school is to cover basic and advanced topics in proof theory. The focus of the first edition will be on structural proof theory, ordinal analysis, provability logic, automated theorem proving, and philosophical aspects of proof. Other areas like reverse mathematics, proof mining, and proof complexity will be covered at the co-located workshop, and in follow up summer schools. The intended audience is advanced master students, PhD students, postdocs and experienced researchers in mathematics, computer science and philosophy.

• Deadline for registration: 15 July 2018
• Limited places, assigned according to first-come-first-served

## Open Positions

### PhD Position on the formalization of automated reasoning in Isabelle

Prof. Christoph Weidenbach, Dr. Jasmin Blanchette, MPI Informatics, Germany

The Automation of Logic group, led by Dr. Christoph Weidenbach, is looking for a PhD student to work on the formalization, in the Isabelle proof assistant, of the metatheory of automated reasoning.

Researchers in automated reasoning spend a substantial portion of their work time developing logical calculi (e.g., DPLL, resolution, and superposition) and proving metatheorems about them. These proofs are typically carried out with pen and paper, which is error-prone and can be tedious. As part of the IsaFoL (Isabelle Formalization of Logic) project, we are interested in formalizing results concerning existing logical calculi. The motivation is manifold:

• Formalization can offer a convenient means to study extensions, generalizations, or variations of existing calculi.
• Once we have developed suitable libraries and a methodology, formalization becomes not only a way to gain more trustworthiness about the results, it also is more convenient than pen and paper (or LaTeX).
• Isabelle includes automatic theorem provers as proving backends. There is an undeniable thrill in applying our own tools and find ways to improve them further, based on practical experience with them.

The PhD project is about verifying a functional implementation of a superposition prover: a minimalistic version of E, SPASS, or Vampire, based on the superposition calculus, a saturation loop, simplification, and subsumption. The project would be executed in close collaboration with Jasmin Blanchette at Vrije Universiteit Amsterdam and members of the Automation of Logic group in Saarbrücken, including Mathias Fleury, Sophie Tourret, and Uwe Waldmann.

The candidate should ideally have some experience with automated or interactive theorem proving, or with some closely related area of theoretical computer science (e.g., term rewriting). To apply, please send your personal record (including CV, grade transcripts, and contact information for two references) by email to Jennifer Müller.

### Ph.D. Research Project on Big Data Monitoring

Prof. David Basin and Dr. Dmitriy Traytel, ETH Zürich, Switzerland

The Information Security Group carries out research on methods and tools for the analysis and construction of safe and secure systems. This includes methods for specifying systems, developing systems in correctness-preserving ways, and verifying or testing existing systems and infrastructures. Our goal is not only to build and analyze novel systems and security solutions, but also to develop better methods and tools for system engineering and quality assurance activities.

We have an open Ph.D. research position on "Big Data Monitoring". The project's main objective is to develop and implement efficient, parallelized algorithms capable of checking whether a high-volume and high-velocity stream of events comply with given rules. The rules are formulated in an input language that allows users to express temporal and data dependencies between different events in the data feed in a simple and intuitive manner. If any of the rules are violated, a compact output of the data that caused the violation should be produced.

The ideal candidate for this position is an enthusiastic, outstanding researcher with a strong background and interest in one or more of the following areas:

• formal methods or mathematical logic,
• automata theory or model checking or runtime verification,
• stream processing or data stream management systems.

Candidates with a strong theoretical background in related areas are also encouraged to apply. ETH Zürich regulations require PhD candidates to hold a Master's or equivalent degree (e.g. Diplom). The project is funded by the Swiss National Science Foundation and will be supervised by Prof. David Basin and Dr. Dmitriy Traytel.

The Ph.D. student will be a paid employee of ETH Zürich. Salary and employment conditions are attractive. ETH Zürich regulations require doctoral students to hold a Master's or equivalent degree (e.g. Diplom).

Zurich is a diverse and multicultural city, which is consistently rated among the best cities in the world in which to live. We favor the same sort of diversity that defines Zurich's cultural makeup and encourage anyone matching the profile above to apply, regardless of where you are from.

Applications should include a curriculum vitae, a brief description of research interests, transcripts of grades, 2-3 letters of recommendation from teachers or employers, and, if possible, the Master's or Bachelor's thesis and publications. Applications and informal inquiries should be sent to Dmitriy Traytel

ETH Zürich specifically encourages women to apply with a view towards increasing the proportion of female researchers.

### Ph.D. Research Project on Privacy, Data Protection, and Access Control

Prof. David Basin, ETH Zurich, Switzerland

We have open Ph.D. research positions in the area of Privacy, Data Protection, and Access Control. We seek to hire one or more doctoral students who will carry out research on the development of novel control and auditing mechanisms that enhance data protection, e.g., by ensuring that data is only used for the purposes it is collected. This will involve developing and prototyping new access control mechanisms as well as using code analysis and machine learning methods to extract and determine "purpose" from code and other system artifacts. In addition and independent of foundational research on these topics, there will be the opportunity to work with our industrial partners to evaluate the developed techniques on realistic large-scale systems.

The ideal candidate for this position is an enthusiastic, outstanding student with a strong background and interest in one or more of the following areas:

• formal methods
• information security or cryptography,
• programing language theory and methods and tools for program analysis
• machine learning

Candidates with a strong theoretical background in related areas are also encouraged to apply. ETH Zurich regulations require PhD candidates to hold a Master's or equivalent degree (e.g. Diplom). The Ph.D. student will be a paid employee of ETH Zurich. Salary and employment conditions are very attractive.

Applications should include a curriculum vitae, a brief description of research interests, transcripts of grades, 2-3 letters of recommendation from teachers or employers, and, if possible, the Master's or Bachelor's thesis and publications. Applications and informal inquiries should be sent to Esfandiar Mohammadi.

ETH Zurich specifically encourages women to apply with a view towards increasing the proportion of female researchers.

### Research Associate in Compositional Reasoning for High-Assurance Many-Core Software

Dr Alastair Donaldson, Dr John Wickerson, Imperial College London, UK

The position is for 2.5 years, with a possible extension. Closing date for applications: 1 July 2018.

We are looking to hire a motivated Research Associate to join IRIS: Interface Reasoning for Interacting Systems - an exciting new EPSRC-funded Programme Grant led by University College London, Imperial College London, Queen Mary University of London and the London School of Economics. The goal of the IRIS project is to study and devise novel approaches for analysing large systems in a scalable manner via reasoning at the level of inter-component interfaces. The current post at Imperial College London will be jointly supervised by Dr Alastair Donaldson (Department of Computing) and Dr John Wickerson (Department of Electrical and Electronic Engineering, EEE), and will focus on reasoning about software designed to run on many-core architectures and other highly parallel accelerators. There will be a special focus on high-assurance software that needs to leverage many-core technology due to performance constraints, and yet which needs to be highly reliable.

Imperial's Computing and EEE departments are both leading departments in their respective subjects among UK Universities, and have consistently been awarded the highest research rating from the Higher Education Funding Council. The 2014 REF assessment ranked the Department of Computing third (first in the Research Intensity table published by The Times Higher), and the EEE department first for research in the country's EEE sector.

Reasoning about many-core software is challenging for various reasons, including the state-space explosion that arises due to interleaving of concurrent components, the subtle relaxed memory semantics of modern architectures and programming languages, and the difficulty of automated testing in the face of the nondeterminism that arises from both of these concerns. As part of the IRIS project we will focus on making both theoretical and practical advances in reasoning capabilities for many-core software, following various lines of inquiry including (but not limited to):

• Specification-based conformance testing. For example: can a concurrent program's pre- and post-conditions be used to automatically generate conformance tests to check that an implementation meets its specification?
• Composition of memory models. For example: if a GPU, an FPGA accelerator and an ordinary processor all have access to the same memory locations, as they do on modern system-on-chip devices, what guarantees can programmers rely on?
• Validation of many-core compilers. For example: can automated program generation techniques for testing compilers be extended and combined with systematic concurrency testing techniques to check that many-core code is compiled correctly?
• Refinement-based parallel program construction. For example, can the common practice of deriving a high performance parallel program via a series of equivalent, increasingly optimised program variants be formalised and mechanised to allow automated exploration of the space of equivalent-by-construction implementations?
The techniques we develop will be evaluated on case studies stemming from the academic and industrial partners of the IRIS project, with a particular focus on high-performance implementations of security- and safety-critical functions, e.g. arising in cryptography or machine vision.

Duties and responsibilities
The successful candidate will work with the investigators at Imperial to conduct original research in areas relevant to the IRIS project (including for example some of the research areas outlined above), and will collaborate with the investigators and researchers involved in the IRIS project more broadly to amplify the technical depth and potential impact of the work. In addition to frequent research meetings at Imperial, the candidate will attend regular IRIS project meetings to engage with the other academic and industrial partners, and will present work arising from the project at international meetings.

Essential requirements
The breadth of the project allows for flexibility in the profile of applicants, ranging from applicants with backgrounds in formal methods or programming languages theory who are interested in applying fundamental theory to challenging engineering problems, to applicants with a background in system-building who are interested in how to reason about systems. All applicants require the following:

• a strong computing background;
• experience either in working on state-of-the-art theoretical frameworks for program reasoning (such as program logics), or building and working with practical verification/testing tools;
• a desire to learn about many-core systems in detail;
• a strong research track record and publications in a relevant area with an ambition to lead high-quality research; and
• excellent verbal and written communication skills.
The successful applicant will have, or be near to completing, a PhD (or equivalent) in an area pertinent to the subject area.

Please get in touch with Alastair Donaldson or John Wickerson for informal enquiries.

### Open Positions for Ph.D. candidates and Postdocs in Information-Flow Security and Side-Channel Analysis

Prof. Dr. Heiko Mantel, TU Darmstadt, Germany

The chair MAIS at TU Darmstadt, led by Prof. Dr. Heiko Mantel, is offering three positions for Ph.D. candidates and Postdocs in the following areas:

1. information-flow analysis techniques for object-oriented programs at the level of source code and byte code based on compositional and precise verification techniques
2. experimental analysis of side-channel vulnerabilities in cryptographic implementations and generation of attacks exploiting such vulnerabilities
3. program analysis techniques for detecting side-channel vulnerabilities in cryptographic implementations and for assessing the seriousness of such vulnerabilities

The positions are available immediately and applications will be considered until the positions are taken. For more information and how to apply, see this web page.

### Fully-funded PhD studentship on specification and verification of C++ data structure libraries

Dr. Mark Batty, University of Kent, UK

The UK Research Institute in Verified Trustworthy Software Systems and the UK's National Cyber Security Centre have provided a PhD studentship to work with Mark Batty at the University of Kent in Canterbury, UK. The position is part of the "Specification and verification of C++ data structure libraries" project.

Details and how to apply on this web page.

The studentship covers UK/EU fees, a travel budget and a stipend for 3.5 years. There is an option to teach, but no requirement. Non-EU students are welcome to apply but are subject to higher fees and would need to find funding for the difference. The position starts in September 2018. Applicants must have, or be about to complete a degree in Computer Science or Mathematics at the BSc or MSc level.

Please do contact Mark Batty if you are interested.

### Postdoctoral positions in Formal Methods

Prof. Clark Barrett, Stanford University, USA

Two postdoctoral research positions are available at Stanford University under Professor Clark Barrett. Applications are being accepted now with a target start date for both positions of Fall 2018. Starting salary is \$80,000 per year and includes benefits. Any updates will be posted on this website.

Verification of Neural Networks
The first position will focus on tools and techniques for applying formal verification to deep neural networks. The project aims to extend and apply the highly-successful Reluplex tool. Applications include safety-critical systems such as self-driving cars and drone aircraft.

The ideal applicant must have:

• a PhD in Computer Science or a closely related field
• strong programming skills, especially in C++
• a strong publication record in formal methods or a related field

Hardware Verification
The second position will focus on building a new generation of open-source tools for hardware verification and model checking. This person will work closely with the Stanford Agile Hardware Center and the CVC4 SMT Solver team.

The ideal applicant must have:

• a PhD in Computer Science or a closely related field
• strong programming skills, ideally in C++ and/or Python
• a strong publication record in formal methods or a related field
In addition, in-depth knowledge of the inner workings of SMT solvers is a plus, as is familiarity with digital design and existing hardware verification techniques.

Stanford University
Stanford University is among the top universities in the world in computer science research. Located in the heart of silicon valley, it is known for an exciting and fast-paced research environment combining exceptional academic talent with abundant opportunities to collaborate with top high-tech companies. The weather is also really nice.

Application details
Questions and applications can be sent to Prof. Clark Barrett. Applicants should include their CV, including a list of publications, together with a brief statement outlining their suitability for the project and the names of at least two references.

### Fully Funded EPSRC iCASE PhD Scholarship: Verification of Real Time Systems

Prof. Markus Roggenbach, Swansea, UK

• Closing date: 2 July 2018
• Start date: October 2018

This project offers an exciting opportunity to combine theory and practice in the verification of real time systems, based on research questions posed by Siemens Rail Automation UK. We are looking for an ambitious candidate, keen to undertake challenging collaborative research with industrial impact.

### PhD student position in logic and verification

Prof. David Pym, Dr. James Brotherston, London, UK

A PhD studentship in the area of logic and verification is available at UCL's PPLV group.

Details are available on the scholarship web page under the title "PhD Studentship in Logic and Verification at UCL".

Closing date is 17 July 2018.

### PhD student position in modelling and verification of software systems

Prof. Alexandra Silva and Dr. Matteo Sammartino, London, UK

Applications are invited for a PhD studentship at University College London, under the supervision of Prof. Alexandra Silva and Dr. Matteo Sammartino.

The start date is flexible. It should be in September 2018 at the latest.

The studentship is funded by the UK Research Institute in Verified Trustworthy Software Systems, and will be carried out within the Programming Principles, Logic and Verification (PPLV) group. The PPLV group offers an exciting research environment, with outstanding connections with cutting-edge industry.

Potential applicants are encouraged to contact Prof. Silva and Dr. Sammartino for further information and expressions of interest. Applications should be made via the UCL evision system.

### Research Associate position on Verification of Linear Dynamical Systems

University of Oxford, UK

The department of Computer Science has a new opening for a Research Associate in Verification of Linear Dynamical Systems, working with Professor James Worrell, and funded by an Established Career Fellowship from EPSRC. The overall goal of this proposal is to develop techniques to solve fundamental computational problems arising in the verification of discrete and continuous linear dynamical systems, including Markov chains, linear recurrence sequences, linear while loops, and linear differential equations.

The closing date for applications is 12 noon on Friday 13th July 2018.

### W2 Professorship in Theoretical Computer Science

Bremen, Germany

At Faculty 3 - Mathematics/Computer Science the following open position is available. The vacancy will be filled - conditional to the release of budgetary funds - as soon as possible:

Professorship
Salary Group W2
in the discipline
Theoretical Computer Science
Reference number: P559/18
as a civil servant, permanent position

The future professor will represent Theoretical Computer Science in research and teaching and should have an outstanding scientific qualification in a relevant area such as Algorithms and Complexity Automata Theory Finite Model Theory Algorithmic Graph Theory.

He/she will teach introductory lectures to undergraduate students as well as specialized courses to graduate students; teaching in the form of student projects is a welcome addition. Commitment and innovativeness in teaching are expected, and so is the willingness for didactical self-improvement and contribution to the internationalization of the University of Bremen.

It is further expected that the future professor contribute to science funding by acquiring third party funds. Cooperation with research institutions associated with the University of Bremen and contributions to the high-profile research area Minds, Media, Machines are highly welcome. Prerequisites for an appointment are a completed university degree in a field relevant to the position, a very good doctoral degree as well as further scientific achievements (equivalent to a habilitation postdoctoral thesis) which may have also been acquired outside of a university, teaching experience at a university, and pedagogical proficiency. Experience in considering the gender perspective in research and teaching is desirable. Non-German speaking candidates are expected to be able to teach in German within two to three years.

The recruitment is based on §18 BremHG.

As a winner of the Total-E-Quality Science Award, the University of Bremen strives to increase the number of female professors and therefore explicitly requests applications from female scientists. Applications from international scientists as well as applications of scientists with a migration background are explicitly welcome. Disabled candidates will be given preference in case of almost identical professional and personal qualifications.

Applications including a cover letter, CV, publication list, copies of degree certificates, should be submitted by July 31st, 2018 to:

Universität Bremen
Fachbereich 3 - Mathematik und Informatik
Fachbereichsverwaltung
Bibliothekstr. 5
28359 Bremen
or electronically in a single PDF file.

Comprehensive information on all aspects of the hiring process can be obtained here.

### PhD Position: Leveraging Automatic Deduction for Verification

Loria and Inria Nancy, France

Matryoshka is an ambitious research project that aims at developing efficient deduction techniques and integrating them in proof assistants. The project is funded by a European Research Council Starting Grant from March 2017 to February 2022. It is co-located between Vrije Universiteit Amsterdam (Jasmin Blanchette) in the Netherlands and Loria, Inria Nancy - Grand Est (Stephan Merz, Pascal Fontaine) in France.

Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. To make interactive verification more cost-effective, we propose to deliver powerful automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. To reach end users, these new provers will be integrated in proof assistants, including Coq, Isabelle/HOL, and the TLA+ Proof System. The subject of the position advertised here is this last aspect, i.e. integrating automatic deduction techniques in the TLA+ Proof System, the proof assistant for Lamport's Temporal Logic of Actions. To provide more automation for the non-temporal aspects of TLA+, which make up perhaps 90% or more of typical proofs, the PhD student will design efficient translations of set theory to higher-order logic. In order to filter the few useful lemmas out of the large TLA+ context, we suggest the design and use of a system of soft types.

We are looking for one outstanding candidate for a Ph.D. due to start before the end of 2018. Candidates should ideally have some experience with automatic or interactive theorem proving and be at ease with both theory and engineering. The student will work in a motivating environment in close collaboration with the Matryoshka and TLA teams. Please contact as soon as possible Jasmin Blanchette, Pascal Fontaine and Stephan Merz for more information.

To know more:

### Postdoc Position: Verification of Autonomous Robots

York, UK

Applications are invited for a Research Associate to carry out research on application of formal verification technology to safety assurance of autonomous robots. This position will be funded by the EPSRC for three years in the context of the recently awarded CyPhyAssure project.

You will assist in the development of a computerised platform for arguing the safety of autonomous robots by application of multi-model based assurance cases. We will build this platform within the Isabelle/HOL proof assistant, and utilise the Structured Assurance Case Metamodel (SACM). The platform, as conceived, will support formal modelling of individual modular components of a robot and its environment, the combination of these models to describe the overall system's behaviour, the description of formal requirements of the overall system, and decomposition and apportionment of these requirements to the constituent models.

You will liaise with academic and the industrial partners and participate in the writing of research papers. You will have a PhD in the area of formal methods, experience in modelling and formal refinement, and understanding of hybrid and/or probabilistic systems. You will have substantial experience in the application of the Isabelle/HOL theorem prover. Experience in the areas of assurance cases, safety processes, and robotics are all highly desirable.

## Other Calls

### Facebook Testing and Verification call for research proposals

Funding research into scalable testing and verification.

Facebook is pleased to invite university faculty to respond to a call for research proposals on Testing and Verification (TAV). This is Phase One of Facebook's funding initiative to support research in Testing and Verification.

We're particularly interested in:

• Automated fixes, from dynamic or static analyses
• Automated test case design
• Dealing with non-deterministic testing
• Incremental verification and testing techniques
• Reasoning about distributed and concurrent programs
and other areas described in the call.

## The Editor's Corner

Sophie Tourret

This is my first newsletter without Philipp as a co-editor. I wish to thank him for his collaboration till now and in the future as secretary of the AAR.

* * *

Now I would like to talk a little about one of the projects I am involved with.

During the last week of June, I attended the Matryoshka workshop. It was packed with interesting talks, mostly about first- and higher-order automatic and interactive theorem proving. One thing I found particularly interesting was the discussion session that concluded the workshop. At some point in this discussion, Martin Riener said something in the spirit of:

I would be very interested if someone could give a list of things that are difficult to do when going from first- to higher-order automated reasoning.
Alexander Steen (a PhD student working on the higher-order automated prover Leo III) immediately replied that he could and started doing so. The rest of the discussion was centered on this issue of when and where things get ugly in higher-order, what that means and how it has been overcome (or not) in different tools.

Among this list, two points particularly struck home:

• Higher-order term unifiability, because it is undecidable (see chapter 16 of the Handbook of Automated Reasoning) and, when it succeeds, can produce an infinite family of unifiers of which some could be useful to your ongoing proof (but which ones?); and
• Boolean variables, because among other things they can mess with the structure of your formulas (how do you stay in CNF when a variable can be instantiated with a conjuction?).
In the lifting of Superposition to higher-order that the Matryoshka team is working on, these points correspond to milestones. In the first step of this lifting, that will be presented at IJCAR (look for the talk by Alexander Bentkamp), the restrictions are such that these issues cannot happen. We are now working on reaching the first milestone by handling lambda-terms, in general and as unifiers in the calculus, while keeping Boolean variables as the last step to full higher-order.

In short, as someone that is stumbling upon these issues today, I look forward to this discussion turning into a paper that could be used as a guide, warning people about the pitfalls in the road to higher-order automated reasoning.