Association for Automated Reasoning

Newsletter No. 128
July 2019

From the AAR President, Larry Wos

As you read this column, you will be traveling a path in history -- a path that begins with M. Stone in 1936 with his monumental result about Boolean algebra, passes through a point in 2000 marked by the successful research of Robert Verofff and William McCune in their search for single axioms for the area of mathematics, takes you past an earlier column of mine (I believe published in 2014), and comes now to the present with some challenges for you. (Marshal Stone, with the Stone Representation Theorem, proved that every Boolean algebra is isomorphic to all closed and open subsets of a certain topological space.) What is common to these points in history is a focus on Boolean algebra -- one of the areas of mathematics that has been studied from widely different views. Boolean algebra can be explored in Terms of relations. That emphasizing union and intersection is more familiar, but here it is studied in terms of the Sheffer stroke.

The Sheffer stroke, denoted by the function f, of A and B is the logical nand of A and B, the not of the and of A and b. Veroff and his colleagues successfully showed that the following equation is a single axiom for Boolean algebra.

f(f(x,f(f(y,x),x)),f(y,f(z,x))) = y.  %  second candidate
                

The denial used, and that I suggest to be used in this column, is the following, where | denotes logical or.

f(f(a,a),f(a,a)) != a | f(a,f(b,f(b,b))) != f(a,a) |
f(f(f(b,b),a),f(f(c,c),a)) != f(f(a,f(b,c)),f(a,f(b,c))).
                

This denial corresponds to the negation of a 3-basis for Boolean algebra in terms of the Sheffer stroke.

Your first challenge is to prove that each of the following three equations is also a single axiom in addition to the equation just given.

f(f(f(x,y),z),f(f(x,f(x,z)),x)) = z.  %  candidate 1

f(f(f(x,y),z),f(x,f(f(x,z),x))) = z.  %  candidate 3

f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y.  %  candidate four
                

Yes, Veroff and McCune proved each of the three, candidates 1, 3, and 4, to be a single axiom. Of course, as is typical of my challenges, I recommend that you do not browse in the literature. I conjecture that many, or most, of you will rely on a Knuth-Bendix approach.

Your second challenge, which some may have already met, is to find for each of the three (1, 3, and 4) a forward proof that is free of demodulation, of course excluding the second of the four offered in an earlier column.

Possibly, the proofs of each of the three deducing the 3-basis, should you obtain them, may vary quite a bit in nature and length. If so, do you have a theory about why such differences occur, a theory based on one or more properties of each of the cited three?

But a far more difficult challenge, if my own research is a model, is the following. When asked to prove that some given equation or formula is a single axiom, in essence you are being asked to prove that the item is powerful enough that a proof can be found from it that derives some known basis. That proof might be one of contradiction; the proof you obtain may not actually derive the members of the basis. You must also prove that the item in focus is a theorem of the area under study, that it can be proved from some basis. Obtaining such a proof can be most difficult.

I have proofs for each of the cited four single axioms, proofs that each is a theorem, derived by using as an axiom set the cited 3-basis. I might not have found these proofs were it not for the substantial guidance provided by my colleague Veroff. So, for your third challenge, you are asked to prove that each of the four is in fact a theorem by starting with the 3-basis as the set of axioms.

The fourth challenge is to produce forward proofs, deriving the 3-basis, each free of the use of demodulation; in other words, you are asked not to rely on Knuth-Bendix.

Guest Column: Challenges in Higher-Order Theorem Proving

Alexander Steen
University of Luxembourg

In the Editor's Corner of AAR Newsletter No. 124, July 2018, Sophie Tourret reported on the Matryoshka workshop that focused on ongoing work in higher-order automated reasoning, its challenges and applications. Given my interest in this topic and my own experience in developing theorem proving software for Extensional Type Theory (ExTT), it is exciting for me to see increasingly many groups and projects working on various aspects of higher-order automation. In addition to the names that usually come to mind when talking about higher-order reasoning, that is e.g. TPS, Satallax, agsyHOL, and the Leo prover family, there is ongoing work on extending first-order provers such as Zipperposition, E and Vampire, and SMT solvers including CVC4, veriT to higher-order reasoning. Input-output standards for formulating higher-order problem statements and system results were included into the TPTP portfolio in 2008 (THF format), and there is ongoing work on a new version of the SMT-LIB standard and library which will address higher-order language features, too. In this column I highlight some of the challenges that I encountered when developing Leo-III, a higher-order theorem prover for ExTT, as part of my PhD studies.

There is a saying that laws are like sausages: It is better not to see them being made. In my opinion this also applies to higher-order automated theorem provers – at least to some extent. While, in contrast, it might be interesting to see how these provers are being made, there is still some truth to the point that not all of their ingredients are pleasing to the eye. This is because there are several complications to ExTT automation stemming from an intricate meta-theory. I will outline some of these complications in the context of practical system development in more detail below, each with a short description about how they are currently addressed within Leo-III. Leo-III is a refutational theorem prover that implements a higher-order paramodulation calculus. The input axioms and the negated conjecture (if any) are clausified and subsequently saturated until an empty clause is found. The proof search is organized as a sequential loop that is inspired by the given-clause algorithm implemented in Stephan Schulz' E prover.

Let's start with higher-order unification. It is generally known that the unification problem is undecidable for higher-order terms of ExTT. From a pragmatic perspective, this situation is unpleasant but not too bad; the usual question is when to stop searching for unifiers during proof search. What is done in most higher-order systems is that either a certain search depth D is fixed (the number of nodes taken in the branching search tree) for ensuring termination, or that full higher-order unification is replaced with a routine for the decidable pattern fragment. Both approaches sacrifice completeness in general, however it seems that often both ways work quite well in practice. In Leo-III, pattern unification is applied whenever possible. If the unification problem is outside of the pattern fragment, a fixed-depth search using a variant of higher-order unification is invoked. Evaluation results suggest that a depth of D = 8 is usually sufficient for higher-order problems from the TPTP library.

To my mind, the more difficult aspect of higher-order unification is that it is not unitary: There might be infinitely many most-general unifiers for a given pair of ExTT terms. The question is how to proceed searching in the branching unification search tree, and how many and which unifiers to take of those that are found within the search depth D. If too few are picked, the unsatisfiable set might not be refutable. If too many are picked, the search space is growing even more and we might also not find a refutation within reasonable resource limits. I do not know of any well-studied approach to select unifiers in a meaningful way. When multiple unifiers are found, Leo-III will currently pick at most N unifiers, at least one from every top-level branch of the search tree (if possible). By default, Leo-III takes at most N = 4 unifiers for any unification task during proof search. Lowering the number of maximal unifiers to N = 1 drastically lowers the number of solved problems in my experience, whereas a higher number does not change the outcome significantly.

