Association for Automated Reasoning

Newsletter No. 126
December 2018

From the AAR President, Larry Wos

I have been asked, sometimes by students, about how research can proceed. Indeed, if memory serves, I once had a course taught by Reinhold Baer on how research progresses.

In this column, I plan to give some insights of my own. Of course, research is risky, often resulting in no visible and useful product. But the journey can be exciting; it certainly has been many times for me. And, occasionally, gold is found: a new proof, a shorter proof, and, that jewel, an answer to an open question.

Two main types of research occur immediately: study of a new approach -- strategy, inference rule, representation, for example -- or study of an area of mathematics or logic that you have not studied before. Or you may simply wish to explain how research sometimes occurs, expounding on the source of new ideas.

Here, I shall offer an area of mathematics for research, an area whose answer is currently unknown, from what I have been told. I shall put forth some notions, in part based on my own years of study in automated reasoning, mathematics, and logic. (Of course, my goal is to inspire research that culminates in effective procedures that I can then use to find new proofs, shorter proofs, and new theorems.) I offer four illustrations leading respectively to the set of support strategy, the demodulation procedure, the inference rule of paramodulation, and the weighting strategy.

Those new to the field of automated reasoning may not be familiar with this part of history; others may just enjoy the retelling of true stories. The illustrations I offer are chosen because, individually and collectively , the discoveries featured have proved invaluable in the use of an automated reasoning program to successfully answer open questions from areas of mathematics and logic.

The year is 1963. The place is Argonne National Laboratory. The individual who provided the needed force is Dan Carson. The object is to find a proof of a simple theorem in group theory, namely, in groups of exponent 2, which asserts that the square of every element x is the identity e, commutativity can be proved. The obstacle is that too many conclusions are drawn and retained for the program to complete a proof. Carson, discouraged, says gloomily: the program runs out of memory. I ask for some time to think about a solution. Thirty-two minutes later Carson calls to say the game is up. I suggest that he try what would be called eventually the set of support strategy: For this theorem, have the program draw conclusions recursively from xx = e and the denial of commutativity, ab != ba; that is, prevent the program from applying binary resolution to pairs of clauses both of which are among the axioms for a group. Yes, a proof was found, and found quickly, and a strategy was formulated that has since become a mainstay of theorem proving. I also find it interesting that different users have different views about the content of the initial set of support. Some recommend including the negation of the goal that is sought, while others prefer a proof that is not bidirectional.

Aphorism: For a new program, new approach, or new strategy, choose a simple theorem that has resisted proof, and see whether, with the new idea, a proof is found. But be careful that your method is general.

The year is 1967. The place again is Argonne National Laboratory. The object this time is to find a proof of a trivial lemma that will in turn be used to prove that the square root of 2 is irrational. The obstacle is the retention of too many clauses before memory is exhausted. Yes, the situation sounds familiar, but the solution was not. The approach was to read some 2,000 clauses in the hope that some key property of the clauses would be discovered. Our first conjecture was that many of the 2,000 clauses were trivial, such as 0 + a + 0 = a for the constant a present in the denial. That conjecture was proved wrong: only about 39 of the 2,000 were trivial in the sense just illustrated. Our next conjecture was that if these clauses were not retained, their removal would result in a huge reduction in their offspring. Such indeed was the case. The solution was to add a list in the input that would "demodulate" such clauses to something that subsumption would take care of, something like 0 + x = x as a subsumer. In other words, canonicalize and simplify deduced conclusions with rules of the type just given or with rules such as associativity. All went well. Demodulation was thus formulated and, eventually, used for various other purposes including finding shorter proofs. I also use it for avoiding the use of various lemmas that are deemed undesirable. Yes, sometimes a logician or mathematician wishes to see whether a proof can be found that is simpler than already known, where simpler means avoiding various lemmas or avoiding certain types of term. What often varies from researcher to researcher is which demodulators to include.

Aphorism: Read the output of retained conclusions when an objective is not reached. Doing so can help you identify useless information.

The year is 1968. The place -- you guessed it -- is Argonne National Laboratory. The object is to address a need, posed by Alan Robinson in a paper for what was then called automated theorem proving, to cope with equality in a manner far better than how all relations were coped with; meaning was not used. In other words, treat equality as if it were understood. Perhaps because of the formulation of demodulation, the notion was to (in effect) generalize the basics of demodulation by permitting unification to go both ways -- to allow, when needed, unification in both an argument of equality and in the term in focus. Paramodulation was born; but, fortunately, George Robinson pointed out that nonunit clauses containing the key equality should be included, rather than merely focusing on unit equalities. Paramodulation has proved most useful. Robert Veroff states that virtually all of his research focusing on proof finding relies on paramodulation.

Aphorism: Accept challenges offered by people with a good track record.

The year is 1971. This time the place is Northern Illinois University. The object is to find a way to increase the efficiency of programs when seeking to find proofs. The approach, introduced by Ross Overbeek, was to circumscribe the terms considered essential for finding the sought-after proof and avoid clauses with (so-to-speak) undesirable terms. Weighting was born, and for many years it was used successfully to instruct a program about the relative desirability of various terms. My own view of weighting differs slightly in that I consider its main function to be advice-giving. By assigning low weights to various expressions, I cause the program to prefer conclusions containing corresponding subterms. Regardless of which view you take, however, weighting remains an important strategy for directing the program's reasoning.

Aphorism: Think hard, formulate a means that appears to meet the objective, and don't be afraid to experiment with or adapt an idea. The danger to avoid is having too limited a focus.

Now I close with the promised area for research, namely, lattice theory, featured in my last column. Where "v" denotes union or join and "^" denotes intersection or meet, William McCune found two 29-letter single axioms, the following.

(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (w v ((v6 v x) ^ (x v v7))) = x.
(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x.

The proposed research focuses on two open questions. (1) Does there exist a shorter single axiom for lattice theory in terms of meet and join? (2) In terms of meet and join, how long is the shortest single axiom for lattice theory? The (nonstandard) 4-basis McCune chose as target was the following.

y v (x^ (y^z)) = y
y^ (x v (y v z)) = y
((x^y) v (y^z)) v y = y
((x v y)^ (y v z))^y = y

The properties of associativity for union and intersection in the 6-basis that follows present obstacles that require, ordinarily, too much CPU time to overcome. Nevertheless, if you would enjoy research focusing on the 6-basis and, particularly, on the difficulties offered by associativity, I offer the following basis.

y ^ x = x ^ y
(x ^ y) ^ z = x ^ (y ^ z)
y v x = x v y
(x v y) v z = x v (y v z)
x ^ (x v y) = x
x v (x ^ y) = x

Attempting to answer an open question is obviously quite challenging, but that activity is so stimulating.

Results of the CADE Trustee Elections

Philipp Rümmer
Secretary of AAR and CADE

An election was held from October 12 to November 15 2018 to fill two positions on the board of trustees of CADE, Inc.

Four candidates were nominated (in alphabetic order): Christoph Benzmüller, Aart Middeldorp, Stephan Schulz, and Geoff Sutcliffe.

Following the decision at the IJCAR business meeting this year, participants of the last three CADE or IJCAR conferences were invited to vote, and a total of 270 ballots were sent by electronic mail on October 12. 57 valid ballots were returned, which translates to a participation rate of 21.1% (as compared to 9.1% in 2017, 11.2% in 2016, 11.0% in 2015, 10.0% in 2014, 11.8% in 2013, 13.0% in 2012, 16.2% in 2011).

The 2 candidates elected are Stephan Schulz and Christoph Benzmüller.

The counting of the votes according to the single transferable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.

After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:

On behalf of the AAR and CADE Inc., I thank Aart Middeldorp for his service on the board of trustees since 2015.

Stephan Schulz is joining the board as new elected member, but was also serving as ex-officio trustee for IJCAR 2018, so we would like to thank him for the continuing service on the board.

I would also like to thank Geoff Sutcliffe for running in the election, and for his invaluable help with the AAR and CADE web presence!

Congratulations to Christoph Benzmüller and Stephan Schulz on being (re)elected!

TABLEAUX Steering Committee Election - Call for Nominations

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

The Steering Committee of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") currently has three elected members whose terms will expire:

The Steering Committee is therefore calling for nominations of candidates who wish to contest an election for three positions, which will be held in December 2018.

To nominate please send an email to Jens Otten (jeotten@ifi.uio.no) containing:

Only members of the TABLEAUX community may act as nominators and a person may nominate or second only one candidate. Closing date for nominations is December 22nd 2018.

The TABLEAUX community consists of all people who have been registered participants in at least one of the three most recent TABLEAUX Conferences including IJCAR (i.e. IJCAR 2016, TABLEAUX 2017 and IJCAR 2018) and all members of the current IJCAR Program Committee.

The current Steering Committee rules and more information can be found on the TABLEAUX website.

Journal Special Issues

Special Issue of Mathematical Structures in Computer Science, open call for papers

in association with the workshops on Homotopy Type Theory and Univalent Foundations HoTT/UF 2017-2018

Homotopy Type Theory is a young research area combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory and higher category theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. These ideas have led to many interesting developments, from the study of syntax and semantics of type theories to practical formalizations in proof assistants based on univalent type theory.

The HoTT/UF workshops, co-located with FSCD since 2016, started out as a forum for formalization of mathematics in a univalent setting. From the 2017 edition and onwards, its scope has been broadened to

Special Issue
We are soliciting submissions for a Special Issue of the journal Mathematical Structures in Computer Science (Cambridge University Press) edited in association with the 2017 and 2018 editions of the HoTT/UF workshop. Submission is open to everyone and not limited to workshop participants. Topics encompass all aspects of Homotopy Type Theory and Univalent Foundations, in particular (but not exclusively):

Submission is open and contributions will be reviewed on a *rolling basis*, as soon as they are received. Accepted papers will be published on the MSCS website via 'FirstView' and will be citeable through a DOI shortly after acceptance - before the completion of the whole journal issue (expected end of 2019). Submission will be closed on December 31, 2018.

For details and submission instructions see the special issue web page.

JLAMP Special Issue on Relational and Algebraic Methods in Computer Science, Call for Papers

Relational and algebraic methods belong to the core of computer science. This special issue aims to showcase the variety and relevance of recent developments in this field ranging from theory to applications.

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

While we welcome substantially extended versions of papers published in the proceedings of the RAMiCS 2018 conference (Springer LNCS 11194), this call is open to anyone interested in the field of relational and algebraic methods.

Important Dates:

Information about the submission instructions and more details is available on the full call for papers.

Special issue on “Imprecise Probabilities, Logic and Rationality”, call for papers

The term “imprecise probability” (IP for short) usually refers to a family of models that provide a description of phenomena for which incomplete or imprecise information has been advanced, overcoming the limitations of traditional models of uncertainty based on precise probabilities. The basic idea of IP models is to extend the standard theory of precise probabilities by considering sets of traditional models. From this perspective the uncertainty (beliefs) of an agent about the possible states of the world is for instance modelled by sets of probabilities rather than a single one. Extensions include, among others, lower and upper previsions, belief functions, sets of desirable gambles and partial preference orderings.

IP is strongly linked with another framework where to express, study and reason on forms of imprecision and incompleteness: logic. Indeed, on the one hand standard logic methodologies have been applied to characterise and study IP notions such as coherence and models in terms of lower and upper probabilities/expectations. On the other hand concepts stemming from the IP tradition have been used to formulate appropriate semantics for statistical relational languages (e.g. by enabling to go beyond limitations such as cyclicity in probabilistic logic programs), whereas viewing IP as an abstract logic structure has lead to its application to domains such as for instance quantum mechanics, sum-of-square optimisation and classical logic itself.

This Special Issue intends to contribute to the state-of-the-art of the interactions and connections between imprecise probabilities and logic, and more generally with formal theories of rationality, the hope being that this cross-disciplinary view will lead to new exciting perspectives for both communities and related areas.

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

Submission Instructions
All submitted papers under this call will undergo the standard review process of the journal.

Submission Period
Mar 1st, 2019 - Jun 1st, 2019

All papers should be submitted to IJAR website by choosing the Special Issue “VSI:Imprecise probabilities, logic and rationality”.

All online submissions should follow the “Guide for Authors” of the journal.

Conferences

TASE 2019: The 13th International Symposium on Theoretical Aspects of Software Engineering, call for paper

July 29-31, Guilin, China

Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to the various aspects of software engineering, for instance, software dependability in trusted computing, interaction with physical components in cyber physical systems, distribution in cloud computing applications, security and privacy in general. Hence, new concepts and methodologies are required to enhance the development of software engineering from theoretical aspects. TASE 2019 aims to provide a forum for people from academia and industry to communicate their latest results on innovative advances in software engineering. The authors of a selected subset of accepted papers will be invited to submit extended versions of their papers to a special issue of the Science of Computer Programs journal.

Topics
The symposium is devoted to theoretical aspects of software engineering. Topics of interest include, but are not limited to:

Important Dates

For more information see the conference website.

FM 2019: 23rd International Symposium on Formal Methods - 3rd World Congress on Formal Methods, call for papers

October 7-11, 2019, Porto, Portugal

It is now more than 30 years since the first VDM symposium in 1987 brought together researchers with the common goal of creating methods to produce high quality software based on rigour and reason. Since then the diversity and complexity of computer technology has changed enormously and the formal methods community has stepped up to the challenges those changes brought by adapting, generalising and improving the models and analysis techniques that were the focus of that first symposium. The theme for FM 2019 is a reflection on how far the community has come and the lessons we can learn for understanding and developing the best software for future technologies.

Topics of Interest:<\ br> FM 2019 encourages submissions on formal methods in a wide range of domains including software, computer-based systems, systems-of-systems, cyber-physical systems, human-computer interaction, manufacturing, sustainability, energy, transport, smart cities, and healthcare. We particularly welcome papers on techniques, tools and experiences in interdisciplinary settings. We also welcome papers on experiences of formal methods in industry, and on the design and validation of formal methods tools. The broad topics of interest for FM 2019 include, but are not limited to:

Important Dates:

For more information see the conference website.

FSCD 2019: Fourth International Conference on Formal Structures for Computation and Deduction, call for papers

June 24-30, 2019, Dortmund, Germany

FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation (e.g. quantum computing, probabilistic computing, homotopy type theory), semantics and verification in new challenging areas (e.g. blockchain protocols or deep learning algorithms).

Suggested, but not exclusive, list of topics for submission are:

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

For more information see the conference website.

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

August 25-30, 2019, Natal, Brazil

CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including foundations, applications, implementations, theoretical results, practical experiences and user studies are solicited.

At every CADE conference the Program Committee selects one of the accepted papers to receive the CADE Best Paper Award. The award recognizes a paper that the Program Committee collegially evaluates as the best in terms of originality and significance, having substantial confidence in its correctness. Overall technical quality, completeness, scholarly accuracy, and readability are also considered. Characteristics associated with a best paper include, for instance, introduction of a strong new technique or approach, solution of a long-standing open problem, introduction and solution of an interesting and important new problem, highly innovative application of known ideas or existing techniques, and presentation of a new system of outstanding power. Under exceptional circumstances, the Program Committee may give two awards (ex aequo) or give no award.

Important Dates:

For more information, see the conference website.

CICM 2019: 12th Conference on Intelligent Computer Mathematics, call for papers

July 8-12, 2019, CIIRC, Prague, Czech Republic

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

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

Important Dates:

More information on the conference website.

SPIN 2019: 24th International Symposium on Model Checking of Software, call for papers

July 15-19, 2019, Beijing, China

The 26th edition of the SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation.

Topics of interest include, but are not limited to:

SPIN 2019 will be organized as an ACM SIGSOFT event, colocated with the International Symposium on Software Testing and Analysis (ISSTA 2019).

Important Dates:

More information on the conference website.

CALCO 2019: 8th International Conference on Algebra and Coalgebra in Computer Science, call for papers

June 3-6, 2019, London, UK

CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science.

Topics of Interest
Typical, but not exclusive topics of interest are:

Important Dates

More information (types of submissions, submission process...) available on the conference website.

FroCoS / TABLEAUX 2019, Joint Call for Workshops and Tutorials

September 2-6, 2019, London, UK

FroCoS (Symposium on Frontiers of Combining Systems) and TABLEAUX (Conference on Automated Reasoning with Analytic Tableaux and Related Methods) are two of the main conferences on the theory and application of logical systems. Their 2019 edition will be hosted by the Middlesex University in London, from 3 to 6 September 2019. In keeping with the tradition of the two events, we invite proposals for colocated workshops and tutorials on all topics related to logical reasoning: from theoretical aspects, to applications, to tools for interactive or automated reasoning. Workshops and tutorials can target the logical systems community in general, or alternatively focus on a particular system, recent theoretical development or application.

Colocated events will take place on 2 and 3 September 2019 (before the start of the conference programs) and will be held on the same premises as the main conferences. Workshop/tutorial-only attendees will enjoy a significantly reduced registration fee.

Detailed matters such as paper submission and review process, or publication of proceedings, are up to the organizers of individual events. All accepted workshops and tutorials will be expected to have their program ready by 10 August 2019.

Proposals for workshops and tutorials should contain at least the following pieces of information:

Proposals are invited to be submitted by email to chair@frocos2019.org and chair@tableaux2019.org, no later than 1 February 2019. Selected events will be notified by 9 February 2019. The workshop/tutorial selection committee consists of the FroCoS and TABLEAUX program chairs and the conference organizers.

FroCoS 2019: The 12th International Symposium on Frontiers of Combining Systems, Call for Papers

September 4-6, 2019, London, UK

FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. Starting in 2000, the conference proceedings have been published in Springer's LNCS/LNAI series. FroCoS 2019 will be co-located with the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019). The two conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions.

Scope of Conference
In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation, and automated reasoning, there is an obvious need for using specialized formalisms and inference systems for selected tasks. To be usable in practice, these specialized systems must be combined with each other and integrated into general purpose systems. This has led to the development of techniques and methods for the combination and integration of dedicated formal systems, as well as for their modularization and analysis. FroCoS traditionally focuses on these types of research questions and activities. Like its predecessors, FroCoS 2019 offers a forum for research in the general area of combination, modularization, and integration of systems, with emphasis on logic-based methods.

Topics of interest

Important Dates

For more information, please visit the conference website.

TABLEAUX 2019: The 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Call for Papers

September 3-5, 2019, London, UK

TABLEAUX is the main international conference at which research on all aspects — theoretical foundations, implementation techniques, systems development and applications — of the mechanization of tableaux-based reasoning and related methods is presented. TABLEAUX has been held every year since 1992. Starting in 1995, the proceedings have been published in Springer's LNCS/LNAI series. TABLEAUX 2019 will be co-located with the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). The two conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions

Scope of Conference
Tableau methods offer a convenient and flexible set of tools for automated reasoning in classical logic, extensions of classical logic, and non-classical logics. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis.

Topics of interest include but are not limited to:

We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community, and should focus on the role of reasoning and on logical aspects of the solution.

Important Dates

For more information, please visit the conference website.

ARITH-26: 26th IEEE Symposium on Computer Arithmetic, Call for Papers

June 10 – 12, 2019, Kyoto, Japan

Since 1969, the ARITH symposia have served as the flagship conference for presenting scientific work on the latest research in computer arithmetic. Computer arithmetic is now driving the most important innovations and product directions in our industry, such as artificial intelligence and security.

Authors are invited to submit papers describing recent advances on all aspects related to computer arithmetic, its applications or implementations. This includes, but is not restricted to, the following topics:

All submissions, whether regular full papers, short or industry papers, or PhD presentations, will have a full presentation slot scheduled.

Important dates

More information on the symposium website.

Workshops

HCVS 2019: 6th Workshop on Horn Clauses for Verification and Synthesis, call for paper

April 7, 2019 - Prague, Czech Republic

This workshop aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE), on the topic of Horn clause based analysis, verification and synthesis.

Horn clauses have been advocated by these communities at different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.

Aims and Scope
Topics of interest include but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:

We solicit regular papers describing theory and implementation of Horn-clause-based analysis and tool descriptions. We also solicit extended abstracts describing work-in-progress, as well as presentations covering previously published results that are of interest to the workshop.

CHC-COMP
HCVS 2019 will host the 2nd CHC competition (CHC-COMP), which will compare state-of-the-art tools for CHC solving for performance and effectiveness on a set of publicly available benchmarks. More information can be found here. All participants of CHC-COMP are invited (but not obliged) to submit a tool description for publishing either online or at the proceedings through the EasyChair system for HCVS (the HCVS deadlines apply).

Important dates

More information on the workshop website.

WoLLIC 2019: 26th Workshop on Logic, Language, Information and Computation, call of papers

July 2 - 5, 2019, Utrecht, The Netherlands

Just before and after the main WoLLIC 2019 event, Utrecht University will host two satellite workshops:

The workshop programs will be announced end of December 2018 via the WoLLIC 2019 website. Attendance of these satellite workshops is free, but registration is required.

Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:

Important Dates

For more information, see the workshop web page.

Winter Schools

VMCAI 2019: first VMCAI Winter School, call for participation

January 9-12, 2019, Lisboa, Portugal

The VMCAI school is meant to facilitate interaction, cross-fertilization, and advancement of hybrid methods that combine Verification, Model Checking, Abstract Interpretation, etc.

A detailed program is available at the school website.

Registration:
The registration deadline for the winter school is December 22, 2018. The registration is *free* but it is mandatory. Please take into consideration that the number of attendees is limited. Register as soon you are sure to be able to attend the Winter School.

More details are available at the school website.

Open Positions

Postdoc position: Symbolic tools for the formal verification of cryptographic protocols

A 12-month position for post-doctoral research on Symbolic tools for the formal verification of cryptographic protocols is available at the Inria Nancy / LORIA research center within the Inria project team PESTO: Proof techniques for security protocols as part of the ERC Grant SPOOC: Automated Security Proofs of Cryptographic Protocols.

Security protocols are distributed programs that aim at ensuring security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the Internet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness.

One generally distinguishes two families of security properties: trace properties and observational equivalence properties. Trace properties verify a predicate on a given trace and are typically used to express authentication properties. Observational equivalence expresses that an adversary cannot distinguish two situations and is used to model anonymity and strong confidentiality properties.

The Tamarin prover is a state-of-the art protocol verification tool which has recently been extended to verify equivalence properties in addition to trace properties. SAPIC allows protocols to be specified in a high-level protocol specification language, an extension of the applied pi-calculus, and uses the Tamarin prover as a backend by compiling the language into multi-set rewrite rules, the input format of Tamarin. Tamarin and SAPIC have been successfully used to verify standards such as TLS 1.3 and 5G AKA as well as industrial protocols such as OPC UA. The objective of this postdoc is to contribute to the development of the SAPIC/Tamarin toolchain, work on extensions and use the tool(s) to analyse particular classes of protocols.

Successful candidates must have defended a PhD in computer science, or expect to defend their PhD before taking up the position. Expected qualifications are:

Security knowledge is not required, but a plus.

Contacts:

The position is located at the Inria Nancy / LORIA research center in Nancy, France, with over 430 researchers, engineers and technicians. Nancy is a young (more than 45,000 students) city in eastern France with a rich cultural life and a high quality of life. It is famous for its UNESCO World Heritage Site "Place Stanislas". Paris is only 1h30 by TGV, Luxembourg, Germany and the Vosges mountains less than 1h30 by car.

Applications, including

should be sent to the the addresses indicated above as two pdf files (one for the publications, the other for the other documents).

Additionally, at least one recommendation letter from your PhD advisor(s), and up to two additional letters of recommendation should be sent directly by their authors to the email addresses indicated above.

Applications should be received by June 30, 2019, but applications received later may still be considered.

Informal enquiries concerning the position are welcome.

Assistant/associate professor positions at Aarhus University, Denmark

The Department of Computer Science at Aarhus University is looking for excellent and visionary tenure track Assistant Professors or Associate Professors to push the frontiers of Computer Science research. Aarhus University - an international top-100 University - has made an ambitious strategic investment in a 5-year recruitment plan to radically expand the Department of Computer Science.

Applicants within all areas of computer science are welcome, including Programming Languages, Software Engineering, Logic and Semantics.

The application deadline is January 6th 2019.

Additional details and instructions on how to apply are found here.

Tenure-Track / Tenured Faculty Positions at Drexel University, Philadelphia, PA, USA

The College of Computing and Informatics (CCI) at Drexel University is uniquely positioned to become a research and education leader for the 21st century. With a commitment to expand the college and grow the faculty in key areas of strength, CCI seeks candidates with intellectual curiosity, as well as, innovative knowledge to help drive cutting edge research, teaching and curriculum design.

CCI invites applications for multiple tenure-track and tenured faculty positions in Computer Science at all levels. Candidates should have a Ph.D. in Computer Science or related field at the time of appointment and a record of high-quality scholarly activities. Applicants for senior hires are expected to have demonstrated exceptional leadership in large-scale, multidisciplinary research programs. Preference will be given to applicants in the areas of Artificial Intelligence, Data Science, Machine Learning, and Privacy/Security.

Drexel is a private university committed to research with real-world applications. The university has over 25,000 students in 14 colleges and schools and offers about 200 degree programs. The College of Computing and Informatics has over 60 faculty, close to 2,000 students and 15 academic programs. Drexel has one of the largest and best known cooperative education programs in the country, with over 1600 co-op employers. Drexel is located on Philadelphia's "Avenue of Technology" in the University City District and at the hub of the academic, cultural, and historical resources of the nation's fifth largest metropolitan region.

Successful applicants will be expected to teach at the undergraduate and graduate levels, establish strong sponsored research programs, advise undergraduate and graduate students, and be involved in service to the college, the university, as well as the global academic community.

Application Instructions
Evaluation of applications will be conducted on a rolling basis; however, applicants should apply by January 15, 2019 for full consideration.

Applications should include a cover letter, CV, letters of reference, and brief statements describing the applicant's research program and teaching interests. Electronic submissions in PDF format are required.

Drexel University is an Equal Opportunity/Affirmative Action Employer. The College of Computing & Informatics is especially interested in qualified candidates who can contribute to the diversity and excellence of the academic community. Background investigations are required for all new hires as a condition of employment, after the job offer is made. Employment will be contingent upon the University's acceptance of the results of the background investigation.

Open Ph.D. and post-doc positions in formal verification of secured networks/ systems at ETH Zurich, Switzerland

The Chairs of Information Security and Programming Methodology at ETH Zurich are recruiting PhD students and post-docs for a project on formal verification of secure networked systems.

The Chairs of Information Security and Programming Methodology at ETH Zurich are recruiting PhD students and post-docs for a project on formal verification of secure networked systems. The project’s focus will be on verifying the protocols and implementation for a secure Future Internet architecture. Details are available online here and here.

Key requirements for successful applications:

Applications and questions should be sent to David Basin and Peter Müller. The application should include a CV, a description of research interests, a transcript of grades for Ph.D. student applicants, and optionally theses or publications. We will consider applications until the positions are filled. The start date is negotiable.

More details about the positions:

PostDoc positions at Inria Paris on F* and on Formally Secure Compilation

Catalin Hritcu

2 PostDoc positions are available in my group at Inria Paris on the F* and ERC SECOMP projects. I am seeking exceptional candidates with a strong, internationally competitive research track record.

On F*, I am looking for someone with research expertise in: programming language semantics, dependent types, type theory, effects, monads, mechanized metatheory, functional programming, formal verification. Here is a (non-exhaustive) list of potential research topics on which we could work.

On ERC SECOMP, I am particularly looking for someone with expertise in:

Here is a (non-exhaustive) list of potential research topics

Candidates are expected to work collaboratively on project-relevant topics and help advise students, but can also dedicate some of their time to their own independent projects. For exceptional candidates with enough experience we can also discuss about Starting Researcher positions, who can propose and follow their own research agenda and be fairly independent. Our team can also support such exceptional candidates for permanent Researcher positions funded and awarded competitively by Inria. Further details about these various positions are available here.

Do not hesitate to contact me if you are interested in joining the team!

ERC "RustBelt" project: Postdoc and PhD student positions available at MPI-SWS, Saarland, Germany

[Note: The initial deadline was October 31, but I will continue considering applications until the end of the year. If you are interested, please contact me directly first.]

I am pleased to announce the availability of multiple postdoc and PhD student positions in my research group at the Max Planck Institute for Software Systems (MPI-SWS), funded by a 2015 ERC Consolidator Grant for the project "RustBelt: Logical Foundations for the Future of Safe Systems Programming".

This 5-year project (which began in April 2016) concerns the development of rigorous formal foundations for the Rust programming language. The project summary appears at the bottom of this message.

Although the main high-level goal of the project is to build logical foundations for the Rust programming language -- see our POPL'18 paper -- the project also serves to fund technical work on two other major research efforts that feed into the main goal:

  1. The development of *Iris*, a simplifying and unifying framework for higher-order concurrent separation logic in Coq [POPL'15, ICFP'16, POPL'17, ESOP'17, ICFP'18, JFP'18]. See the Iris web page at http://iris-project.org/ for further details.
  2. Our ongoing study of improved semantics and logics for relaxed memory models (see e.g. our work on the separation logic GPS [OOPSLA'14, PLDI'15, ECOOP'17] and the "promising" semantics for solving the out-of-thin-air problem [POPL'17, ECOOP'17, ESOP'18]).

Postdocs:
I am seeking exceptional candidates with a strong, internationally competitive track record of research in programming languages and/or verification. The primary criterion is quality, but I am particularly interested in candidates who have specialized expertise in one or more of the following areas:

Experience programming in Rust is a welcome bonus, but not required.

Students:
I am seeking exceptional candidates who have at least some background in programming language theory and/or formal methods, and who are eager to work on deep foundational problems with the potential for direct impact on a real, actively developed language. A bachelor's or master's degree is required. For more details about the MPI-SWS graduate program, see here.

Applications will be considering until the end of the year. If you are interested in joining the RustBelt team and want to learn more about the project, please contact Derek Dreyer directly. To apply for a postdoc (or PhD student) position, please submit a CV (and/or grade transcript), research statement (or statement of purpose), and list of references here. If you are unable to apply by the deadline but are interested in a position, please contact Derek Dreyer anyway.

For further information, see the project web page.

Multiple Postdoc Positions @ Nanyang Technological University on verification

Multiple Postdoc Positions on Verification and Security Analysis for Hypervisor and Block Chain at Nanyang Technological University.

We have several exciting research projects on

  1. Hypervisor development, formal modelling and verification,
  2. Testing, verification and security analysis of block chain (Ethereum and beyond)

The postdoc will work in the Cyber-Security Laboratory at Nanyang Technological University using theorem proving technologies.

The position involves conducting basic research, developing tools, working as part of a large research team, travelling, and giving presentations. The working language is English.

Apart from specific requirement to the topic a general candidate requirement are:

The term is currently one to three years starting immediately. The salary is 5.5k to 7k SGD per month with up to 4 month performance bonus. (Singapore Tax is around 5%)

Interested applicants should send their CV to Dr. David Sanan.

Candidates must be experienced on one or more of the following areas:

Data61 Seeking Proof Engineers

We are are hiring again!

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

Sounds too good to exist?

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

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

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

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

If you additionally have experience

you should definitely apply!

If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. 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.

Salary ranges, in AUD (plus superannuation):

depending on experience and qualifications.

Apply online at the following link for the Proof Engineer positions:

Your application should include a cover letter, CV, undergraduate transcript (if applicable), and contact information for two references.

This round of applications closes on 17 December 2018.

For any questions on these positions, please contact Rafal Kolanski.

The seL4 code and proof are open source. Check them out.

More information about Data61's Trustworthy Systems team here.

There are additional proof engineering positions available on the Cogent project. Cogent is a language we designed to ease the verification of systems components around seL4. For expressions of interest, see contact details.

Looking to do a PhD? Data61 and UNSW offer scholarships! See here for details.

Data61 Seeking Research Scientist

We are looking for a full-time research scientist in formal verification to join us, the Trustworthy Systems group, at Data61, CSIRO. 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.

Our vision is a world in which computer users can choose all three: correct, secure, and fast. We believe that most current approaches to building systems are fundamentally flawed. We aim to demonstrate a better way. Our approach is rooted in foundational, formal verification using theorem provers (e.g., Isabelle, HOL4), and high-performance system design. If you find this vision appealing, and have ideas about how to pursue it, we want to hear from you.

Our team brings together a unique combination of expertise in systems, security, formal verification, and programming languages. We are the creators of seL4, the world's first operating system microkernel with a machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance and foundational binary-level correctness and security proofs. We are also involved in CakeML, the most realistic verified compiler for a functional programming language, and a promising approach to scaling full verification up to applications code.

We are building on these successes in various directions, including concurrency (formal reasoning and implementation), timing (real-time guarantees and timing channels), and whole-system verification using component systems (e.g., CAmKES) and code+proof co-generation.

We publish in top conferences, and are involved in multiple international research collaborations. You will have the opportunity to teach at UNSW should you wish to take it. We have a flexible, friendly, and intellectually stimulating work environment.

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.

The salary range for this position (plus superannuation) is

depending on experience and qualifications.

Apply online here.

Your application should include a cover letter, CV, short research statement, and contact information for two references.

This round of applications closes on 15 January 2019.

For any questions on this position, please contact June Andronic.

Job Opportunity at D-RisQ

Colin O'Halloran

I am looking to recruit someone who has experience of writing proof tactics in HOL and/or is experienced in using Z3 in order to accelerate D-RisQ’s product development of independent code verification. Proof tactic development would be done using ProofPower Z but we have expertise within D-RisQ to help a recruit familiar with one of the other HOL implementations work with ProofPower and Z.

Several PhD Positions on Verified Mathematics at VU Amsterdam, the Netherlands

Lean Forward is an ambitious research project that aims at formally proving theorems in research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles, by collaborating with number theorists. The project is funded by an NWO Vidi grant from January 2019 to December 2023 and is hosted by the Vrije Universiteit Amsterdam.

We will use Lean, an exciting new proof assistant developed at Microsoft Research (Leonardo de Moura) and Carnegie Mellon (Jeremy Avigad). Lean draws on decades of experience in interactive and automatic theorem provers, including Coq, Isabelle, and Z3. Its logic is very expressive, and emphasis is placed on strong proof automation. The system is easy to extend via metaprograms that rely on the same logical language that is used to express specifications and proofs.

As part of this project, we will develop formal libraries of fundamental number theory and explore how to automate proof search in these. Moreover, we will develop techniques and tools that help mathematicians perform accurate computations and reasoning using proof assistants, integrating procedures from computer algebra systems in a foundational, verified fashion. The ultimate aim is to develop a proof assistant that actually helps mathematicians by making them more productive and more confident in their results.

We are looking for outstanding candidates for several fully funded, four-year PhD positions, due to start in 2019 or early 2020. Candidates should ideally have some experience with (automatic or interactive) theorem proving or mathematics and be at ease with both theory and engineering. Please contact Jasmin Blanchette for more information.

10 PhD studentships in Nottingham

Applications are invited for up to ten fully-funded PhD studentships in the School of Computer Science at the University of Nottingham, starting on 1 October 2019.

The topics for the studentships are open, but should relate to one of the School’s research groups: Agents Lab; Automated Scheduling and Planning; Computer Vision Lab; Data Driven Algorithms, Systems and Design; Functional Programming Lab; Intelligent Modelling and Analysis; Uncertainty in Data and Decision Making; Mixed Reality Lab.

The studentships are for a minimum of three years and include a stipend of £14,777 per year and tuition fees. They are open to students of any nationality. Applicants are normally expected to have a first-class MSc or BSc in Computer Science or a related discipline, and must obtain the support of a supervisor in the School prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications. Informal enquiries may be addressed here.

To apply, please submit the following items by email to Christine Fletcher:

  1. a brief covering letter that describes your reasons for wishing to pursue a PhD, your proposed research area and topic, and the name of the potential supervisor whose support you have already secured;
  2. a copy of your CV, including your actual or expected degree classes, and results of all University examinations;
  3. an extended example of your technical writing, such as a project report or dissertation;
  4. contact details for two academic referees.

Closing date for applications: Friday 18 January 2019

Applicants in the area of the Functional Programming Laboratory are strongly encouraged! If you are interested in applying, please contact a potential supervisor at least two weeks prior to the 18th January deadline:

PhD Studentship: A Coalgebraic framework for reductive logic and proof-search

We are seeking to appoint a PhD student in UCL’s Programming Principles, Logic, and Verification (PPLV) group,to work alongside the EPSRC-funded project “A coalgebraic framework for reductive logic and proof-search (ReLiC)”.

The project is led by David Pym (PI), Alexandra Silva, and Simon Docherty (Co-Is). Facebook (Peter O’Hearn) is a partner in the project.

The position is available from 23 September 2019 for 4 years. The starting stipend will be approximately £17,280, with an approximate annual uplift of 3%.

We are looking for a talented, highly motivated student interested in working on some aspects of the project. Here is a description of the project.

The traditional treatment of logic is that of a deductive science: from axioms, conclusions are deduced according to formal proof rules. However, in practice many applications of logic and mathematical reasoning proceed in the opposite direction: from a putative conclusion, one finds sufficient axioms from which it may be concluded. This proceeds not by a step-by-step application of proof rules, but instead by the systematic reduction of the space of possible (deductive) proofs. We call this the reductive approach to logic. Archetypal examples of reductive reasoning in computer science include automated theorem proving, logic programming languages such as PROLOG, and precondition inference in program verification.

The ReLiC project aims to produce a uniform mathematical foundation for reductive logic via the framework of coalgebra and coinduction. Coalgebra can fruitfully be seen as a unifying formalism for stateful systems, while coinduction is a closely connected proof principle based on the reduction of goals into subgoals. In doing so we aim to

We are looking for a student with an excellent first degree in mathematics, computer science, philosophy, or another mathematical discipline, who has a strong background and interest in logic. Ideally, candidates will also have an excellent, relevant Master’s degree and strong programming skills.

For an informal discussion of the position, please contact David, Alexandra, or Simon.

To apply, please follow the instructions here and indicate clearly on your application that you are applying for this Scholarship ("A Coalgebraic framework for reductive logic and proof-search") under the scholarships section, or in your personal statement.

Postdoc positions in formal methods, U. Oslo

1-3 Postdoc positions in formal methods are available at the Department of Informatics, University of Oslo. The positions are for 3 years. Application deadline 13 January 2019.

The official announcement can be found here.

Please get in touch with Einar Broch Johnsen for more information.

Topics
The successful applicants are expected to contribute to ongoing research activities in the group, including:

  1. Integration of optimization and SMT-techniques with rich executable models
  2. Rewrite-based models and analysis of geological evolution and processes
  3. New techniques for actor-based modelling and analysis of distributed systems, e.g. resource restricted systems, IoT

The positions are funded by Sirius, a Centre for Research-Driven Innovation (SFI) at the University of Oslo. It constitutes a long-term interdisciplinary research initiative, funded by the Research Council of Norway, involving both academic research teams (UiO, NTNU and Oxford University) as well as industrial partners including operators (Equinor), service companies (Schlumberger and DNV GL) and IT companies (e.g., Computas, Evry, IBM).

The successful applicant should have an interest in working on real industrial problems in collaboration with industrial partners, as well as on basic research problems. The candidate will be expected to contribute to on-going activities in the group, such as:

Expected Background
The candidate should have expertise in one or more of the following areas:

The candidate should have implementation experience and programming skills in these fields. The candidate should have a strong publication record. Experience in research collaboration with industry, international mobility, and international collaborations is an advantage.

Competitive Salary and Environment

Research Assistant position at the University Koblenz-Landau, Germany

The Computer Science department of the University Koblenz-Landau (Campus Koblenz) invites applications for the position of a Research Assistant (wissenschaftlicher Mitarbeiter/Mitarbeiterin, 1,0 EGr. 13 TV-L) at PhD level, in the research groups Formal methods and theoretical computer science (Prof. Dr. Viorica Sofronie-Stokkermans) and Computer Networks (Prof. Dr. Hannes Frey).

The application deadline is January 31, 2019.

Additional details and instructions on how to apply can be found here.

Informal enquiries are welcome and may be sent to Viorica Sofronie-Stokkermans.

Counting of the Ballots of the CADE Trustee Elections

Philipp Rümmer
Secretary of AAR and CADE

An election was held to fill 2 positions. Christoph Benzmüller, Aart Middeldorp, Stephan Schulz, and Geoff Sutcliffe were nominated. 57 valid ballots were returned. Therefore, in each iteration of the single transferable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 29 first preference votes. Otherwise, the votes of the candidate with the least first preference votes are redistributed.

The following table reports the initial distribution of preferences among the candidates:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. no supp.
Christoph Benzmüller 17 11 15 12 2
Aart Middeldorp 17 8 9 21 2
Stephan Schulz 15 17 18 6 1
Geoff Sutcliffe 8 21 13 12 3
No candidate reaches at least 29 first preference votes.

By redistributing the votes of Geoff Sutcliffe, one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. no supp.
Christoph Benzmüller 19 17 19 2
Aart Middeldorp 19 13 23 2
Stephan Schulz 19 25 12 1
No candidate reaches at least 29 first preference votes.

By redistributing the votes of Aart Middeldorp, one gets the following table:

Candidate 1st pref. 2nd pref. no supp.
Christoph Benzmüller 26 29 2
Stephan Schulz 31 25 1
Now, Stephan Schulz reaches at least 29 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Stephan Schulz and get the following table:

Candidate 1st pref. 2nd pref. 3rd pref. no supp.
Christoph Benzmüller 20 22 13 2
Aart Middeldorp 21 10 24 2
Geoff Sutcliffe 16 24 14 3
No candidate reaches at least 29 first preference votes.

By redistributing the votes of Geoff Sutcliffe, one gets the following table:

Candidate 1st pref. 2nd pref. no supp.
Christoph Benzmüller 29 26 2
Aart Middeldorp 27 28 2
Now, Christoph Benzmüller reaches at least 29 first preference votes, and is elected.

To summarize, the 2 candidates elected are Stephan Schulz and Christoph Benzmüller.

The Editor's Corner

Sophie Tourret
Editor of the AAR Newsletter

A few days before I am done with editing an issue of the newsletter, I often receive an email that start with "I have heard that the next AAR newsletter will soon be published..." or something similar. It also happens that sometimes such an email comes a bit too late for me to include the information in the newsletter.

I realize that, since there is no fixed schedule, people that organize events such as conferences and can't anticipate if they have a chance to publish their CfP (or any other information) in the next AAR newsletter can easily be taken by surprise. To remedy that, I am considering creating a mailing list for people that want to know a few weeks in advance when the next newsletter will appear. If you would be interested in such a thing let me know. I'll see if it is worth creating such a list depending on the number of people interested.

* * *

A few days ago, I discovered this paper by Luca Aceto that talks about what it is that researchers in universities are doing.

I found this text on the mark, easy of access and also quite funny, which made me want to talk about it here. The end of the year festivities are an opportunity to catch up with people you don't see often. This year, I am definitely going to use this reference if the question of what I do at work comes up in the discussion!

* * *

Happy end of the year festivities and holidays to all AAR members