The next point might cause acute abdominal pain to those unprepared: From the previous paragraph it is apparent that higher-order unification cannot in general be used as a meta-operation for filtering possible inferences; even if employed with a termination condition and sacrificing completeness. Instead, the individual unification transformation rules are interpreted as calculus rules in their own right and they may need to be applied even though the respective pair of terms is known to be non-unifiable. There are cases in which inferences need to be generated and inserted into the search space although the terms involved in the inference are evidently not unifiable. This is due to the intricate relationship between unifiability and equality modulo Boolean extensionality; as ExTT equality (=) and equivalence (<=>, if and only if) coincide for Boolean-typed terms. One can easily imagine the implications on the search space's size.

As an example, consider the three clauses p(a), p(b) and ~p(a & b), where a, b are formulas (atomic propositions) and p is a predicate on formulas. The set containing these clauses is unsatisfiable in ExTT. However, every inference between the first two and the last clause will be disregarded if the system restricts generating inferences to unifiable terms only. In contrast, resolving and applying the decomposition rule of Huet's unification procedure produces the new clauses a != (a & b) and b != (a & b) from which a refutation can be found (after applying further rules handling Boolean extensionality and clausification). Simply taking all type-correct inferences is infeasible in practice, so Leo-III uses heuristics to determine whether to disregard or keep an inference result, even if unification fails. This heuristic will keep inference results where at least one of the simplifying unification rules can be applied, or results that have Boolean-typed subterms. This behavior can be disabled if required, but it seems a passable trade-off at the current state.

I could now go on about issues involving primitive substitutions (blind guessing of top-level predicate variable instantiations), equality reasoning (lack of powerful redundancy methods, semantically definable equality predicates), re-clausification, lack of indexing techniques, etc, but let me stop here. The important aspect is that there are hardly any results available that guide the implementation of a higher-order theorem prover for ExTT. Leo-III tries to carefully balance between completeness and effectivity using various heuristics and trade-offs, and recent evaluations seem to confirm that this is indeed a fruitful approach. All of this is still merely a remedy for the symptoms of deeper and more fundamental problems, and I certainly hope that this is not the end of it.

What I learned from developing Leo-III is that efficiency as such is not of primary importance when it comes to ExTT reasoning. If the system does the wrong things very fast it will get you nowhere; but if it does the right thing slow, it will still produce results. There are, in my experience, usually only few genuine higher-order reasoning steps involved (the "Eureka-steps") in the whole process. So, if these steps are addressed appropriately, the remaining proof search can hopefully be done by faster and more efficient reasoning tools e.g. for first-order logic. Cooperation between higher-order and first-order systems is one of the underlying ideas of the Leo-III prover and the reason why Leo-III is intended to be used in combination with a first-order ATP system (such as E, iProver, Vampire, etc.) as a sub-system.

Honestly, I am not genuinely satisfied with the state of the art in automated higher-order reasoning and with Leo-III for that matter. There are quite a few aspects in Leo's source code that feel like trial-and-error, finger-crossing and magic. There is certainly need for more sophisticated proof calculi, practically oriented implementation techniques and well-grounded heuristics and I am excited to see what we will come up with in the next years and decades. If you have ideas on how to address the above sketched issues in Leo-III, I'd be happy to hear them!

Thanks to Jasmin Blanchette for proof-reading this column :-)

Announcement of the 2019 Herbrand Award

Christoph Weidenbach
President of CADE Inc.

The 2019 Herbrand Award for distinguished contributions to automated reasoning will be presented to

Nikolaj Bjørner and Leonardo de Moura

in recognition of their numerous and important contributions to SMT solving, including its theory, implementation, and application to a wide range of academic and industrial needs.

Call for Nominations: CADE Trustees Elections

Philipp Rümmer
Secretary of AAR and CADE

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

Nominations for four CADE trustee positions are being sought, in preparation for the elections to be held after CADE-27.

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

The terms of Jasmin Blanchette, Laura Kovács, Renate Schmidt, and Christoph Weidenbach end. All of them may be nominated for a second term.

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

In summary, we are seeking to elect four trustees.

Nominations can be made by any CADE member, either by e-mail or in person at the CADE business meeting at CADE-27 in Natal. 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 CADE members, i.e., they must have participated at any of the CADE or IJCAR conferences in the years 2016-2019. 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, Secretary of CADE Inc.

Vote for location of ITP 2021

John Harrison, John O'Leary, and Andrew Tolmach
ITP 2019 organizers

It is a long-standing custom of ITP (and TPHOLs) to vote on where the next installment of the conference should take place. It has already been decided that ITP 2020 will be incorporated into IJCAR 2020, the International Joint Conference on Automated Reasoning, to be held in Paris. However, we are already looking forward to 2021.

Anyone who is seriously considering attending ITP 2021 is entitled to vote. We received two bids, for Rome and London. Details of the bids can be viewed here where you will also find voting instructions. The deadline for voting is Friday, 2 August, 2019

Journal Special Issues

Journal of Logic and Computation: Special Issue on External and Internal Calculi for Non-Classical Logics, call for papers

This special issue intends to contribute to the current state-of-the-art of on analytic (external or internal) calculi for non-classical logics like intuitionistic, modal, epistemic logics, conditional logics, substructural, resouce logics, and other logical systems. Among some key points we can mention the relationships between internal} and external calculi for such logics and also their use for studying proof-search, automated deduction (proof-theory and implementation) and also logical properties like decidability, conservativity, axiomatisations and interpolation.

Topics of interests include but are not limited to the following:

All submitted papers under this call will be considered following the high-standard review process of the Journal of Logic and Computation. We expect submissions to present original contributions of the highest quality, that have not been previously published in, or submitted to, another journal.

All submissions should be send as a pdf-file to Didier Galmiche, by September 1, 2019.

If you have in mind to submit a paper to this special issue please send a message of intention to Didier Galmiche no later than July 31, 2019.

Springer Software Quality Journal: Special Issue on Improving Software Quality Through Program Analysis

Formal methods are paramount to ensure strong guarantees on the correct behavior of software. Based on mathematics and logic, formal methods help practitioners construct technology that can ensure increasingly important concerns such as safety, security, reliability and accountability.

This special issue of the Software Quality Journal is dedicated to program analysis techniques that can be used to improve the quality of software products. The special issue welcomes static and dynamic program analysis techniques, approaches based on theorem proving, model checking, and any other analysis technique that can help improving the quality of software systems.

Possible topics include, but are not limited to:

Requirements for Submission
Papers should be original and must not have been previously published or being currently under submission at any other venue. A paper extending a conference or workshop publication must contain at least 30% of new material to be considered for publication. In that case, a clear indication in the introduction is expected.

Manuscripts should be formatted according to the rules of the Software Quality Journal, available by following the "Instructions for Authors" link on the journal webpage, the CfP. To submit, please make sure to select "SI: Improving Software Quality Through Program Analysis". See here for frequently asked questions.

Important dates

More information is available on the special issue's CfP.

Conferences

CADE 2019: 27th International Conference on Automated Deduction, call for participation

23-30 August 2019, Natal, Brazil

The conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974, with this year's conference being the 27th CADE. Early CADEs were mostly biennial, and annual conferences started in 1996. The CADE conference series is managed by CADE Inc.

Important Dates:

For information about registration, see the conference website.

Woody Bledsoe Award, call for nominations

The Woody Bledsoe award honors outstanding contributions of students to automated reasoning and CADE. The winners are selected by quality of the contribution. We encourage all student authors for CADE-27 and affiliated workshops and events, to apply for the Woody Bledsoe Award, independently of a financial need. Please specify in your recommendation letter whether there is a financial need or not. The decision on the award will be done independently of a financial need.

A nomination consists of a recommendation letter of up to 300 words from the student’s advisor. The nomination should also contain full contact details for the students. Nominations for CADE-27 should be sent by e-mail to the program committee chair and conference chair. Please contact them as soon as possible, preferably before registering, and no later than July 15th. Full nominations can be sent until July 20th.

ITP 2019: the Tenth International Conference on Interactive Theorem Proving, call for participation

September 8-13, 2019, Portland, Oregon, USA

ITP is the premier international conference for researchers from all areas of interactive theorem proving and its applications.

More information is available on the conference's web page.

SVT 2020: 35th Annual ACM Symposium on Applied Computing Software Verification and Testing Track, call for papers

March 30 - April 3, 2020, Brno, Czech Republic

The ACM Symposium on Applied Computing (SAC) has gathered scientists from different areas of computing over the last thirty years. The forum represents an opportunity to interact with different communities sharing an interest in applied computing.

Software Verification and Testing Track
The Software Verification and Testing track aims at contributing to the challenge of improving the usability of formal methods in software engineering. The track covers areas such as formal methods for verification and testing, based on theorem proving, model checking, static analysis, and run-time verification. We invite authors to submit new results in formal verification and testing, as well as development of technologies to improve the usability of formal methods in software engineering. Also are welcome detailed descriptions of applications of mechanical verification to large scale software. Possible topics include, but are not limited to:

Important dates

More information is available on the conference's web page.

RAMiCS 2020: 18th International Conference on Relational and Algebraic Methods in Computer Science, call for papers

April 8-11, 2020, Palaiseau, France

Since 1994, the RAMiCS conference series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond.

We invite submissions in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to:

Important Dates:

More information is available on the conference web page.

CPP 2020 : The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, call for papers

January 20-21, 2020, New Orleans, Louisiana

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

CPP 2020 will be co-located with POPL 2020. CPP 2020 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.

Topics of Interest
We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interests to CPP:

Important Dates

More information is available on the conference's web site.

Workshops

F-IDE 2019: 5th Workshop on Formal Integrated Development Environments, call for papers

October 7, 2019 - Porto, Portugal

High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process.

List of Topics
The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. It welcomes the presentation of tools, methods, techniques and experiments. Topics of interest include, but are not limited to, the following:

Important Dates

More information is available on the workshop's web page.

RADICAL 2019: 2nd International Workshop on Recent Advancement in Concurrency and Logic, call for papers

August 26, 2019, Amsterdam, the Netherlands

Concurrency and Logics are two of the most active research areas in the theoretical computer science domain. The literature in these fields is extensive and provides a plethora of logics and models for reasoning about intelligent and distributed systems. More recently, the interplay of concurrency and logic with areas such as:

has received much attention, as witnessed by recent editions of AI conferences. All these examples share the challenge of developing novel theories and tools for automated reasoning that take into account the behaviour of concurrent and multi-agent entities.

The workshop aims to bring together researchers working on different aspects of logic and concurrency in AI, multi-agent systems, and computer science, both from a theoretical and a practical point of view. Besides, it aims to promote research on Foundation of AI in other research communities that are traditionally Theoretical Computer Science-oriented.

The topics covered by the workshop include, but are not limited to, the following:

IMPORTANT DATES

More information is available on the workshop's web page.

FTSCS 2019: 7th International Workshop on Formal Techniques for Safety-Critical Systems, call for papers

November, 9, 2019, Shenzhen, China

The aim of this workshop is to bring together researchers and engineers who are interested in the application of formal and semi-formal methods to improve the quality of safety-critical computer systems. FTSCS strives to promote research and development of formal methods and tools for industrial applications, and is particularly interested in industrial applications of formal methods.

Specific topics include, but are not limited to:

The workshop will provide a platform for discussions and the exchange of innovative ideas, so submissions on work in progress are encouraged.

Important dates:

More information is available on the workshop's web page.

SYCO-STRING 2019: 3rd Annual Workshop on String Diagrams in Computation, Logic, and Physics, call for papers

September 4-6, 2019, Birmingham, UK

The Symposium on Compositional Structures is a new interdisciplinary series of meetings aiming to support the growing community of researchers interested in the phenomenon of compositionality, from both applied and abstract perspectives, and in particular where category theory serves as a unifying common language. We welcome submissions from researchers across computer science, mathematics, physics, philosophy, and beyond, with the aim of fostering friendly discussion, disseminating new ideas, and spreading knowledge between fields. Submission is encouraged for both mature research and work in progress, and by both established academics and junior researchers, including students.

While no list of topics could be exhaustive, SYCO-STRING welcomes submissions with a compositional focus related to any of the following areas, in particular (but not necessarily) from the perspective of category theory:

Important dates
All deadlines are 23:59 anywhere-on-earth on the given dates.

More information is available on the workshop's web page.

2nd Workshop on Proof Theory and its Applications, call for papers

September 11-13, 2019, Swansea, UK

The mission of The Proof Society is to support the notion of proof in its broadest sense, through a series of suitable activities; to be therefore inclusive in reaching out to all scientific areas which consider proof as an object in their studies; to enable the community to shape its future by identifying, formulating and communicating it most important goals; to actively promote proof to increase its visibility and representation.

The 2nd Workshop on Proof Theory and its Applications, organised under the auspices of The Proof Society, will bring together researchers on proof theory and its applications. The aim of the meeting is to reflect on the mission of The Proof Society, through a series of invited and contributed talks, as well as a panel discussion.

Important dates

More information is available on the workshop's web page.

CiSS 2019: Circularity in Syntax & Semantics, call for papers

November 20-22, 2019, Gothenburg, Sweden

Circularity in Syntax & Semantics is dedicated to aspects of circularity and ill-foundedness in formal methods. The aim is to gather together researchers who study and/or utilise these phenomena from different perspectives such as provability, formal reasoning, construction, computation and complexity. As well as invited speakers there will be sessions for contributed talks.

Topics of interest include (but are not restricted to):

We are proud to announce that the 2019 Lindström Lectures will be held in connection with CiSS and delivered by Johan van Benthem. More information is available here.

Important Dates

More information is available on the conference's web page.

Open Positions

Open Positions in Tokyo: Formal Methods, Learning and Cyber-Physical Systems

Ichiro Hasuo

Dear colleagues,

For our research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for senior researchers and postdocs (10+ positions in total and some are still open), together with research assistants (PhD students) and internship students. The project runs until March 2022.

This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application esp. in automotive industry.

In order to deal with the complexity of real-world cyber-physical systems, we need to rely on empirical, learning-based and data-driven measures for quality assurance (such as search-based testing). At the same time, we are finding logical and automata-theoretic methods---the bedrock of formal verification and synthesis--playing pivotal roles also in those empirical quality assurance measures. This way, our project offers an exciting scientific environment that mixes formal methods, software engineering and machine learning. We also collaborate closely with Autonomoose, an automated driving project at Waterloo, Canada.

The following are prerequisites for application.

For more about the project, including our recent activities and output, please visit the project's web page.

About the open positions, this page has more information (esp. how to apply/inquire).

Postdoc position on quantified effects at Reykjavik University

Tarmo Uustalu

Quantified computational effects and interaction
Applications are invited for one postdoctoral position at the Department of Computer Science, Reykjavik University. The position is part of a three-year research project funded by the Icelandic Research Fund under the direction of Tarmo Uustalu. The overarching goal of to advance the theory and practice of disciplined effectful programming, based on graded monads, monad-like structures and interaction laws. Interested applicants should contact the PI for closer details on the research proposal.

The successful candidate will benefit from, and contribute to, the research environment at the Icelandic Centre of Excellence in Theoretical Computer Science (ICE-TCS), with research groups on concurrency, logic and semantics, algorithms, combinatorics. For information about ICE-TCS and its activities, see here. Moreover, she/he will cooperate with Shin-ya Katsumata and Maciej Piróg during the project work and will benefit from the interaction with their research groups at the National Institute of Informatics in Tokyo and the University of Wroclaw.

Qualification requirements
Applicants for the postdoctoral position should have, or be about to defend, a PhD degree in Computer Science or a closely related field. Previous knowledge of at least one of lambda calculus and functional programming, proof theory/type theory, programming language semantics, category theory in computer science, proof assistants is a prerequisite.

Remuneration
The wage will be approx 500 kISK per month before income tax, but depend on the qualifications and experience of the postdoc. Check here for what this means in terms of take-home pay. A tax relief for foreign experts may apply.

The position is for two years, to start in autumn 2019 (the start date is negotiable), and is renewable for another year, based on good performance and mutual satisfaction.

Application details
Interested applicants should send their CV, including a list of publications, to the PI, together with a statement outlining their suitability for the project and the names of at least two references.

Informal enquiries about the project and the conditions of work are very welcome.

We will review applications as they arrive. Please apply before 5 July 2019.

Postdoc position on Verification of Network Protocols at Aalborg University (Denmark)

We are looking for a highly motivated researcher with interest in formal methods and their application to verification of computer networks in order to join a project on "Quantitative Analysis and Synthesis of Network Protocols" funded by the Independent Research Fund, Denmark. The goal of this project is to significantly advance the state-of-the-art of automatic network analysis and synthesis, with a particular focus on accounting for the possibility of failures and supporting efficient what-if analysis, as well as for the quantitative consequences on quality-of-service.

Applicants are required to demonstrate strong background and understanding in formal methods and in particular model checking and show willingness to apply these methods to the domain of computer networks. An experience with quantitative systems and programming skills are an advantage. The postdoc is expected to perform independent research, collaborate with team members, and help with the supervision of PhD and MSc students as appropriate.

The project is led by prof. Jiri Srba (Aalborg University) in collaboration with prof. Stefan Schmid (Vienna University), prof. Kim G. Larsen (Aalborg University) and assoc. prof. Nate Foster (Cornell University). A part of the position will be sponsored by ERC advanced grant LASSO of Kim G. Larsen. The postdoc will have the possibility for a number of short term visits to Vienna University in order to strengthen the collaboration between Aalborg and Vienna.

For an idea of the research conducted within the project, you may have a look at:

The position is for the duration of 2 years with the option of limited teaching duties within the area. The postdoc must have obtained a PhD degree before the appointment day. The salary will be in accordance with the collective agreement for state-employed academics.

The deadline for the application is on August 2nd, 2019 with the employment starting (after agreement) shortly after. The applications must be submited electronically at this link.

For further information about the project, the conditions of the employment and life in Denmark contact prof. Jiri Srba.

Research Assistant / PhD Student / Post-Doc Position in Formal Methods for Software and Systems Engineering, Konstanz, Germany

Stefan Leue

The Chair for Software and Systems Engineering (Prof. Stefan Leue) of the University of Konstanz has the immediately opening of a definite term full-time Research Assistant / PhD Student / Post-Doc position available for up to three years, with the possibility of a finite extension. We are primarily looking for a PhD Student interested in working on formal methods for the design and analysis of complex systems. Areas of particular interest include, but are not limited to,

While preference will be given to candidates intending to pursue a PdD, applications from post-doctoral researchers with fitting interests will also be considered.

For more information and details on how to apply see here.

The salary is according to the payscale Entgeltgruppe 13 of the TV-L labor agreement (starting from appr. € 46.000 p.a.), which can be found here.

Application deadline: July 28, 2019.

Contact Stefan Leue directly if you have further questions.

PhD project on Verification of Efficient Algorithms at Manchester, UK

Peter Lammich

Funding for a PhD project on verification of efficient algorithms (in Isabelle/HOL) is available at the University of Manchester.

Short Description: This project aims at extending the current LLVM code generator for Isabelle/HOL, and developing new tools and techniques for the verification of efficient algorithms, down to their implementation in LLVM.

A long description and more information is available at the following link.

General information on doing a PhD at Manchester is available here.

Do not hesitate to contact Peter Lammich with additional questions!

Postdoctoral Opportunity at the University of Minnesota

Gopalan Nadathur

Applications are invited for a one-year postdoctoral position, possibly extendable into a second year, at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and reviews of applications will be conducted as they are received.

The project within which the appointment is to be made concerns the further development of a logic that incorporates a treatment of fixed-point definitions and the enhancement of the capabilities of the Abella proof assistant that is based on this logic. One particular extension to the underlying logic that is being investigated is the addition of predicate quantification. The research group is also interested in building into the Abella system the capability to reason about specifications written in linear logic and dependently typed lambda calculi, and in demonstrating the benefits of the system in tasks such as compiler verification.

To be suitable for the position, the candidate should be broadly conversant with the areas of computational logic and programming languages and should have the mathematical and programming skills necessary for conducting research in them. Prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and other similar logical systems would be needed for participating in the research at the appropriate level. For more details about the necessary background and possible topics of research within the project, please feel free to contact Gopalan Nadathur.

To view the official announcement for this position, please visit this URL. This link also provides details about how to apply and serves as the portal for applications. The application process will require you to submit a letter indicating your interest, a current CV, one or two of your papers broadly related to the topics of research and the names and contact details for two references who might be contacted as part of the application review process. Note that a prerequisite for employment is a doctoral degree in Computer Science or closely related field.

Postdoc positions on ERC project fun2model in 'strong' AI/verification at Oxford

An exciting opportunity has arisen at the intersection of AI and verification: three postdoctoral positions and two fully funded doctoral (DPhil) studentships are available under the supervision of Professor Marta Kwiatkowska on the ERC Advanced Grant project FUN2MODEL, to commence in October 2019 or as soon as possible thereafter.

The FUN2MODEL "From FUNction-based TO MOdel-based automated probabilistic reasoning for DEep Learning" project aims to make advances towards provably robust 'strong' Artificial Intelligence. In contrast to 'narrow' AI perception tasks realised by deep learning, which are limited to learning data associations, and sometimes referred to as function-based, 'strong' AI aims to match human intelligence and requires model-based reasoning about causality and 'what if' scenarios, incorporation of cognitive aspects such as beliefs and goals, and probabilistic reasoning frameworks that combine logic with statistical machine learning.

The objectives of FUN2MODEL are to develop novel probabilistic verification and synthesis techniques to guarantee safety, robustness and fairness for complex decisions based on machine learning, formulate a comprehensive, compositional game-based modelling framework for reasoning about systems of autonomous agents and their interactions, and evaluate the techniques on a variety of case studies.

The positions are briefly described below; please follow the links for information about the selection criteria and how to apply.

Senior Research Associate on FUN2MODEL, fixed term for 3 years from 1st October 2019, with the possibility of extension Grade 8: Salary £40,792 – £48,677 p.a. (note: post may be under-filled at grade 7: £32,236 - £39,609 p.a.)
The successful appointee will be expected to provide overall leadership for the development of probabilistic verification and synthesis methods, including software implementation and PRISM extensions, with emphasis on data-centric modelling, coordination and reasoning for autonomous multi-agent systems, capturing cognitive and affective aspects. This includes causal reasoning based on Bayesian networks; game-theoretic methods and algorithmic schemes for coordination and collaboration; formalisation of provably robust and beneficial collaboration; extensions of PRISM modelling language and software; and relevant case studies.

Research Associate post 1 on FUN2MODEL, fixed term for 3 years from 1st October 2019, with the possibility of extension Grade 7: Salary £32,236 - £39,609 p.a.
The successful appointee will be expected to contribute to the development of probabilistic verification and synthesis methods, with emphasis on developing automated probabilistic verification and synthesis methods for machine learning components. This includes Bayesian interpretation; provable probabilistic robustness guarantees for neural networks; provably correct synthesis for neural networks; complex correctness properties for machine learning decisions; software implementation; and relevant case studies.

Research Associate post 1 on FUN2MODEL, fixed term for 3 years from 1st October 2019, with the possibility of extension Grade 7: Salary £32,236 - £39,609 p.a.
The successful appointee will be expected to contribute to the development of probabilistic verification and synthesis methods, with emphasis on developing an algebraic theory of probabilistic components amenable to machine learning (ML). This includes study of interfaces and algebraic operations for ML components; contract-based probabilistic reasoning for ML components; reasoning about complex ML decisions; integration with autonomous multi-agent system models and reasoning tools; and relevant case studies.

The division of responsibilities between the three research posts may be adapted following interview depending on the qualifications and experience of the candidates.

2 x Doctoral (DPhil) Studentships on FUN2MODEL, 3.5 years from 1st October 2019, with the possibility of extension Stipend of at least £15600 per annum p.a, including fees at EU/home level, laptop and conference travel

For more information about the studentships, selection criteria and how to apply see here.

Studenship 1: Fairness and bias in multi-agent interactions
Fairness and bias of algorithmic decisions is critical to ensure their acceptance in society, but has been lacking in recently deployed AI software, for example Microsoft’s bot Tay. As a result, a variety of definitions of algorithmic fairness and corresponding verification approaches have been developed. However, these do not capture the influence of the cognitive and affective aspects of complex decisions made by autonomous agents, such as preferences and emotional state, which are essential to achieve effective collaboration of human and artificial agents. This project aims to develop a probabilistic, Bayesian framework based on causal inference for reasoning about fairness and bias in multi-agent collaborations, together with demonstrator case studies and associated software tools.

Studentship 2: Causal reasoning about accountability and blame
While deep learning is able to discern data associations, Bayesian networks are capable of reasoning about counterfactual and interventional scenarios, for example “What if the car had swerved when the child stepped on to the road?”. However, in order to model realistic human behaviours, Bayesian priors and inference must additionally account for cognitive goals and intentions, such as inference of intent for the pedestrian. This project aims to develop a framework for probabilistic causal reasoning with cognitive aspects to study accountability and blame in autonomous scenarios, together with demonstrator case studies and associated software tools.

The successful applicants will join an internationally leading research group of Professor Marta Kwiatkowska, who has an extensive track record in probabilistic verification and pioneering research on safety verification for neural networks and trust in human-robot collaborations. More information about Professor Kwiatkowska’s research and PRISM model checker can be found here, here, and here.

The closing date for all applications is 8 July 2019 (note different procedures for postdocs and studentships) . Interviews are expected to be held on 23-24th July 2019.

Enquiries to Professor Marta Kwiatkowska are welcome.

Our staff and students come from all over the world and we proudly promote a friendly and inclusive culture. Diversity is positively encouraged, through diversity groups and champions, see here for example, as well as a number of family-friendly policies, such as the right to apply for flexible working and support for staff returning from periods of extended absence, for example maternity leave.

A PhD position at Imperial College London

The Department of Computing at Imperial College London is a leading department of Computer Science among UK Universities, and has consistently been awarded the highest research and teaching (rated as "Excellent" in the previous national assessment of teaching quality).

We invite applications for a PhD studentship funded by VeTSS in programming languages and software engineering research related to concurrency theories and session types under the supervision of Professor Nobuko Yoshida and Dr Rumyana Neykova.

The primary objective of the PhD project is verification of distributed protocols using session types.

Session types (also called protocols) are a typing discipline to structure and verify message-passing communications. Session types (or behavioural types) have been applied to concurrent/distributed main stream languages, including Scala [PLDI'19], Go [POPL'19,ICSE'18,POP'17] and F# [CC'18].

Session types are also well-connected to several foundational areas such as automata theories/model-checking [CAV'19,POPL19b] and Game Semantics/Linear Logic [POPL19c,FoSSaCs'19].

See here for more details on session types and applications.

This research will centre on the hypothesis that: (1) multiparty session types, and their development approach, can be effectively extended to deal with data and control-flow constraints; and (2) the effectiveness of the approach (in a mainstream language) can be demonstrated via a concrete embedding of the theory. A successful candidate will develop the underlying theory and language implementation.

The PhD candidate will be part of the Mobility and Session Types Research Group (MRG). Informal inquiries about this position are also encouraged and can be directed to Nobuko Yoshida.

Applicants are expected to have a First Class or Distinction Masters level degree, or equivalent, in a relevant scientific or technical discipline, such as computer science. Applicants must be fluent in spoken and written English. The PhD studentship consists of an annual bursary up to a maximum of three and a half years. In addition, you will receive a desktop computer and conference allowance.

To apply for this position, you must have a strong background in at least one of the following areas:

The starting date is 1st October 2019

Applications must include the following:

please email your application to Nobuko Yoshida with the subject title "vetss phd scholarship on session types"

New permanent Researcher position in Formal Methods open at MERCE, Rennes, France

David Mentré

Mitsubishi Electric R&D Centre Europe (MERCE), is opening a new permanent Researcher position in Formal Methods located in Rennes, France.

MERCE is part of Mitsubishi Electric Corporate R&D and directly works for various research labs and business units of the group to fulfill their needs in formal methods or popularize the use of formal methods. We work from first research ideas to production-ready tools.

One core goal of our research is to acquire state-of-the-art in Formal Methods (on all the various kinds of formal methods) and adapt and enhance it to fulfill industrial needs of Mitsubishi Electric. We have many collaboration with academics through collaborative projects, PhD co-advising or direct collaborations. We work on real, industrial challenges.

Our research environment is obviously different from academic research but as we don't work directly for a business unit it is closer to academic research than business unit development. Rennes city is very nice to live in. Our research team is small and growing in a cheerful and open-minded work environment.

You'll find a more detailed announce with details on how to apply here in English, or in French.

2 PhD studentships, MSP group, University of Strathclyde, UK

Applications are invited for PhD study on any aspect of functional programming, type theory, logic, category theory, coalgebra etc. Candidates need not have a topic in mind, as we have plenty of ideas! The positions are expected to start on 1 October 2019, is fully funded for UK or EU students and will last for 3 years. The MSP group at the University of Strathclyde contains some marvellous researchers (if we do say so ourselves) and prides itself on its friendly and welcoming atmosphere. Members of the group are Dr Bob Atkey, Dr Ross Duncan, Dr Fredrik Forsberg, Professor Neil Ghani, Dr Clemens Kupke, and Dr Conor McBride.

Anyone interested should in the first instance contact Professor Neil Ghani and outline their academic background. Applications will be considered on a first come, first served basis.

PhD position ONERA/LIPN on formal methods and model checking, Palaiseau, France

ONERA and LIPN are cofunding a PhD position starting in the last trimester of 2019 on formal modelling of flight constraints. The PhD aims at exploring high-performance model-checking methods to verify continuous properties in an air traffic management system. It takes place within a collaboration between ONERA (R. Kervarc, A. Joulia), LIPN (C. Coti, C. Choppy, L. Petrucci) and LIP6 (F. Kordon). The PhD student will also have if desired the opportunity to participate in some of the international collaborations of these laboratories during the PhD. Applications must be made before the end of May.

The PhD is shortly described as follows:

In order to tackle the global increase in air traffic, a general tendency aims at allowing the Air Traffic Control (ATC) to focus on its regulation and overall supervision mission, and hence to use richer data exchanges to provide constraint to aircrafts and giving them flexibility within these constraints. These constraints must be both planified in advance for a given air space and adapted in real time to the situation (in order to avoid dangerous zones such as storms, to compensate for delays, etc.). The overall idea is that conflicts must be manageable locally in a distributed manner, while the ATC focuses solely on overall supervision. The planification must also be sufficiently robust to cope with delays and emergency situation. All this of course implies a large quantity of verifications that can only be performed through formal methods.

A particular difficulty in this context is that the properties to be verified are not only symbolic and discrete, but include physical and geometrical constraints: in addition to the more usual properties such as robustness or the proportionality between the rarity of a disturbing event and the number of aircracts involved in the subsequent deconfliction, some physical properties must be guaranteed, such as the flyability of trajectories, which means that it must always be possible to include a flyable trajectory within the constraints provided by ATC (e.g. an aircraft cannot stay still in air, cannot tack too tightly, cannot change height too abruptly, etc.).

Model-checking is a well-suited approach for the verification issues described above, but the inclusion of continuous properties that cannot easily be discretized (such as flyability) has a severe impact on computation performance. Various approaches have been developed to perform model-checking on a complex system with continuous properties. They generally consist in abstracting some details to limit the complexity of models and ease reasoning and verifications, and then in reintroducing these details by refinement operations that must follow some rules to preserve model semantics. The purpose of this PhD is to show that these methods allow verifying these properties in spite of the performance loss induced by the discretization of continuous properties asserted on a large number of objects, and to illustrate this on an ATC application provided by ONERA.

The full position offer (in French) is available here. Knowledge of French is not a requirement for the position, and the work can be performed in English.

PhD Scholarships in Computer Science at the Free University of Bozen-Bolzano (Italy)

19 PhD positions (15 four-year funded PhD grants and an additional 4 unfunded positions) are currently offered by the Faculty of Computer Science of the Free University of Bozen-Bolzano in Italy for its PhD programme. The Free University of Bozen-Bolzano was founded in 1997 as a multilingual (English, German, Italian) internationally oriented institution. The university is located in one of the most fascinating European regions, the Dolomites. This young university has already established itself as an important research institution, both in Italy and abroad. According to the Times Higher Education World University Rankings 2018, the university is the tenth world’s best small university and it is the second best young Italian University. According to the same ranking, the Faculty of Computer Science of the Free University of Bozen-Bolzano is the third best Italian computer science department, it is the best for international outlook Italian computer science department, and it is the best for citations Italian computer science department.

A public competition for in total 19 PhD positions at the Faculty of Computer Science is currently open, of which 15 positions will be fully covered by grants (17,000€ per year). In addition, students will have access to funding for attending summer schools and conferences. Additional financial support is given to spend a period of 6-12 months at an international research center. The language of the PhD program is English.

The deadline for applications is the 8th of July, 2019.

PhD candidates are strongly advised to look at the three areas (listed below) which are the focus of research at the Faculty of Computer Science, and to get in contact with their desired research area coordinators/supervisors before applying. The Selection Committee ranks PhD students based on a comparative assessment of the merits and qualifications of applicants, taking into account also feedback from potential supervisors in the selected research area.

Information and database systems engineering:

  1. Spatial And Temporal Databases
  2. Processing Data Streams And Time Series Data
  3. Approximation Techniques In Databases
  4. Query Optimization In Databases
  5. Data Mining And Machine Learning For Personalization
  6. Decision Support And Recommendation Systems
  7. Human-centered Computing
  8. Cooperative Interfaces For Information Access And Filtering
  9. Interaction Design
  10. Edge Computing Architectures And Platforms
  11. Image Processing And Computer Vision
  12. Mathematical And Scientific Computing

Knowledge representation and databases:

  1. Logic-based Languages For Knowledge Representation
  2. Intelligent Data Access And Integration
  3. Semantic Technologies
  4. Conceptual And Cognitive Modelling
  5. Data-aware Process Modelling, Verification, And Synthesis
  6. Business Process Monitoring, Mining, And Conformance
  7. Temporal Aspects Of Data And Knowledge
  8. Extending Database Technologies
  9. Visual And Verbal Paradigms For Information Exploration
  10. Reasoning With Uncertain And Imprecise Knowledge

Software and systems engineering:

  1. Empirical Software Engineering
  2. Mining Software Repositories
  3. Software Reliability And Testing
  4. Automatic Improvement And Empirical Investigation Of Software Quality Attributes
  5. Recommendation Systems In Software Engineering
  6. Software System Behavior
  7. Software Evolution And Maintenance
  8. Software Engineering Education
  9. Agile And Lean Processes
  10. Lean Startup And Software Startups
  11. Dependable IoT, Edge And Cloud Computing
  12. Software Architecture

Some positions are also offered in collaboration with external research and industry partners (FBK, SIAG). Please indicate in your application if you are interested in these collaboration topics.

For detailed information on the call and application procedures, please look here.

For further questions, contact the coordinator of the 2019/2020 PhD Programme, Prof. Claus Pahl.

PhD studentship in logic and systems verification at UCL, London, UK

We are looking to hire an exceptionally able and highly-motivated PhD student in the area of logic and verification to work in UCL's PPLV group. We are particularly keen to find someone who is interested in systems modelling and verification and their underlying logical theory:

The studentship is aligned with the IRIS project, --- which is focussed on understanding and reasoning about the compositional structure of systems models and the supporting idea of an interface --- and will be supervised by Professor David Pym and Dr. James Brotherston.

In more detail, area of the studentship is in logic and its application to program and systems verification, with a particular interest in the development and application of logical tools based on bunched logic, separation logic, and concurrent separation logic (and related ideas) and their use to reason about the correctness of interfaces between programs, systems, and organizations. The project may range from theoretical work in logic (semantics and proof theory) through the theory of system modelling tools to the design and implementation of modelling and verification tools.

The PPLV group conducts world-leading research in logical and algebraic methods and their applications to program and systems modelling and verification. The Interface Reasoning for Interacting Systems (IRIS) project, led by Prof. David Pym, uses logical and algebraic methods to understand the compositional structure of systems and their communications, seeking to develop analyses at all scales, from code through distributed systems to organizational structure, generically and uniformly.

The IRIS project, funded as a UK EPSRC Programme Grant, is a collaboration involving James Brotherston, Byron Cook, George Danezis, Peter O’Hearn, and David Pym at UCL, Alastair Donaldson at Imperial College, Will Venters at LSE, and Edmund Robinson at QMUL. Industry partners include Amazon AWS, BT, Facebook, HP Labs, GridPP, and Methods Group.

Candidates should normally have or be about to complete a Master's level qualification in mathematics or computer science, with a strong component in logic or theoretical computer science.

The student is available with an earliest start-date of October 2019. Candidates should be UK or EU nationals.

Interested candidates may contact David Pym or James Brotherston for more information.

To apply, please follow the instructions here.

Mathematical Verification Engineer, London area, UK

An applied research position is available at Imagination Technologies (Kings Langley, UK) in the domain of formal verification for arithmetic hardware.

Context:
The PowerVR graphics team produce the world's leading family of ultra-low power GPU IP cores. To create our next generation of ultra-high performing processors we need you to put your mathematical skills to the test and help us use cutting edge tools and techniques to prove mathematically that our components are bug free.

Job Description: Working in the Datapath team, a unique applied research team with a remit both to research and to deliver high performing hardware, you will be a vital part of the development of innovative mathematical components. You will contribute to projects ranging from geometric calculations for real-time mobile graphics, to heavily optimised hardware for neural network and AI applications. Depending on skills and interest, there may be opportunities to contribute to hardware design as well.

No prior knowledge of digital hardware is required. Full training will be provided on both industry tools and cutting edge techniques developed in-house, and you will be creating your own original ideas to push out the boundary of what can be achieved.

Link:
Please consult this web page for more details and to apply online.

Postdoc Position VirginiaTech: x86-64 binary verification, 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:

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.

CIFRE PhD thesis position at Siemens Mobility, Chatillon, France

Subject
Optimization of source code for safety-critical systems

Supervisors
Thesis supervisors:

Context
The research work on the thesis will take place at Siemens Mobility in Chatillon, France, a division providing the computer systems (hardware and software) for many on the World's automatic metros.

Being safety-critical, our computer systems are certified according to the norm EN 50126/50128/50129. To achieve the highest safety integrity level (SIL4), for some of our components, we use formal methods based on mathematical proof and programming languages technology. We are one of the pioneers of using such methods in industry, with our work on Paris's line 14.

The use of formal methods in large and real-life projects poses interesting challenges for the optimization of execution time of software derived using the formal methods.

Objectives
The goal of the thesis will be to develop ways to optimize the performance of software, while not sacrificing the guarantees of safety already provided for non-optimized code.

It is expected that the PhD candidate will implement the methods discovered, and that a certification according to the relevant safety norms be prepared for the implementation.

Necessarily going beyond the state-of-the-art, the candidate is expected to obtain an independent confirmation of the novelty of her/his results (in form of a scientific publication or patent) and write a PhD thesis that she/he will defend.

Qualifications
The PhD candidate should preferably have a previous training or a first research experience in 2 of the following 3 areas:

Employment Terms
The PhD researcher will be engaged under a 3-year work contract (French CDD) at Siemens Mobility in Chatillon.

The start of the PhD thesis and the work contract may be conditioned by the fulfillment of the Qualification and ZRR admission procedures of the doctoral school (Ecole Polytechnique, Palaiseau).

Admission Procedure
The application can be submitted at the Siemens Mobility web site, at this address. We encourage candidates to send their application ASAP.

Open position: Formal Verification Engineer (m/f/x) at HENSOLDT Cyber in Munich, Germany

HENSOLDT Cyber develops embedded IT products that meet the highest security requirements. It integrates an invulnerable operating system with security-hardened hardware to build the most secure product on the global IT market. The company combines more than 50 years of domain experience with world-class expertise in hardware- and software design to achieve global leadership.

Tasks

Skills

If you want to apply for an internship, feel free to contact us as well.

A young dynamic team is awaiting you. We offer a start-up atmosphere and benefits of a corporate company as well as flexible and mobile working. Apply directly or contact us.

PostDoc Research Fellowship for Females @ MPII/Germany: Lise Meitner Award Postdoctoral Fellowship

The Max Planck Institute for Informatics is looking for excellent female computer scientists, offering them PostDoc positions to develop their scientific ideas without exertion of influence. The PostDoc positions are funded by the Lise Meitner Award. It is a two-year tax-free postdoctoral research fellowship including business expenses. This grant is according to the fellowship rules of the Max Planck Society: it usually amounts to 3,000 Euro/month and is completed by compensation for business expenses of 10,000 Euro/year.

Fellows will be chosen based on the strength of their academic background and research credentials. Applications should include a CV, a cover letter, a publication list, a short research plan (one page is enough), and two references, that will be contacted later to provide recommendation letters.

The application process for 2019 ends on September 30th, 2019. See the Lise Meitner Award web page for details on how to apply.

For more information, please contact the Lise Meitner award commitee.

Postdoc position at National University of Singapore on Program Synthesis

Candidates are invited for a postdoc position, which is available in Ilya Sergey's group at Yale-NUS College and School of Computing of National University of Singapore. The position is for two years, funded by Singapore MOE Tier 1 grant "Scalable Deductive Synthesis of Thread-Safe Concurrency".

As the project name implies, we will be working on synthesising correct-by-construction concurrent programs. I am looking for motivated candidates with a strong, internationally competitive research track record. Particularly relevant is research expertise in:

A tentative starting date is 1 October 2019, but the appointment can start earlier if the position is filled. The successful candidate is expected to work with me and external collaborators (specifically, Prof. Nadia Polikarpova from UC San Diego), as well as to help advising students and interns on the project topic, but can also allocate some part of their time for the projects of their interest.

The NUS School of Computing is one of the world-leading departments in the areas of programming languages, software engineering, distributed systems, security and privacy. It provides a diverse and welcoming environment, and the researchers from different groups at SoC frequently collaborate on joint projects of mutual interest.

See the official advert here.

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

UNSW Sydney Seeking a Postdoc in Programming Languages and Verification

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

Sounds too good to exist?

In the Trustworthy Systems team at UNSW and 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 offering a two-year postdoctoral researcher position that would allow you to join us in Sydney, move things forward, and have a global impact.

Cogent is a language we designed that co-generates code and proofs in order to ease the verification of systems components around seL4. Potential topics include designing and implementing new domain-specific programming languages extending Cogent, writing formal specifications and proofs in Isabelle/HOL, developing formally verified infrastructure for building secure systems on top of seL4, contributing to improved proof automation and reasoning techniques, and applying formal proof to real-world systems and tools.

To apply you should have (or be about to obtain) a PhD degree in Computer Science, Mathematics, or similar.

You should also possess a significant subset of the following skills:

If you additionally have experience

you should definitely apply!

You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages.

Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements.

We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See here for more information.

For applying, use the following link.

This round of applications closes on the 13th of July 2019, 11:50pm AEST.

For any questions on this position, please contact Christine Rizkallah.

The seL4 code and proof, and the Cogent project, are open source. Check them out here and here.

More information about the Trustworthy Systems team here.

Still studying? We also have internship opportunities!

PhD Position in logic and formal verification, Barcelona, Spain

The University of Barcelona offers a PhD position in collaboration with the Catalan industrial sector. The industrial component of the PhD revolves around the development and verification of legal software in Coq within Formal Vindications SL. This work will be complemented with the formalization of parts of logic/mathematics. The group where this project will be embedded works on ordinal analysis via modal logic and reflection principles; we expect collaboration with the main group to arise, but we are open to alternative proposals. The PhD student will be part of a large and active research group. Currently, the group is lead by Joost J. Joosten and consists of three researchers who have over two years of experience with proof assistants, type-theory and pure and applied proof theory. There are three fellow PhD students working on related topics. Furthermore, the project counts with three junior scientific staff members, a senior Coq developer and a versatile programmer. The group is embedded into various research projects, including European, National and Regional funds. The general logic landscape of the Barcelona metropolitan area is rich and diverse and counts with groups and specialists in areas like algebraic logic, computability theory, formal linguistics, model theory, and set theory.

We offer a three-year position in the PhD program in Mathematics and Computer Science which is located in the very center of Barcelona. If after three years the PhD has not been finished, but there is realistic expectations that it will be finished soon, the company will consider continuing the position in its major characteristics. Apart from the usual PhD trajectory, the candidates will participate in cutting edge formalization developments in an industrial setting. The travel allowances can exceed 2200€ per year and the gross salary varies between 18K and 22K per year depending on how much financial support this project receives from the Catalan authorities.

We are looking for candidates with a background in theoretical computer science and/or mathematical logic. It is a strict requirement to have finished a relevant Master with an average undergraduate and master score of at least 6.5 out of 10. Apart from the required knowledge of Coq and Ocaml, other IT skills are recommended, especially knowledge/experience with other functional programming languages. Previous commercial work experience is a plus and working proficiency in English is a must.

Interested candidates should make their first statement of interest through the official AGAUR site, where they can fill in a pre-application. A direct link to it is here.

After a first selection, candidates will be asked to file their application package no later than September 5. The application package should contain:

Further information about the position can be obtained by writing an email to Aleix Solé.

The Editor's Corner

Sophie Tourret
Editor of the AAR Newsletter

Jean-Marie Hullot, a computer scientist with a substantial scientific and industrial career, including early contributions to automated reasoning, has passed away. His eulogy (in french), written by Gérard Berry et Gérard Huet, can be found here.