# Association for Automated Reasoning

March 2019

## From the AAR President, Larry Wos

I have derived much satisfaction and joy from finding new results in mathematics and logic. And I expect that many of you find equal delight in your research, whether looking for a new proof or even trying to duplicate a result in a particularly daunting area. Many of the challenges I have presented in this column in past AAR newsletters have fallen into both categories. Here I return to logic, specifically to an area called the BCSK logic and one of its extensions.

Matthew Spinks and Robert Veroff spent some time and research in that area before I was introduced to it by them. Two 3-literal clauses are needed, the following, which you will recognize as old friends if you have spent some time with condensed detachment.

```-P(i(x,y)) | -P(x) | P(y).                 % Modus
-P(j(x,y)) | -P(x) | P(y).                 % Modus
```
The function i denotes implication, and the function j denotes implication.

As noted, condensed detachment is in focus here. I shall offer several challenges in this area. The solutions may have been presented in the literature already, but my intention is twofold: to provide you the opportunity to do the research on your own and to, I hope, have you go beyond the known solutions and find new ways to attack the problems.

The following nine formulas in clause notation axiomatize the BCSK logic.

```P(i(x,i(y,x))).                           % (A1)
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).       % (A2)
P(i(i(i(x,y),x),x)).                      % (A3)
P(i(x,j(y,x))).                           % (A4)
P(i(j(x,j(y,z)),j(j(x,y),j(x,z)))).       % (A5)
P(i(j(x,j(y,z)),j(y,j(x,z)))).            % (A6)
P(i(j(j(x,y),x),x)).                      % (A7)
P(i(j(i(x,y),y),j(i(y,x),x))).            % (A8)
P(j(i(x,y),j(x,y))).                      % (A9)
```

Your first challenge is to prove each of the following theorems, called theses by various logicians. Each theorem is given in its negated form.

```-P(i(i(A,B),j(A,B))).
-P(j(i(A,B),i(j(B,C),j(A,C)))).
-P(j(i(B,C),i(j(A,B),j(A,C)))).
```

Your second challenge involves BCSK+, which is created by adding the following extension to BCSK:

```P(i(j(j(x,y),y),j(j(y,x),x))). %  (A10)
```
You are asked to prove in BCSK+ the following, given in negated form; but your proof should not use A6 as an axiom or as a deduced clause.
```-P(i(a1,i(j(a2,j(a3,a4)),j(a3,j(a2,a4))))).
```
You might find that various proofs in BCSK+ are longer than in BCSK. This may be unexpected in that BCSK+ has access to one additional axiom, which intuitively might suggest proofs that are found will be shorter. For more possible understanding, consider the case in which some lemma is proved on the way to finding the desired proof. That part of the larger proof might be moderately long. However, if the lemma is instead included as part of the s-called axiom set, then the sought-after proof will be clearly shorter.

One reason is that you might, if successful, invent or formulate a general approach to solve such problems. Another reason is that sometimes a logician or mathematician knows of a proof of a theorem but wishes to avoid the use of some lemma or lemmas and, possibly, avoid the use of some axiom and still find a proof of the theorem.

For your third challenge, you are asked to find a proof of the preceding, stated in its negated form; however, rather than in BCSK+, you are asked to obtain a proof in BCSK. In other words, A10 cannot be used as an axiom.

For your fourth challenge, you are asked to prove the following, in negated form, in BCSK+, and then in BCSK+ replace A10 with the positive form of the following and prove it from this new set of axioms.

```-P(i(j(A,B),i(A,B))).     %(A10a)
```

In other words, A10 and A10a are equivalent in the presence of A1 through A9. In addition, you are asked to find the proofs in both directions but without using A3, A6, and A7 as axioms.

I now come to the aspect that is to me most exciting. You are asked to find which, if any, of the nine axioms for BCSK are dependent. Then you are asked to find which of the ten axioms for BCSK+ are dependent. Similar investigations can lead to the discovery of theorems that are new to the field in focus. Or, you may find new axiom dependencies or discover that certain axioms previously believed to be needed to prove particular theorems are, in fact, not needed.

If you wish to wander deeper into research, you can try to determine which simple formulas (undefined) adjoined to BCSK+, all ten axioms, have the property that, from the larger set, you can prove the three axioms for Lukasiewicz, the following in negated form.

```-P(i(i(p,q),i(i(q,r),i(p,r)))).
-P(i(i(n(p),p),p)).
-P(i(p,i(n(p),q))).
```

If you begin with just the ten axioms, A1 through A10, can you prove any of the three Lukasiewicz axioms just given? If you return to BCSK, removing A10, can you prove any of the Lukasiewicz axioms?

Experiments of this type might encourage you to formulate new strategies or to incorporate into the program you use new parameters to choose from.

To close this column, I now offer a formidable challenge.

Thanks to John Halleck, a single axiom can be studied, the following.

```P(i(xp,i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(j(xq,j(xr,xq)), xs),xs),i(j(j(xt,j(u,v)),j(j(xt,u),j(xt,v))),w)),w),
i(j(j(j(x,y),x),x),z)),z),i(j(xp1,i(xq1,xp1)),xr1)),xr1),i(j(i(xs1,i(xt1, u1)), i(i(xs1,xt1),i(xs1,u1))),v1)),v1),
i(j(i(w1,i(x1,y1)),i(x1,i(w1,y1))),z1)) z1),i(j(i(i(xp2,xq2),xp2),xp2),xr2)),xr2),i(i(j(xs2,xt2),i(xs2,xt2)),
u2)),u2),i(j(i(j(v2,w2),w2),i(j(w2,v2),v2)),x2)),x2),i(j(i(i(y2,z2), z2),i(i(z2,y2),y2)),xp3)),xp3),i(i(xq3,
i(xr3,i(xs3,xr3))),xt3)),xt3))).
```

The challenge, in two parts, first asks you to prove from this formula the ten axioms A1 through A10 for BCSK+.

The second half asks for a proof that the cited single axiom is a theorem, provable from the ten axioms of BCSK+. The length of the given single axiom may indeed prove to be a substantial obstacle, for either of the two parts of the challenge. And, as a bit of a puzzle to solve, of the two given 3-literal clauses for implication, only one is needed to meet the various challenges.

## Herbrand Award: Call for Nominations

Philipp Rümmer
Secretary of AAR and CADE Inc.
On behalf of the CADE Inc. Board of Trustees

The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

• Larry Wos (1992)
• Woody Bledsoe (1994)
• Alan Robinson (1996)
• Wu Wen-Tsun (1997)
• Gerard Huet (1998)
• Robert S. Boyer and J Strother Moore (1999)
• William W. McCune (2000)
• Donald W. Loveland (2001)
• Mark E. Stickel (2002)
• Peter B. Andrews (2003)
• Harald Ganzinger (2004)
• Martin Davis (2005)
• Wolfgang Bibel (2006)
• Alan Bundy (2007)
• Edmund Clarke (2008)
• Deepak Kapur (2009)
• David Plaisted (2010)
• Nachum Dershowitz (2011)
• Melvin Fitting (2012)
• Greg Nelson (2013)
• Robert L. Constable (2014)
• Andrei Voronkov (2015)
• Zohar Manna and Richard Waldinger (2016)
• Lawrence C. Paulson (2017)
• Bruno Buchberger (2018)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE-27 is

13 May 2019
Nominations pending from previous years must be resubmitted in order to be considered.

Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to

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

## Ackermann Award 2019 - The EACSL Outstanding Dissertation Award for Logic in Computer Science, call for nominations

Nominations are now invited for the 2019 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1.1.2017 and 31.12.2018 are eligible for nomination for the award. The deadline for submission is 1 April 2019. Submission details follow below.

Nominations can be submitted from 1 January 2019 and should be sent to the chair of the Jury, Thomas Schwentick.

The Award
The 2019 Ackermann award will be presented to the recipient(s) at CSL 2020, the annual conference of the EACSL, 13-16 January 2020, in Barcelona.

The award consists of

• a certificate,
• an invitation to present the thesis at the CSL conference,
• the publication of the laudatio in the CSL proceedings, and
• financial support to attend the conference.
The jury is entitled to give the award to more (or less) than one dissertation in a year.

Jury
The jury consists of:

• Christel Baier (TU Dresden);
• Michael Benedikt (Oxford University);
• Mikolaj Bojanczyk (University of Warsaw);
• Jean Goubault-Larrecq (ENS Paris-Saclay);
• Dexter Kozen (Cornell University);
• Dale Miller (INRIA and Ecole Polytechnique), ACM SigLog representative;
• Simona Ronchi Della Rocca (University of Torino), the vice-president of EACSL;
• Thomas Schwentick (TU Dortmund) , the president of EACSL.

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

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

The submission should be sent by e-mail as attachments to the chairman of the jury, Thomas Schwentick.

With the following subject line and text:

• Subject: Ackermann Award 2019 Submission
• Text: Name of candidate, list of attachments

Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text.

## CPP as a Venue for AR Research

Jasmin Christian Blanchette
Cătălin Hriţcu
Co-chairs of CPP 2020

The CPP (Certified Programs and Proofs) conference series, initiated in 2011, targets any research promoting formal development of certified software and proofs. We would like to bring this conference to the attention of AR researchers.

CPP is often perceived as a close relative of the ITP (Interactive Theorem Proving) conference, but as explained in its manifesto, it has a substantially broader scope, including

• the development of certified or certifying programs
• the development of certified mathematical theories
• the development of new languages and tools for certified programming
• new program logics, type systems, and semantics for certified code
• new automated or interactive tools and provers for certification

CPP welcomes any research promoting formal development of certified software and proofs. Beyond papers that have a mechanized implementation, it also welcomes papers that present new foundational theory, semantic models, program logics, and type systems even if they have only pen-and-paper proofs.

Historically, CPP has received few submissions from the AR community (beyond its ITP subcommunity), but these have usually been well received. The authors of the following accepted papers, from the last five years, can attest to this:

• Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller:
A Proof-Theoretic Approach to Certifying Skolemization.
CPP 2019: 78–90
• Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Proofs in Conflict-Driven Theory Combination.
CPP 2018: 186–200
• Jan Jakubuv, Josef Urban:
BliStrTune: Hierarchical Invention of Theorem Proving Strategies.
CPP 2017: 43–52
• Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov:
The Vampire and the FOOL.
CPP 2016: 37–48
• Thomas Sternagel, Sarah Winkler, Harald Zankl:
Recording Completion for Certificates in Equational Reasoning.
CPP 2015: 41–47

Why not join them? The next edition of CPP will be held in New Orleans, USA, on 20 and 21 January 2020. It will be co-located with the POPL (Principles of Programming Languages) conference. See the forthcoming call for paper for details. We hope you will consider submitting your best AR-related work at CPP.

## Conferences

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

October 7-11, 2019, Porto, Portugal

Topics of Interest
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:

• Interdisciplinary formal methods: Techniques, tools and experiences demonstrating the use of formal methods in interdisciplinary settings.
• Formal methods in practice: Industrial applications of formal methods, experience with formal methods in industry, tool usage reports, experiments with challenge problems. The authors are encouraged to explain how formal methods overcame problems, led to improved designs, or provided new insights.
• Tools for formal methods: Advances in automated verification, model checking, and testing with formal methods, tools integration, environments for formal methods, and experimental validation of tools. The authors are encouraged to demonstrate empirically that the new tool or environment advances the state of the art.
• Formal methods in software and systems engineering: Development processes with formal methods, usage guidelines for formal methods, and method integration. The authors are encouraged to evaluate process innovations with respect to qualitative or quantitative improvements. Empirical studies and evaluations are also solicited.
• Theoretical foundations of formal methods: All aspects of theory related to specification, verification, refinement, and static and dynamic analysis. The authors are encouraged to explain how their results contribute to the solution of practical problems with formal methods or tools.

Important Dates

• Abstract submission: 28 March, 2019
• Full paper submission: 11 April, 2019, 23:59 AoE
• Camera ready: 9 July, 2019
• Conference: 7-11 October, 2019

### TAP 2019: 13th International Conference on Tests And Proofs

October 9-11, 2019, Porto, Portugal

The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.

The TAP conference aims to promote research in the intersection of testing and proving by bringing together researchers and practitioners from both areas of verification.

Topics of Interest
TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Its topics of interest center around the connection between proofs (and other static techniques) and testing (and other dynamic techniques). Papers are solicited on, but not limited to, the following topics:

• Verification and analysis techniques combining proofs and tests
• Program proving with the aid of testing techniques
• Deductive techniques supporting the automated generation of test vectors and oracles (theorem proving, model checking, symbolic execution, SAT/SMT solving, constraint logic programming, etc.)
• Deductive techniques supporting novel definitions of coverage criteria,
• Program analysis techniques combining static and dynamic analysis
• Specification inference by deductive and dynamic methods
• Testing and runtime analysis of formal specifications
• Search-based technics for proving and testing
• Verification of verification tools and environments
• Applications of test and proof techniques in new domains, such as security, configuration management, learning
• Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, …)
• Case studies, tool and framework descriptions, and experience reports about combining tests and proofs

Important Dates

• Abstract: March 28, 2019
• Paper: April 11, 2019
• Camera-Ready Version: July 9, 2019
• Conference: October 9-11, 2019

### ITP 2019: Tenth International Conference on Interactive Theorem Proving, call for paper

September 9-12, 2019, Portland, Oregon, USA

The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics. This will be the 10th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988.

Paper Submission
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include, but are not limited to, the following:

• formal aspects of hardware and software
• formalizations of mathematics
• improvements in theorem prover technology
• integration with automated provers and other symbolic tools
• user interfaces for interactive theorem provers
• formalizations of computational models
• verification of security algorithms
• use of theorem provers in education
• industrial applications of interactive theorem provers
• concise and elegant worked examples of formalizations (proof pearls)

Important Dates

• Paper submission deadline: March 31, 2019
• Author notification: May 31, 2019
• Camera-ready copy due: July 1, 2019
• Conference: September 9-12, 2019

### MFPS XXXV: Thirty-fifth Conference on the Mathematical Foundations of Programming Semantics, call for paper

June 4-7, 2019, London, UK

MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.

Topics include, but are not limited to, the following:

• bio-computation;
• concurrent qualitative and quantitative distributed systems;
• process calculi;
• probabilistic systems;
• constructive mathematics;
• domain theory and categorical models;
• formal languages;
• formal methods;
• game semantics;
• lambda calculus;
• programming-language theory;
• quantum computation;
• security;
• topological models;
• logic;
• type systems;
• type theory.
We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example.

Important Dates

• April 1, 2019: Abstract Submission
• April 4, 2019: Paper Submission
• May 24, 2019: Final Papers Deadline

### MFPS XXXV: Thirty-fifth Conference on the Mathematical Foundations of Programming Semantics, call for paper

June 4-7, 2019, London, UK

MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.

Topics include, but are not limited to, the following:

• bio-computation;
• concurrent qualitative and quantitative distributed systems;
• process calculi;
• probabilistic systems;
• constructive mathematics;
• domain theory and categorical models;
• formal languages;
• formal methods;
• game semantics;
• lambda calculus;
• programming-language theory;
• quantum computation;
• security;
• topological models;
• logic;
• type systems;
• type theory.
We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example.

Important Dates

• April 1, 2019: Abstract Submission
• April 4, 2019: Paper Submission
• May 24, 2019: Final Papers Deadline

### QPL 2019: 16th International Conference on Quantum Physics and Logic, call for papers

June 10-14, 2019, Orange, California, USA

The conference brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behaviour in general. Work that applies structures and methods inspired by quantum theory to other fields (including computer science) is also welcome.

Important Dates

• April 1: abstract submission
• April 7: paper submission
• April 30: application for student support
• May 12: notification of authors
• May 17: early registration deadline
• May 24: final papers ready
• June 10-14: conference

### TbiLLC 2019: the Thirteenth International Tbilisi Symposium on Logic, Language and Computation, call for papers

September 16-20, 2019, Batumi, Georgia

The Programme Committee invites submissions for contributions on all aspects of logic, language, and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:

• Natural language syntax, semantics, and pragmatics
• Linguistic typology and semantic universals
• Language evolution and learnability
• Historical linguistics, history of logic
• Natural logic, inference and entailment in natural language
• Logic, games, and formal pragmatics
• Logics for artificial intelligence and computer science
• Constructive, modal and algebraic logic
• Categorical logic
• Algorithmic game theory
• Computational social choice
• Formal models of multiagent systems
• Information retrieval, query answer systems
• Distributional and probabilistic models of information, meaning and computation
• Models of computation

Important Dates

• Submission deadline: 1 April 2019
• Final abstracts due: 1 July 2019
• Registration deadline: 1 August 2019
• Symposium: 16-20 September 2019

Programme and submission details can be found here.

### MFPS XXXV: Thirty-fifth Conference on the Mathematical Foundations of Programming Semantics, call for paper

June 4-7, 2019, London, UK

MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.

Topics include, but are not limited to, the following:

• bio-computation;
• concurrent qualitative and quantitative distributed systems;
• process calculi;
• probabilistic systems;
• constructive mathematics;
• domain theory and categorical models;
• formal languages;
• formal methods;
• game semantics;
• lambda calculus;
• programming-language theory;
• quantum computation;
• security;
• topological models;
• logic;
• type systems;
• type theory.
We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example.

Important Dates

• April 1, 2019: Abstract Submission
• April 4, 2019: Paper Submission
• May 24, 2019: Final Papers Deadline

### 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. CALCO 2019 is co-located with MFPS XXXV.

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

• Abstract models and logics
• Automata and languages
• Categorical semantics
• Graph transformation
• Modal logics
• Proof systems
• Relational systems
• Term rewriting
• Algebraic and coalgebraic semantics
• Abstract data types
• Inductive and coinductive methods
• Re-engineering techniques (program transformation)
• Semantics of conceptual modelling methods and techniques
• Semantics of programming languages
• Corecursion in programming languages
• Corecursion in logic/constraint/functional/answer set programming
• Corecursive type inference
• Coinductive methods for proving program properties
• Implementing corecursion
• Applications
• Role of algebraic and coalgebraic methods in software and systems engineering
• Development processes with algebraic and coalgebraic methods
• Method integration
• Usage guidelines
• Specialised models and calculi
• Hybrid, probabilistic, and timed systems
• Models and calculi of concurrent, distributed, mobile, cyber-physical, and context-aware computing
• Systems theory and computational models (chemical,biological,etc.)
• String diagrams and network theory
• Combinatorial approaches
• Theory of PROPs and operads
• Rewriting problems and higher-dimensional approaches
• Automated reasoning with string diagrams
• Applications of string diagrams
• Connections with control theory, engineering, and concurrency
• System specification and verification
• Algebraic and coalgebraic specification
• Formal testing and quality assurance
• Generative programming and model-driven development
• Integration of formal specification techniques
• Model-driven development
• Process algebra
• Specification languages, methods, and environments
• Validation and verification
• Tools supporting algebraic and coalgebraic methods for
• Model checking
• Theorem proving
• Testing
• Quantum computing with algebra and coalgebra
• Categorical semantics for quantum computing
• Quantum calculi and programming languages
• Foundational structures for quantum computing
• Applications of quantum algebra

Important Dates

• Abstract submission: April 3, 2019
• Paper submission: April 8, 2019
• Author notification: May 13, 2019
• Final version due: May 27, 2019

### 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:

• Formal verification techniques for automated analysis of software
• Formal analysis for modeling languages, such as UML/state charts
• Formal specification languages, temporal logic, design-by-contract
• Model checking
• Automated theorem proving, including SAT and SMT
• Verifying compilers
• Abstraction and symbolic execution techniques
• Static analysis and abstract interpretation
• Combination of verification techniques
• Modular and compositional verification techniques
• Verification of timed and probabilistic systems
• Automated testing using advanced analysis techniques
• Combination of static and dynamic analyses
• Derivation of specifications, test cases, or other useful material via formal analysis
• Case studies of interesting systems or with interesting results
• Engineering and implementation of software verification and analysis tools
• Benchmark and comparative studies for formal verification and analysis tools
• Formal methods education and training
• Insightful surveys or historical accounts on topics of relevance to the symposium

Important Dates
Please keep in mind the following dates for submission:

• Paper Submission: April 5th, 2019 (23:59:59 Anywhere on Earth)
• Author Notification: April 27th, 2019
• Symposium: July 15-19, 2019

### CONCUR 2019 The 30th International Conference on Concurrency Theory, call for papers

August 27-30, 2019, Amsterdam, The Netherlands

The purpose of the CONCUR conferences is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications.

Topics
Submissions are solicited in semantics, logics, verification and analysis of concurrent systems. The principal topics include (but are not limited to):

• Basic models of concurrency such as abstract machines, domain-theoretic models, game-theoretic models, process algebras, graph transformation systems, Petri nets, hybrid systems, mobile and collaborative systems, probabilistic systems, real-time systems, biology-inspired systems, and synchronous systems;
• Logics for concurrency such as modal logics, probabilistic and stochastic logics, temporal logics, and resource logics;
• Verification and analysis techniques for concurrent systems such as abstract interpretation, atomicity checking, model checking, race detection, pre-order and equivalence checking, run-time verification, state-space exploration, static analysis, synthesis, testing, theorem proving, type systems, and security analysis;
• Distributed algorithms and data structures: design, analysis, complexity, correctness, fault tolerance, reliability, availability, consistency, self-organization, self-stabilization, protocols;
• Theoretical foundations of architectures, execution environments, and software development for concurrent systems such as geo-replicated systems, communication networks, multiprocessor and multi-core architectures, shared and transactional memory, resource management and awareness, compilers and tools for concurrent programming, programming models such as component-based, object- and service-oriented.

Important Dates
All dates are AoE.

• Abstract submission: April 15, 2019
• Paper submission: April 22, 2019
• Camera ready copy: July 3, 2019
• Conference: August 27-30, 2019

### SAS 2019: 26th Static Analysis Symposium, call for papers

October 8-11, 2019, Porto, Portugal

Static analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area.

Topics
The technical program for SAS 2019 will consist of invited lectures and presentations of refereed papers. Contributions are welcomed on all aspects of static analysis, including, but not limited to:

• Abstract domains
• Abstract interpretation
• Automated deduction
• Data flow analysis
• Debugging
• Deductive methods
• Emerging applications
• Model checking
• Program optimizations and transformations
• Program synthesis
• Program verification
• Security analysis
• Tool environments and architectures
• Theoretical frameworks
• Type checking

Important Dates

• Paper Submission: Thursday, April 18, 2019
• Artifact Submission: Thursday, April 25, 2019
• Author Response: Friday-Monday, May 31-June 3, 2019
• Notification: Friday, June 14, 2019
• Conference: Wednesday-Friday, October 9-11, 2019

### FMICS 2019: the 24th International Conference on Formal Methods for Industrial Critical Systems

August 30-31, 2019, Amsterdam, The Netherlands

The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.

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

• Case studies and experience reports on industrial applications of formal methods, focusing on lessons learned or identification of new research directions.
• Methods, techniques and tools to support automated analysis, certification, debugging, descriptions, learning, optimisation and transformation of complex, distributed, real-time, embedded, mobile and autonomous systems.
• Verification and validation methods (model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, etc.) that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues).
• Impact of the adoption of formal methods on the development process and associated costs. Application of formal methods in standardisation and industrial forums.

Important Dates

• Abstract submission: 19 April 2019
• Paper submission: 26 April 2019
• Camera ready: 19 June 2019
• Conference: 30-31 August 2019

### TABLEAUX 2019: the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, second 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:

• tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, substructural, relevance, non-monotonic logics) and their proof-theoretic foundations
• related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation-based methods, etc.)
• sequent calculi and natural deduction calculi for classical and non-classical logics, as tools for proof search and proof representation
• flexible, easily extendable, light-weight methods for theorem proving
• novel types of calculi for theorem proving and verification in classical and non-classical logics
• systems, tools, implementations, empirical evaluations and applications (provers, proof assistants, logical frameworks, model checkers, etc.)
• implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, etc.)
• extensions of tableau procedures with conflict-driven learning
• techniques for proof generation and compact (or humanly readable) proof representation
• theoretical and practical aspects of decision procedures
• applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching

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

• Abstract submission: 21 Apr 2019
• Paper submission: 24 Apr 2019
• Notification of paper decisions: 6 Jun 2019
• Camera-ready papers due: 1 Jul 2019
• TABLEAUX conference: 3-5 Sep 2019

### FroCoS 2019: The 12th International Symposium on Frontiers of Combining Systems, second 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

• combinations of logics (such as higher-order, first-order, temporal, modal, description or other non-classical logics)
• combination and integration methods in SAT and SMT solving
• combination of decision procedures, satisfiability procedures, constraint solving techniques, or logical frameworks
• combination of logics with probability and/or fuzzy measures
• combinations and modularity in ontologies
• integration of equational and other theories into deductive systems
• hybrid methods for deduction, resolution and constraint propagation
• hybrid systems in knowledge representation and natural language semantics
• combined logics for distributed and multi-agent systems
• logical aspects of combining and modularizing programs and specifications
• integration of data structures into constraint logic programming and deduction
• combinations and modularity in term rewriting
• methods and techniques for the verification and analysis of information systems
• methods and techniques for combining logical reasoning with machine learning

Important Dates

• Abstract submission: 21 Apr 2019
• Paper submission: 24 Apr 2019
• Notification of paper decisions: 6 Jun 2019
• Camera-ready papers due: 1 Jul 2019
• FroCoS conference: 4-6 Sep 2019

### PPDP 2019: 21st International Symposium on Principles and Practice of Declarative Programming, call for papers

October 7–9, 2019, Porto, Portugal

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

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

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

Important Dates

• Title and abstract registration 26 April 2019 (AoE)
• Paper submission 3 May 2019 (AoE)
• Rebuttal period (48 hours) 3 June 2019 (AoE)
• Author notification 14 June 2019
• Final paper version 15 July 2019
• Conference 7–9 October 2019

### MPC 2019: 13th International Conference on Mathematics of Program Construction, call for papers

October 7-9, 2019, Porto, Portugal

The International Conference on Mathematics of Program Construction (MPC) aims to promote the development of mathematical principles and techniques that are demonstrably practical and effective in the process of constructing computer programs.

Scope:
MPC seeks original papers on mathematical methods and tools put to use in program construction. Topics of interest range from algorithmics to support for program construction in programming languages and systems. Typical areas include type systems, program analysis and transformation, programming language semantics, security, and program logics. The notion of a 'program' is interpreted broadly, ranging from algorithms to hardware.

Theoretical contributions are welcome, provided that their relevance to program construction is clear. Reports on applications are welcome, provided that their mathematical basis is evident. We also encourage the submission of 'programming pearls' that present elegant and instructive examples of the mathematics of program construction.

Timeline:

• Abstract submission 26th April 2019
• Paper submission 3rd May 2019
• Author notification 14th June 2019
• Camera ready copy 12th July 2019
• Conference 7-9 October 2019

### SEFM 2019: 17th International Conference on Software Engineering and Formal Methods, call for papers

September 16-20, 2019, Oslo, Norway

SEFM aims to bring together leading researchers and practitioners from academia, industry, and government, to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools.

Topics of interest include, but are not limited to, the following aspects of software engineering and formal methods:

• Software Development Methods
• Formal modeling, specification, and design
• Software evolution, maintenance, re-engineering, and reuse
• Design Principles
• Programming languages
• Domain-specific languages
• Type theory
• Abstraction and refinement
• Software Testing, Validation, and Verification
• Model checking, theorem proving, and decision procedures
• Testing and runtime verification
• Statistical and probabilistic analysis
• Synthesis
• Performance estimation and analysis of other non-functional properties
• Other light-weight and scalable formal methods
• Security and Safety
• Security, privacy, and trust
• Safety-critical, fault-tolerant, and secure systems
• Software certification
• Applications and Technology Transfer
• Service-oriented and cloud computing systems, Internet of Things
• Component, object, multi-agent and self-adaptive systems
• Real-time, hybrid, and cyber-physical systems
• Intelligent systems and machine learning
• HCI, interactive systems, and human error analysis
• Education
• Case studies, best practices, and experience reports

Important Dates

• Abstract submission deadline: May 3, 2019 (AoE)
• Paper submission deadline: May 10, 2019 (AoE)
• Conference: September 16-20, 2019

### ICTAC 2019: 16th International Colloquium on Theoretical Aspects of Computing, call for papers

October 30 - November 4, 2019, Hammamet, Tunisia

The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing. ICTAC also aims to promote research cooperation between developing and industrial countries. The proceedings will be published as a volume of Springer's LNCS series.

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

• Languages and automata
• Semantics of programming languages
• Logic in computer science
• Lambda calculus, type theory and category theory
• Domain-specific languages
• Theories of concurrency and mobility
• Theories of distributed, grid and cloud computing
• Models of objects and components
• Coordination models
• Models of software architectures
• Autonomous systems
• Timed, hybrid, embedded and cyber-physical systems
• Static analysis
• Software verification
• Software testing
• Program generation and transformation
• Model checking and automated theorem proving
• Interactive theorem proving
• Verified software, formalized programming theory

The important dates are:

• Abstracts 5 May 2019
• Papers 12 May 2019
• Final version 11 August 2019
• Conference 30 October to 4 November 2019

### FMCAD 2019: International Conference on Formal Methods in Computer-Aided Design

October 22 - 25, 2019, San Jose, California, USA

FMCAD 2019 is the nineteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.

Topics of Interest
FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer-aided design. Topics of interest include (but are not limited to):

• Model checking, theorem proving, equivalence checking, abstraction and reduction, compositional methods, decision procedures at the bit- and word-level, probabilistic methods, combinations of deductive methods and decision procedures.
• Synthesis and compilation for computer system descriptions, modeling, specification, and implementation languages, formal semantics of languages and their subsets, model-based design, design derivation and transformation, correct-by-construction methods.
• Application of formal and semi-formal methods to functional and non-functional specification and validation of hardware and software, including timing and power modeling, verification of computing systems on all levels of abstraction, system-level design and verification for embedded systems, cyber-physical systems, automotive systems and other safety-critical systems, hardware-software co-design and verification, and transaction-level verification.
• Experience with the application of formal and semi-formal methods to industrial-scale designs; tools that represent formal verification enablement, new features, or a substantial improvement in the automation of formal methods.
• Application of formal methods to verifying safety, connectivity and security properties of networks, distributed systems, smart contracts, blockchains, and IoT devices.

Important Dates

• Abstract Submission: May 10, 2019
• Paper Submission: May 17, 2019
• Author Response Period: June 17-21, 2019
• Author Notification: July 3, 2019
• Camera-Ready Version: Aug 16, 2019
All deadlines are 11:59 pm AoE (Anywhere on Earth)

### CSL 2020: Computer Science Logic, call for papers

January 13-16, 2020, Barcelona, Spain

Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.

List of topics:

• automated deduction and interactive theorem proving,
• constructive mathematics and type theory,
• equational logic and term rewriting,
• automata and games,
• game semantics,
• modal and temporal logic,
• model checking,
• decision procedures,
• logical aspects of computational complexity,
• finite model theory,
• computational proof theory,
• logic programming and constraints,
• lambda calculus and combinatory logic,
• domain theory,
• categorical logic and topological semantics,
• database theory,
• specification,
• extraction and transformation of programs,
• logical aspects of quantum computing,
• logical foundations of programming paradigms,
• verification and program analysis,
• linear logic,
• higher-order logic,
• nonmonotonic reasoning.

Dates:

• paper submission: 4 July 2019

### ETAPS 2019: 22nd European Joint Conferences on Theory And Practice of Software, call for participation

6-11 April 2019, Prague, Czech Republic

ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of five main annual conferences, accompanied by satellite workshops. ETAPS 2019 is the twenty-second event in the series.

Main Conferences (8-11 April)

• ESOP: European Symposium on Programming
• FASE: Fundamental Approaches to Software Engineering
• FoSSaCS: Foundations of Software Science and Computation Structures
• POST: Principles of Security and Trust
• TACAS: Tools and Algorithms for the Construction and Analysis of Systems

TACAS '19 hosts the 8th Competition on Software Verification (SV-COMP) and TOOLympics, an event to celebrate the achievements of the various competitions or comparative evaluations.

Satellite Events (6-7 April)
18 satellite workshops and other events will take place before ETAPS 2019: DICE-FOPARA, GaLoP, HSB, QAPL, SynCoP, VerifyThis, TOOLympics (6-7 April) BEHAPI, InterAVT, LiVe, MeTRiD, PERR (6 April) CREST, HCVS, PLACES, SPIoT, SYNTCOMP Camp, Mentoring Workshop (7 April)

See the full program here.

### NFM 2019: The Eleventh NASA Formal Methods Symposium, call for participation

May 7 - 9, 2019, Houston, Texas, USA

The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.

New developments and emerging applications like autonomous software for uncrewed deep space human habitats, caretaker robotics, Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), and the need for system-wide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. The focus of these symposiums are on formal techniques and other approaches for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.

The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Steering Committee, comprised of researchers spanning several NASA centers. NFM 2019 is being co-organized by Rice University and NASA- Johnson Space Center in Houston, TX.

Location & Cost:
The symposium will take place in the McMurtry Auditorium, Rice University, Houston, Texas, USA, May 7--9, 2019. Travel information and discounted hotel reservations can be found here. Houston hotel space is scarce for these dates and the hotel block expires March 20.

There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.

### iFM 2019: 15th International Conference on integrated Formal Methods, call for workshops and tutorials

December 2-6, 2019, Bergen, Norway

iFM 2019 is concerned with how the application of formal methods may involve modelling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modelling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding modelling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.

Besides the standard conference track and the Doctoral Symposium, iFM will host a number of workshops and tutorials related to the theme of the conference. The purpose of the workshops is to provide participants with a friendly, interactive atmosphere for presenting novel ideas and discussing their application. The goal of the tutorials is to enable the participants to familiarise themselves with theoretical aspects and application of formal methods.

Proposals must be written in English, not exceed 5 pages with a reasonable font and margins, and be submitted in PDF format via email to the iFM workshop chairs, Martin Leucker and Violet Ka I Pun.

Workshop proposals should include:

• The name, the duration (1 or 2 days) and the preferred date of the proposed workshop
• A short description of the workshop.
• If applicable, a description of past versions of the workshop, including dates, organisers, submission and acceptance counts, and attendance.
• The publicity strategy that will be used by the workshop organisers to promote the workshop,
• The participant solicitation and selection process.
• The target audience and expected number of participants.
• Approximate budget proposal (see section Budget below for details).
• The equipment and any other resource necessary for the organisation of the workshop.
• The name and short CV of the organiser(s).
• The publication plan (only invited speakers, no published proceedings, pre-/post-proceedings published with EPTCS/ENTCS/...).
Tutorial proposals should include
• The name, the duration (1/2 or 1 day).
• A short description of the tutorial.
• Motivation for the tutorial (e.g., relation to conference).
• Overview of content, description of the aims, presentation style, potential/preferred prerequisite knowledge.
• Intended audience and expected number of participants.
• List of readings, handbook, tools used in the tutorial.

Important Dates

• Submission of proposals: 31th of March 2019
• Notification: 15th of April 2019
• Pre-conference workshops/tutorials: 2-3 December 2019
• Main conference: 4-6 December 2019

### FSCD 2021: the International Conference on Formal Structures for Computation and Deduction, call for location

Delia Kesner, FSCD SC Chair

The FSCD conference covers all aspects of Formal Structures for Computation and Deduction from theoretical foundations to applications. The annual FSCD conference comprises the main conference and a considerable number of affiliated workshops (expectedly, more than ten).

We invite proposals for locations to host the 6th FSCD International Conference to be held during the summer of 2021. Previous (and upcoming) FSCD meetings include:

• FSCD 2016 in Porto (Portugal);
• FSCD 2017 in Oxford (UK) co-located with ICFP 2017;
• FSCD 2018 in Oxford (UK) as part of FLoC 2018;
• FSCD 2019 in Dortmund (Germany);
• FSCD 2020 in Paris (France) co-located with IJCAR 2020.
Therefore, for 2021, we particularly encourage proposals outside Europe.

The deadline for proposals is 31st March 2019. Proposals should be sent to the FSCD Steering Committee Chair (see contact information above). We encourage proposers to register their intention informally as soon as possible. Selected proposals are to be presented at the business meeting of FSCD 2019 taking place at Dortmund in June 2019. The final decision about hosting and organising of FSCD 2021 will be taken by the SC after an advisory vote of the members of the community in attendance at the business meeting.

Proposals should address the following points:

• FSCD Conference Chair (complete name and current position), host institution, FSCD Local Committee (complete names and current positions), availability of student-volunteers.
• National, regional, and local government and industry support, both organizational and financial.
• Accessibility to the location (i.e., transportation) and attractiveness of the proposed site. Accessibility can include both information about local transportation and travel information to the location (flight and/or train connections), as well as estimated costs.
• Appropriateness of the proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities for students.
• Estimated costs on registration for the conference and workshops, both for regular and student participants.
• Conference and exhibit facilities for the anticipated number of registrants (typically around 200). For example: number, capacity and audiovisual equipment of meeting rooms; a large plenary session room that can hold all the registrants; enough rooms for parallel sessions/workshops/tutorials; internet connectivity and workstations for demos/competitions; catering services; and presence of professional staff.
• Residence accommodations and food services in a range of price categories and close to the conference venue, for example, number and cost range of hotels, and availability and cost of dormitory rooms (e.g., at local universities) and kind of services they offer.
• Other relevant information, which can include information about leisure activities and attractiveness of the location (e.g., cultural and historical aspects, touristic activities, etc...).

### LearnAut: Learning and Automata

Learning models defining recursive computations, like automata and formal grammars, are the core of the field called Grammatical Inference (GI). The expressive power of these models and the complexity of the associated computational problems are major research topics within mathematical logic and computer science, spanning the communities that the Logic in Computer Science (LICS) conference brings together. Historically, there has been little interaction between the GI and LICS communities, though recently some important results started to bridge the gap between both worlds, including applications of learning to formal verification and model checking, and (co-)algebraic formulations of automata and grammar learning algorithms.

The goal of this workshop is to bring together experts on logic who could benefit from grammatical inference tools, and researchers in grammatical inference who could find in logic and verification new fruitful applications for their methods.

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

• Computational complexity of learning problems involving automata and formal languages.
• Algorithms and frameworks for learning models representing language classes inside and outside the Chomsky hierarchy, including tree and graph grammars.
• Learning problems involving models with additional structure, including numeric weights, inputs/outputs such as transducers, register automata, timed automata, Markov reward and decision processes, and semi-hidden Markov models.
• Logical and relational aspects of learning and grammatical inference.
• Theoretical studies of learnable classes of languages/representations.
• Relations between automata and recurrent neural networks.
• Active learning of finite state machines and formal languages.
• Methods for estimating probability distributions over strings, trees, graphs, or any data used as input for symbolic models.
• Applications of learning to formal verification and (statistical) model checking.
• Metrics and other error measures between automata or formal languages.

Important dates

• Submission deadline: March 30th, 2019
• Notification of acceptance: April 25th, 2019
• Workshop: June 23rd, 2019

## Workshops

### ThEdu'19: Theorem proving components for Educational software, call for papers

August 25 or 26, 2019, Natal, Brazil

Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems.

Topics of interest include:

• methods of automated deduction applied to checking students' input;
• methods of automated deduction applied to prove post-conditions for particular problem solutions;
• combinations of deduction and computation enabling systems to propose next steps;
• automated provers specific for dynamic geometry systems;
• proof and proving in mathematics education.

Important Dates

• Extended Abstracts: 5 May 2019
• Author Notification: 2 June 2019
• Workshop Day: 25 or 26 August 2019

### LSFA 2019: 14th Workshop on Logical and Semantic Frameworks, with Applications, call for papers

August 24-26, 2019, Natal, Brazil

Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning. LSFA 2019 will be a satellite event of CADE-27.

Topics of interest include, but are not limited to:

• Specification languages and meta-languages
• Formal semantics of languages and logical systems
• Logical frameworks
• Semantic frameworks
• Type theory
• Proof theory
• Automated deduction
• Implementation of logical or semantic frameworks
• Applications of logical or semantic frameworks
• Computational and logical properties of semantic frameworks
• Logical aspects of computational complexity
• Lambda and combinatory calculi
• Process calculi

Important Dates:

• Notification to authors: May 24
• ENTCS proceedings version due: June 21
• LSFA 2019: August 24-26

### PxTP 2019: Sixth Workshop on Proof eXchange for Theorem Proving, call for papers

August 25-26, 2019, Natal, Brazil

The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms. PxTP 2019 is affiliated with the 27th International Conference on Automated Deduction (CADE-27).

The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and also collaboration between HOL Light and Isabelle in the formal proof of the Kepler conjecture.

Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation and communication methods, standards, protocols, and programming interfaces. The workshop welcomes the interested developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are also interested both in success stories and in descriptions of the current bottlenecks and proposals for improvement.

Topics
Topics of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are:

• applications that integrate reasoning tools (ideally with certification of the result);
• interoperability of reasoning systems;
• translations between logics, proof systems, models;
• distribution of proof obligations among heterogeneous reasoning tools;
• algorithms and tools for checking and importing (replaying, reconstructing) proofs;
• proposed formats for expressing problems and solutions for different classes of logic solvers (SAT, SMT, QBF, first-order logic, higher-order logic, typed logic, rewriting, etc.);
• meta-languages, logical frameworks, communication methods, standards, protocols, and APIs related to problems, proofs, and models;
• comparison, refactoring, transformation, migration, compression and optimization of proofs;
• data structures and algorithms for improved proof production in solvers (e.g. efficient proof representations);
• (universal) libraries, corpora and benchmarks of proofs and theories;
• alignment of diverse logics, concepts and theories across systems and libraries;
• engineering aspects of proofs (e.g. granularity, flexiformality, persistence over time);
• proof certificates;
• proof checking;
• mining of (mathematical) information from proofs (e.g. quantifier instantiations, unsat cores, interpolants, ...);
• reverse engineering and understanding of formal proofs;
• universality of proofs;
• origins and kinds of proofs (e.g. (in)formal, automatically generated, interactive, ...);
• Hilbert's 24th Problem (i.e. what makes a proof better than another?);
• social aspects (e.g. community-wide initiatives related to proofs, cooperation between communities, the future of (formal) proofs);
• applications relying on importing proofs from automatic theorem provers, such as certified static analysis, proof-carrying code, or certified compilation;
• application-oriented proof theory;
• practical experiences, case studies, feasibility studies;

Important Dates

• Abstract submission: May 12, 2019
• Paper submission: May 19, 2019
• Author notification: Juine 21, 2019
• Camera ready version due: July 14, 2019
• Workshop: 25-25 August, 2019

### ARCADE 2019: "Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements", call for papers

August 25 or 26, 2019, Natal, Brazil

The main goal of this workshop is to bring together key people from various sub-communities of automated reasoning—such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving—to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community.

The structure of the workshop will be informal. We invite extended abstracts in the form of non-technical position statements aimed at prompting lively discussion. The title of the workshop is indicative of the kind of discussions we would like to encourage:

• Challenges: What are the next grand challenges for research on automated reasoning? Thereby, we refer to problems, solving which would imply a significant impact (e.g., shift of focus) on the CADE community and beyond?
• Applications: Is automated reasoning applicable in real-world (industrial) scenarios? Should reports on such applications be encouraged at a venue like CADE, perhaps by means of a special case study paper category?
• Directions: Based on the grand challenges and requirements from real- world applications, what are the research directions the community should promote? What bridges between the different sub-communities of CADE need to be strengthened? What new communities should be included?
• Exemplary Achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself? What can we learn from those successes when shaping our future research?

### UNIF 2019: the 33rd International Workshop on Unification, call for papers

June 24, 2019, Dortmund, Germany

Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.

Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense. Topics of interest to this forum include, but are not limited to:

• Unification algorithms, calculi, and implementations
• Equational unification and unification modulo theories
• Unification in modal, temporal and description logics
• Narrowing
• Formalisation of unification
• Matching Problems
• Applications
• Unification in Special Theories
• Higher-Order Unification
• Combination problems
• Constraint Solving
• Disunification
• Complexity Issues
• Type Checking and reconstruction

The workshop is proposed to be hosted by the 4th International Conference on Formal Structures for Computation and Deduction (FSCD, Dortmund, 24-29 June 2019).

Important Dates

• Submission of titles and abstracts: April 14, 2019
• Submission of full paper: April 21, 2019
• Author notification: May 31, 2019
• Camera-ready papers: June 4, 2019
• UNIF 2019: June 24, 2019 (intended)

### ICE 2019: 12th Interaction and Concurrency Experience

June 20-21, 2019, Lyngby, Denmark

Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions. ICE 2019 is a satellite workshop of DisCoTec 2019.

The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. We solicit contributions relevant to Intereaction and Concurrency, including but not limited to:

• Formal semantics
• Process algebras and calculi
• Models and languages
• Protocols
• Logics and types
• Expressiveness
• Model transformations
• Tools, implementations, and experiments
• Specification and verification
• Coinductive techniques
• Tools and techniques for automation
• Synthesis techniques

Important dates

• Paper registration deadline: March 26, 2019
• Paper submission deadline: April 2, 2019
• Notification of acceptance: May 3, 2019
• Camera-ready copies: May 24, 2019
• Workshop: June 18-21, 2019

### The Coq Workshop 2019: call for talk proposals

September 8 2019, Portland, OR, USA

The Coq workshop is part of ITP 2019.

While conferences usually provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks.

We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop.

Relevant subject matter includes but is not limited to:

• Theory and implementation of the Calculus of Inductive Constructions
• Language or tactic features
• Plugins and libraries for Coq
• Techniques for formalization programming languages and mathematics
• Applications and experience in education and industry
• Tools and platforms built on Coq (including interfaces)
• Formalization tricks and pearls

Important dates:

• June 4 2019: Deadline for abstract submission
• July 2 2019: Notification to authors
• September 8 2019: Workshop

### ICE 2019: 12th Interaction and Concurrency Experience

June 20-21, 2019, Lyngby, Denmark

Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions. ICE 2019 is a satellite workshop of DisCoTec 2019.

The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. We solicit contributions relevant to Intereaction and Concurrency, including but not limited to:

• Formal semantics
• Process algebras and calculi
• Models and languages
• Protocols
• Logics and types
• Expressiveness
• Model transformations
• Tools, implementations, and experiments
• Specification and verification
• Coinductive techniques
• Tools and techniques for automation
• Synthesis techniques

Important dates

• April 18, 2019: abstract submission
• April 20, 2019: paper submission
• April 20 - May 11, 2019: reviews and PC discussion
• June 20-21, 2019: ICE workshop
• July 15, 2019: camera-ready for EPTCS post-proceedings

### NSV 2019: The 12th International Workshop on Numerical Software Verification, call for papers

July 13-14, 2019, New York, NY, USA

Numerical computations are ubiquitous in digital systems: supervision, prediction, simulation and signal processing rely heavily on numerical calculus to achieve desired goals. Design and verification of numerical algorithms has a unique set of challenges, which set it apart from rest of software verification. To achieve the verification and validation of global properties, numerical techniques need to precisely represent local behaviors of each component. The implementation of numerical techniques on modern hardware adds another layer of approximation because of the use of finite representations of infinite precision numbers that usually lack basic arithmetic properties such as commutativity and associativity. Finally, the development and analysis of cyber-physical systems (CPS) which involve the interacting continuous and discrete components pose a further challenge. It is hence imperative to develop logical and mathematical techniques for the reasoning about programmability and reliability. The NSV workshop is dedicated to the development of such techniques. NSV 2019 is co-located with CAV.

Topics of interest:
The scope of the workshop includes, but is not restricted to, the following topics:

• Quantitative and qualitative analysis of hybrid systems
• Models and abstraction techniques
• Optimal control of dynamical systems
• Parameter identification for hybrid systems
• Numerical optimization methods
• Hybrid systems verification
• Applications of hybrid systems to systems biology
• Propagation of uncertainties, deterministic and probabilistic models
• Specifications of correctness for numerical programs
• Quality of finite precision implementations
• Numerical properties of control software
• Validation for space, avionics, automotive and real-time applications
• Validation for scientific computing programs

Important Dates:

• Submission deadline: 24 April 2019
• Notification of acceptance: 22 May 2019
• Final version: 29 May 2019
• Workshop: 13-14 July 2019

### LearnAut: Learning and Automata, call for papers

The Coq workshop is part of ITP 2019.

While conferences usually provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks.

We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop.

Relevant subject matter includes but is not limited to:

• Theory and implementation of the Calculus of Inductive Constructions
• Language or tactic features
• Plugins and libraries for Coq
• Techniques for formalization programming languages and mathematics
• Applications and experience in education and industry
• Tools and platforms built on Coq (including interfaces)
• Formalization tricks and pearls

Important dates:

• Submission deadline: March 30th, 2019
• Notification of acceptance: April 25th, 2019
• Workshop: June 23rd, 2019

### IWC 2019: 8th International Workshop on Confluence, call for papers

June 28, 2019, Dortmund, Germany

Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties. It is collocated with FSCD.

Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications.

Topics:

• confluence and related properties (unique normal forms, commutation, ground confluence)
• completion
• critical pair criteria
• decidability issues
• complexity issues
• system descriptions
• certification
• applications of confluence
The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2019 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.

Important Dates

• Title and Abstract:   April 14, 2019
• Paper Submission:   April 21, 2019
• Notification to authors:   May 24, 2019
• Workshop date:   June 28, 2019

### Fifth Workshop on: Bridging the Gap between Human and Automated Reasoning, call for papers

August 10 - 12, 2019, Macau, China

A core goal of Bridging-the-gap-Workshops is to make results from psychology, cognitive science, and AI accessible to each other. The goal is to develop systems that can adapt themselves to an individuals' reasoning process and that such systems follow the principle of explainable AI to ensure trustfulness and to support the integration of results from other fields. We propose a human syllogistic reasoning challenge to predict future inferences of an individual reasoner based on some previous observations. Hence, participants can develop cognitive AI models (written in Python) that predict the next inference. These predictions are then evaluated in the CCobra framework.

Despite a common research interest -- reasoning -- there are still several milestones necessary to foster a better inter-disciplinary research. First, to develop a better understanding of methods, techniques, and approaches applied in both research fields. Second, to have a synopsis of the relevant state-of-the-art in both research directions. Third, to combine methods and techniques from both fields and find synergies. E.g., techniques and methods from computational logic have never been directly applied to model adequately human reasoning. They have always been adapted and changed. Fourth, we need more and better experimental data that can be used as a benchmark system. Fifth, cognitive theories can benefit from a computational modeling. Hence, both fields -- human and automated reasoning -- can both contribute to these milestones and are in fact a conditio sine qua non. Achievements in both fields can inform the others. Deviations between fields can inspire to seek a new and profound understanding of the nature of reasoning. Additionally to predict human inferences is a major step that can help to foster the integration of digital companions and cognitive assistance systems into our everyday life. An important condition is that such systems can adapt themselves to an individual's reasoning process and that such systems follow the principle of explainable AI to ensure trustfulness and to support the integration of results from other fields. Symbolic approaches do provide an easier access to it.

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

• limits and differences between automated and human reasoning
• psychology of deduction and common sense reasoning
• logics modeling human reasoning
• non-monotonic, defeasible, and classical reasoning
• benchmark problems relevant in both fields
• approaches to tackle benchmark problems like the Winograd Schema Challenge or the COPA challenge
• predicting an individual reasoners response (see here)

The workshop will be located at the 28th International Joint Conference on Artificial Intelligence (IJCAI 2019) at Macao, China. The Bridging workshop is supported by IFIP TC12.

Important Dates

• Full Paper submission deadline: 12th April, 2019
• Final submission: 10th June, 2019
• Model submission for PRECORE challenge: 15th May, 2019
• Workshop: 10th - 12th August, 2019

### Dynamic Logic: New Trends and Applications, call for papers

October 9, 2019, Porto, Portugal

Building on the pioneer intuitions of Floyd-Hoare logic, dynamic logic was introduced in the 70's as a suitable logic to reason about, and verify, classic imperative programs. Since then, the original intuitions grew to an entire family of logics, which became increasingly popular for assertional reasoning about a wide range of computational systems. Simultaneously, their object (i.e. the very notion of a program) evolved in unexpected ways. This lead to dynamic logics tailored to specific programming paradigms and extended to new computing domains, including probabilistic, continuous and quantum computation. Both its theoretical relevance and practical potential make dynamic logic a topic of interest in a number of scientific venues, from wide-scope software engineering conferences to modal logic specific events. However, no specific event is exclusively dedicated to it. This workshop aims at filling fill such a gap, joining an heterogeneous community of colleagues, from Academia to Industry, from Mathematics to Computer Science.

Topics
Submissions are invited on the general field of dynamic logic, its variants and applications, including, but not restricted to

• Dynamic logic, foundations and applications
• Logics with regular modalities
• Modal/temporal/epistemic logics
• Kleene and action algebras and their variants
• Quantum dynamic logic
• Coalgebraic modal/dynamic logics
• Graded and fuzzy dynamic logics
• Dynamic logics for cyber-physical systems
• Dynamic epistemic logic
• Complexity and decidability of variants of dynamic logics and temporal logics
• Model checking, model generation and theorem proving for dynamic logics

Important Dates

• Paper Submission: June 14, 2019
• Camera Ready: September 2, 2019
• Workshop: October 9, 2019

### F-IDE Workshop 2019, 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:

• F-IDE building: design and integration of languages, development of user-friendly front-ends
• How to make high-level logical and programming concepts palatable to industrial developers
• Integration of Object-Oriented and modularity features
• Integration of static analyzers
• Integration of automatic proof tools, theorem provers and testing tools
• Documentation tools
• Impact of tools on certification
• Experience reports on developing F-IDEs
• Experience reports on using F-IDEs
• Experience reports on formal methods-based assessments in industrial applications

The F-IDE workshop is part of FM Week 2019.

Important Dates

• Abstract submission: June 18, 2019
• Paper submission: June 25, 2019
• Camera-ready version: September 3, 2019
• Workshop date: October 7, 2019

### HOR 2019: 10th International Workshop on Higher-Order Rewriting, call for submissions

June 28 2019, Dortmund, Germany

HOR is a forum to present work concerning all aspects of higher-order rewriting. HOR 2019 is affiliated with FSCD 2019.

HOR aims to provide an informal and friendly setting to discuss recent work and work in progress concerning higher-order rewriting, broadly construed. This includes rewriting systems that have functional variables or bound variables, the lambda-calculus and combinatory logic being paradigmatic examples.

Topics
The following is a non-exhaustive list of topics for the workshop:

• Applications: proof checking, theorem proving, generic programming, declarative programming, program transformation.
• Foundations: pattern matching, unification, strategies, narrowing, termination, syntactic properties, type theory.
• Frameworks: term rewriting, conditional rewriting, graph rewriting, net rewriting, comparisons of different frameworks.
• Implementation: graphs, nets, abstract machines, explicit substitution, rewriting tools, compilation techniques.
• Semantics: operational semantics, denotational semantics, separability, higher-order abstract syntax.

Important Dates

• Submission deadline: 15 April 2019
• Final version: 31 May 2019

### WPTE 2019: Sixth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, call for papers

June 24, 2019, Dortmund, Germany

The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally-based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.

Topics of interest in the scope of this workshop include:

• Correctness of program transformations, optimizations and translations.
• Program transformations for proving termination, confluence and other properties.
• Correctness of evaluation strategies.
• Operational semantics of programs, operationally-based program equivalences such as contextual equivalences and bisimulations.
• Cost-models for reasoning about the optimizing power of transformations and the costs of evaluation.
• Program transformations for verification and theorem proving purposes.
• Translation, simulation, equivalence of programs with different formalisms, and evaluation strategies.
• Program transformations for applying rewriting techniques to programs in specific programming languages.
• Program transformations for program inversions and program synthesis.
• Program transformation and evaluation for Haskell and Rewriting.
The programming languages of interest include pure, deterministic, impure, nondeterministic, concurrent, parallel languages, and may employ programming paradigms such as functional, logical, typed, imperative, object-oriented, and higher-order.

Important Dates

• Submission of extended abstracts: April 15, 2019
• Notification of acceptance: May 20, 2019
• Final version for proceedings deadline: May 27, 2019
• Workshop: June 24, 2019
• Submission deadline for post proceedings: September, 2019 (exact date to be announced)

### SD'19: 5th Int. Workshop on Structures and Deduction 2019, call for papers

June 29-30, 2019, Dortmund, Germany

SD’19 is the fifth in a series of workshops aiming to gather various communities of structural proof theorists. As well as theoretical work in the form of regular papers, we encourage submission of implementations, tools and system descriptions. SD'19 is affiliated with FSCD 2019

Topics of interest

• Syntactic representations of proofs (e.g. sequent calculi, deep inference, focusing)
• Combinatorial representations of proofs (e.g. proof nets)
• Algebraic representations of proofs (e.g. via game semantics or category theory)
• Methods for proof manipulation and normal forms of proofs
• Formulas-as-types interpretations of proofs
• Computation and rewriting in proof search (e.g. deduction modulo or cyclic proofs)
• Complexity theoretic aspects of proof representations

Important Dates

• Submission: April 12

### LCC 2019: 20th International Workshop on Logic and Computational Complexity, call for contributions

July 8, 2019, Patras, Greece

LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. The program will consist of invited lectures as well as contributed talks selected by the Program Committee. LCC 2019 is collocated with ICALP 2019.

Important Dates:

• submission May 1, 2019
• workshop July 8, 2019

### WiL 2019: 3rd Women in Logic Workshop, call for talks and papers

Women are chronically underrepresented in the LiCS community. The workshop will provide an opportunity for women in the field to increase awareness of one another and one another’s work, to combat the feeling of isolation. It will also provide an environment where women can present to an audience comprising mostly women, replicating the experience that most men have at most LiCS meetings, and lowering the stress of the occasion; we hope that this will be particularly attractive to early-career women. WiL 2019 is affiliated with the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).

Previous versions of Women in Logic (Reykjavik, Iceland 2017 and Oxford, UK 2018) were very successful in showcasing women's work and as catalysts for recognition of the need for change in the community. Our extended program committee tries to cover most areas of Logic in Computer Science. These include but are not limited to the usual Logic in Computer Science (LICS) topics. These are:

• automata theory,
• automated deduction,
• categorical models and logics,
• concurrency and distributed computation,
• constraint programming,
• constructive mathematics,
• database theory,
• decision procedures,
• description logics,
• domain theory,
• finite model theory,
• formal aspects of program analysis,
• formal methods,
• foundations of computability,
• games and logic,
• higher-order logic,
• lambda and combinatory calculi,
• linear logic,
• logic in artificial intelligence,
• logic programming,
• logical aspects of bioinformatics,
• logical aspects of computational complexity,
• logical aspects of quantum computation,
• logical frameworks,
• logics of programs,
• modal and temporal logics,
• model checking,
• probabilistic systems,
• process calculi,
• programming language semantics,
• proof theory,
• real-time systems,
• reasoning about security and privacy,
• rewriting,
• type systems and type theory, and
• verification.

Important Dates

• Paper submission deadline: 7 April 2019
• Author notification: 23 April 2019
• Contribution for Informal Proceedings: 9 May 2019

### LFMTP 2019: Logical Frameworks and Meta-Languages: Theory and Practice, call for papers

22 June 2019, Vancouver, CA, USA

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.

LFMTP 2019 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:

• Encoding and reasoning about the meta-theory of programming languages, logical systems and related formally specified systems.
• Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.
• Logical treatments of inductive and co-inductive definitions and associated reasoning techniques, including inductive types of higher dimension in homotopy type theory
• Graphical languages for building proofs, applications in geometry, equational reasoning and category theory.
• New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy and cubical type theory.
• Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc.
• Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog.

Important Dates

• Abstract submission deadline: Monday March 25
• Submission deadline: Monday April 1
• Notification to authors: Monday April 30
• Final version due: Monday May 21
• Workshop date: Saturday June 22

### HCVS 2019: 6th Workshop on Horn Clauses for Verification and Synthesis

April 7, 2019, Prague, Czech Republic
Co-located with ETAPS 2019

Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses, and many recent advances in the Constraint/Logic Programming, Verification, and Automated Deduction communities have centered around efficiently solving problems presented as Horn clauses.

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:

• Analysis and verification of programs and systems of various kinds (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent)
• Program synthesis
• Program testing
• Program transformation
• Constraint solving
• Type systems
• Case studies and tools
• Challenging problems

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 on the competition's web page. 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

• Paper submission: 15 Feb 2019
• Paper notification: 7 Mar 2019
• Camera-ready (for informal pre-proceedings): 15 Mar 2019
• Workshop: 7 Apr 2019
• Final camera-ready (for formal post-proceedings): 12 May 2019

### CLA'19 meeting: the Computational Logic and Applications workshop, call for submissions

July 1-2, 2019, Versailles, France

The Computational Logic and Applications (CLA) workshops are a series of annual meetings, whose main purpose is to provide a free and open forum for research on combinatorial and quantitative aspects of mathematical logic and their applications in computer science.

Scope
Topics within the scope of CLA include:

• combinatorics of lambda calculus and related formalisms,
• quantitative aspects of program evaluation and normalisation,
• asymptotic enumeration in computational logic,
• statistical properties of formulae, terms and programs,
• random generation of large combinatorial structures in computational logic,
• randomness in software testing and counter-example generation methods.

Special Issue
Following the meeting, a special issue of DMTCS is planned for early 2020 with full papers on the topics of CLA. These papers can be either results presented at the 2019 CLA meeting, or at a former meeting but not published elsewhere, or results not presented at CLA, as long as they fall within the scope of the workshop. The submitted papers should present original research, including survey papers, which is not already published or submitted to publication to another journal.

Important Dates
• June 11, 2019: submission deadline for talk proposals
• June 14, 2019: speaker notification for workshop
• June 24, 2019: registration deadline
• July 1-2, 2019: workshop
• September 30, 2019: submission deadline for contributions to the DMTCS special issue

### Martin Hofmann Memorial Meeting, call for participation

July 13, 2019, Munich, Germany

This is the first call for participation for a one-day meeting in memory of Martin Hofmann in Munich on Saturday, 13 July 2019.

We will meet to remember and celebrate Martin's life and work. There will be invited talks from friends and colleagues as well as ample time for discussions and exchange of memories during the breaks. The talks will be about various topics in Computer Science and Mathematics that Martin would have enjoyed. The talks will combine scientific content with personal stories about Martin.

If you are planning to attend then please register on the website of the meeting.

There may be a small registration fee to help cover refreshments; more information later.

If you would like to propose a contribution to the program then contact Jan Hoffmann or Don Sannella.

Important Dates:

• registration opens May 1, 2019
• registration closes July 1, 2019
• workshop July 13, 2019

## Summer Schools

### Caleidoscope: Research School in Computational Complexity

June 17-21, 2019, Paris, France

Computational complexity theory was born more than 50 years ago when researchers started asking themselves what could be computed efficiently. Classifying problems/functions with respect to the amount of resources (e.g. time and/or space) needed to solve/compute them turned out to be an extremely difficult question. This has led researchers to develop a remarkable variety of approaches, employing different mathematical methods and theories.

The future development of complexity theory will require a subtle understanding of the similarities, differences and limitations of the many current approaches. In fact, even though these study the same phenomenon, they are developed today within disjoint communities, with little or no communication between them (algorithms, logic, programming theory, algebra...). This dispersion is unfortunate since it hinders the development of hybrid methods and more generally the advancement of computational complexity as a whole.

The goal (and peculiarity) of the Caleidoscope school is to reunite in a single event as many different takes on computational complexity as can reasonably be fit in one week. It is intended for graduate students as well as established researchers who wish to learn more about neighbouring areas.

Lectures

1. Boolean circuits and lower bounds. (Rahul Santhanam, University of Oxford)
2. Algebraic circuits and geometric complexity. (Peter Bürgisser, Technical University Berlin)
3. Proof complexity and bounded arithmetic. (Sam Buss, University of California San Diego)
4. Machine-free complexity (descriptive and implicit complexity). (Anuj Dawar, University of Cambridge and Ugo Dal Lago, University of Bologna)
In addition to these broad-ranging themes, there will also be three more focussed topics, providing examples of (already established or potential) interactions between logic, algebra and complexity:
1. Constraint satisfaction problems. (Libor Barto, Charles University in Prague)
2. Communication complexity. (Sophie Laplante, Paris 7 University)
3. Duality in formal languages and logic. (Daniela Petrisan, Paris 7 University)

### ISR'19: 11th International School on Rewriting

July 1-6 2019, Paris, France

Rewriting is a simple yet powerful model of computation with numerous applications in computer science and many other fields: logic, mathematics, programming languages, model checking, quantum computing, biology, music...

ISR'19 is hosted in the center of Paris and proposes to master students, PhD students and researchers, two parallel tracks:

• basic track: introduction to first-order term rewriting and λ-calculus with lectures by Aart Middeldorp, Sarah Winkler and Femke van Raamsdonk
• advanced track: lectures on rewriting theory and applications
• Automated complexity analysis of term rewrite systems, Martin Avanzini
• Reachability in logically constrained term rewriting systems, Stefan Ciobaca
• Deduction modulo rewriting, Gilles Dowek
• Introduction to graph rewriting, Rachid Echahed
• Rewriting and music, Florent Jacquemard
• Picturing quantum processes, rewriting quantum pictures, Aleks Kissinger
• Stochastic graph rewriting and (executable) knowledge representation for molecular biology, Jean Krivine
• Higher-order term rewriting, Cynthia Kop
• Homotopy and homology of rewriting, Yves Lafont
• Rewriting in theorem proving, Christopher Lynch
• Formal specification and analysis of real-time systems in Real-Time Maude, Peter Csaba Ölveczky
• Infinitary rewriting and streams, Hans Zantema

Registration is open until May 17!

### Midlands Graduate School 2019 in the Foundations of Computing Science

April 14-18, 2019, Birmingham, UK

The Midlands Graduate School (MGS) in the Foundations of Computing Science provides an intensive course of lectures on the mathematical foundations of computing. The MGS has been running since 1999, and is aimed at PhD students in their first or second year of study, but the school is open to everyone, and has increasingly seen participation from industry. We welcome participants from all over the world!

Courses:
Eight courses will be given. Participants usually take all the introductory courses and choose additional options from the advanced courses depending on their interests.

• Invited course
• Adventures in Property Based Testing, John Hughes
• Introductory courses
• Lambda Calculus, Venanzio Capretta
• Category Theory, Thorsten Altenkirch
• Univalent Type Theory in Agda, Martín Escardó
• Calculating programs, Jennifer Hackett
• Type Refinement Systems, Noam Zeilberger
• Synthesis of Reactive Systems, Rayna Dimitrova
• Monoidal Categories, Higher Categories, Jamie Vicary

The registration deadline is Sunday, 31 March. Spaces are limited, so please register early to secure your place.

### Ninth Summer School on Formal Techniques

May 18 - 24, 2019, Atherton, California

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

The lecturers at the school include:

• Peter Mueller, ETH Zurich Switzerland: Modular Program Verification
• Daniel Jackson, CSAIL MIT USA: A principled approach to software design
• Orna Grumberg, Technion Israel: Model Checking and its Applications
• Kwangkeun Yi, Seoul National University, S. Korea: Introduction to Static Analysis from an Abstract Interpretation Perspective
• Benjamin Gregoire, INRIA France: An overview of Easycrypt and how to prove concrete security of cryptographic primitives
The main lectures in the summer school will be preceded by a background course on logic:
• Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (SRI-CSL) Speaking Logic
The school also include several distinguished invited talks.

Applicants are urged to submit their applications before April 30, 2019, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early. We strongly encourage the participation of women and under-represented minorities in the summer school.

For more information and to apply go to the summer school web page.

### 40th edition of the International Summer School Marktoberdorf 2019

The 40th edition of the International Summer School Marktoberdorf 2019 based on the excellent networking in the Summer School Marktoberdorf series on Safety and Security of Software Systems: Logics, Proofs, Applications is now ready for application. Deadline is: April 7, 2019.

The "Marktoberdorf Summer School" is a ten days' course for young computer scientists and mathematicians working in the field of formal software and systems development. It takes place at the little town of Marktoberdorf, this year from July 31 to August 9, 2019.

Our challenge is to give in-depth presentations of state-of-the-art topics in verification for safety and security of software systems and to promote international contacts and collaborations between leading researchers and young scientists.

Further information including lecturers, topics and the application form are available on the web page of the summer school.

### Autumn school "Proof and Computation"

September 20 - 26, 2019, Herrsching, Germany

The fourth international autumn school "Proof and Computation" will be held from 20th to 26th September 2019 in Herrsching near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy.

Scope

• Predicative Foundations
• Constructive Mathematics and Type Theory
• Computation in Higher Types
• Extraction of Programs from Proofs

Deadline for applications: 31st May 2019. Applicants will be notified by 28th June 2019.

More information such as financial support and application procedure are available on the school's web page.

## Competitions

### CASC 2019: the CADE ATP System Competition, call for participation

In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-27 will be held during the 27th International Conference on Automated Deduction (CADE-27).

CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of:

• the number of problems solved,
• the number of problems solved with a solution output, and
• the average runtime for problems solved;
in the context of:
• a bounded number of eligible problems, chosen from the TPTP Problem Library, and
• specified time limits on solution attempts.

• System submission for problem rating (optional) 17th June Email to Organizers
• System registration deadline 22nd June Online
• System descriptions deadline 29th July Email to Organizers
• Sample solutions deadline 29th July Email to Organizers
• Formal CASC registration 29th July Online
• System delivery deadline 5th August
• Soundness testing reports 9th August
• Unsoundness repairs completed 16th August

### SyGuS-COMP 2019 Call for Solvers and Benchmarks Submission

This is a call for participation for the 6th Syntax-Guided Synthesis Competition to be organized as a satellite event of SYNT & CAV 2019 in New York City.

The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementation. The motivation is twofold. First, narrowing the space of implementations makes the synthesis problem more tractable. Second, providing a specific syntax can potentially lead to better optimizations.

The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions that satisfies the specification in the given theory. The formulation of the problem builds on SMT-LIB.

There has been a lot of recent interest in both using SyGuS solvers for various synthesis applications and developing different solving algorithms. Despite significant progress in solution strategies in the last few years, synthesis remains a challenging problem. Last year, in the general track, more than 25% of the problems were unsolved, and we welcome solvers that can advance the state of the art.

Important Dates:

• 1 May 2019: Benchmark submission deadline.
• 1 June 2019: Deadline for first version of solvers.
• 14 June 2019: Deadline for final version of solvers and for solver description
• 7 July 2019: Author notification
• 13/14 July 2019: Solvers presentation (at SYNT workshop)

## Open Positions

### PhD Studentship at UCL: 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

1. deepen the theoretical understanding of reductive logic, facilitating a broadening of the applicability of such techniques;
2. implement prototype provers and automated reasoning support based on a clear, principled semantics;
3. interface with state-of-the-art coalgebraic and category theoretic approaches to the semantics of programs and probabilistic inference to understand and export shared features of key applications of reductive reasoning like Facebook’s program verification tool Infer and the machine-learning paradigm inductive logic programming.

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.

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.

### Jobs at multiple levels in Canberra Australia

Rajeev Gore

We are advertising both fixed term and tenure track positions in computer sciences from level B (assistant professor), level C (associate professor) and level D (associate professor plus plus :)

See here.

Canberra is a great place to live! See here.

We are also into proof-theory, formal verification using HOL4, Isabelle/HOL and Coq, type-theory and other topics which should be music to your ears, see here.

Please feel free to contact me if you wish to discuss applying.

And I promise that there are no crocodiles, jellyfish or sharks in our lake! See here.

### PostDoc position at Inria Paris on Formally Secure Compilation in Coq

Catalin Hritcu

A PostDoc position is available in my group at Inria Paris on Formally Secure Compilation in Coq. I am seeking outstanding candidates with a strong, internationally competitive research track record. Particularly interesting for us is research expertise in:

• formal verification in the Coq proof assistant and verified compilation in particular (e.g. CompCert)
• security foundations, e.g., reference monitoring, hyperproperties, noninterference
Here are some (non-exhaustive) lists 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!

### Phd (4 years) or Postdoc (2 years) Position at TU Darmstadt

There is a vacancy for either a PhD student (up to 4 years) or a Postdoc (2 years) in the Software Engineering group at TU Darmstadt, Germany. We perform cutting-edge research in the intersection between software engineering and formal methods, being a co-developer of the leading static verification tool KeY. You will work in a DFG-funded project that looks at one of the most intriguing questions in software analysis: how can information from static verification be combined with information obtained at runtime? We will investigate methodologies and data structures suitable to represent information from hybrid sources. To this end we team up with the group of Bernhard Steffen at TU Dortmund who develop LearnLib , a leading tool for automated learning of automata-based models from execution traces.

The salary follows the E13 scale . You will work in an international research group with a friendly and supportive climate. TU Darmstadt offers excellent training and development opportunities for young researchers.

Prerequisites:
For a PhD position we expect a very good MSc degree in Computer Science or a closely related field, as well as documented research exposure in an area relevant to the position, for example, a first publication or an excellent, research-oriented MSc thesis. For a postdoc position we expect a PhD in a relevant area, such as software engineering, formal methods, static analysis, or programming languages as well as several international, peer-reviewed publications. The position is available immediately.

Please send your application consisting of the usual material (cover letter, CV, papers, thesis, grade record, name of one or two references) as a zip file to this email address.

### PhD Positions on Verified Mathematics at VU Amsterdam

Jasmin Blanchette

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.

As part of this project, we will develop formal libraries of fundamental number theory in Lean 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 contribute to the development of 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 me for more information.

### Multiple Research Positions, IMDEA Software Institute, Madrid, Spain

Applications are invited for multiple positions (PhD/Postdoc/Scientific Programmer) at the IMDEA Software Institute, Madrid, Spain.

Selected candidates will work under the supervision of Aleks Nanevski. The topic of the research, to be determined based on the common interests of the candidate and the supervisor, will be in the areas of software verification, logics for concurrent programs, and language-based security. The research will be funded by Aleks' ERC Consolidator award "MATHADOR: Type and Proof Structures for Concurrent Software Verification", which aims to investigate the type-theoretic foundations for verification of concurrent software.

PhD candidates should have an excellent MSc or BSc degree in computer science or a related subject, with an interest in the above areas, and a strong commitment to research.

Postdoc candidates should have, or expect shortly to obtain, a PhD in computer science. The ideal candidate will have expertise in program semantics and program logics, concurrent or distributed computing, type theory or interactive theorem proving, as they apply to the above areas.

Scientific programmer candidates should hold a BSc or MSc degree in computer science, with experience in and passion for functional programming and interactive theorem proving (eg., Coq).

All positions require good teamwork and communication skills, including excellent spoken and written English. Salaries at IMDEA Software Institute are internationally competitive.

Deadline for applications is March 31st, 2019. Review of applications will begin immediately.

Applications should be submitted online here.

### Fully-funded PhD studentship on weak-memory concurrency (University of Kent)

with Mark Batty, Research Fellow of the Royal Academy of Engineering.

The UK Research Institute in Verified Trustworthy Software Systems and the UK's National Cyber Security Centre have provided a fully funded 3.5-year PhD scholarship (for UK/EU students) to work on concurrency, programming languages and formal methods in Mark Batty's group at the University of Kent in Canterbury, UK. Applications are due by the 26th April 2019.

The post is suited to a wide range of applicants with formal or practical skills: you will join a team that spans theory (formal semantics, verification, proof) and practice (tool building, concurrent programming, compilation).

The project will focus on concurrency in mainstream programming languages where our work has found fundamental problems and made changes to the C and C++ standards through the International Standards Organisation (ISO). The specifications of Languages like C/C++ and Java do not adequately describe when the programmer can rely on the compiler to leave program dependencies in place, or when the optimiser is free to remove them. Removing dependencies can lead to unexpected concurrency behaviour as it enables speculative execution on the processor. Industry bodies like the ISO know that their specifications are broken and keenly await a fix. We have a fix, and we are building tools and verification techniques around it. The PhD project focusses on this area of research.

This research is part of PLAS, one of the largest programming languages research groups in Europe. It is currently ranked 17th worldwide by the independent CSrankings website. We provide a supportive environment for research and we have a vibrant postgraduate population. We encourage our students to engage with the wider research community through attending conferences and taking internships with leading industrial companies. We are located in Canterbury, a lively and cosmopolitan historic town with convenient travel links to London and Europe.

Application process:

• Contact Mark Batty by email including a brief CV (preferably by the first week of April 2019).
• Submit a formal application through the university admission system by the 26th April 2019. Your application should include a completed online admission form; the name and contact details of two referees; an original document providing confirmation of your degree (or a transcript if the degree is not yet awarded). For non-native English speakers, a certificate of competence in English is required at IELTS 6.5 or higher, with no element less than 6.0 (or equivalent).

Mark Batty's web page.

Programming Languages and Systems Group's web page.

Applications process web page.

The studentship covers UK/EU fees, a travel budget and a stipend for 3.5 years. There is an option to teach, but no requirement. Non-EU students are welcome to apply but are subject to higher fees and would need to find funding for the difference.

### Fully-funded 3-years Phd scolarship at Université d’Orléans, France

• Reactive Synchronous Programming : Semantics and applications to IOT
• Advisors : W. Bousdira, F. Dabrowski
• Research Team : LIFO/LMV
• Theme : Concurrency semantics

Laboratory
The Laboratory of Fundamental Computer Science of Orleans (LIFO, EA 4022) is a laboratory of the University of Orleans and INSA Center-Val de Loire. Research conducted at LIFO ranges from algorithmics to natural language processing, from automatic learning to massive parallel computing, from verification and certification to system security.

Team
The aim of the LMV team is to improve the understanding of safety and security of computer systems. From "partial order" logic to usual programming languages, the team members work on these questions at different levels of abstraction.

Funding : Fully-funded 3-years scholarship from the French Ministry for Education and Research

Subject : The reactive synchronous programming model [9] is a relaxation of the ESTEREL model [6]. In the latter, a collection of processes progress by successive phases of global synchronization (“ clock ticks ”) and communicate by events. At each instant (a phase between two ticks) each component reacts to the presence / absence of events. While the ESTEREL model solves the problem of causality posed by the instantaneous reaction to absence by restricting the expressivity of the language, the synchronous reactive model delays reaction to absence (the absence of a signal can not be decided before the end of an instant). Several works have focused on the semantic study of languages derived from this model [2, 5, 3] and on the analysis of the properties of such programs [4, 12]. Other works have successfully studied the possibility of using this programming model in the context of mobility [7]. Implementations of this programming model have been proposed for several languages like C, Scheme, Ocaml and Java [8, 13, 10, 11]. In [9], the authors propose a version of this model supporting strong security properties.

In this thesis, we will focus on a purely functional approach of the synchronous reactive model (existing languages have imperative features). As a first step, the selected candidate will have to carry out the semantic study of a programming language based on this model. An obvious starting point will be the article [1]. In a second step, the definition of desirable properties for the programs of this language will lead to the implementation of verification tools dedicated to these properties. The different developments will have to be formalized using the Coq proof assistant. Depending on the results obtained, the automatic extraction of code from the latter may be considered.

From an applied point of view the objective of this thesis is to propose a high-level programming language for the Internet Of Objects. In particular, such a language should make it possible to deploy a program, conceived in a global manner, on the different actors of a communicating scenario.

Application
We are happy to provide more details to potential applicants. Requests for additional information regarding the project’s content/motivation, other informal enquiries, and formal applications can be sent to Frédéric Dabrowski. Formal applications must include:

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

Deadline for applications: May 15th 2019.

References

1. M. Abadi and G. Plotkin. A model of cooperative threads. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’09, pages 29–40, New York, NY, USA, 2009. ACM.
2. R. M. Amadio. The sl synchronous language, revisited. The Journal of Logic and Algebraic Programming, 70(2):121 – 150, 2007. Algebraic Process Calculi: The First Twenty Five Years and Beyond.
3. R. M. Amadio. A synchronous pi-calculus. Inf. Comput., 205(9):1470–1490, 2007.
4. R. M. Amadio and F. Dabrowski. Feasible reactivity in a synchronous pi-calculus. In Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP ’07, pages 221–230, New York, NY, USA, 2007. ACM.
5. R. M. Amadio and M. Dogguy. On affine usages in signal-based communication. CoRR, abs/0804.1729, 2008.
6. G. Berry and G. Gonthier. The esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19(2):87 – 152, 1992.
7. G. Boudol. Ulm: A core programming model for global computing. In D. Schmidt, editor, Programming Languages and Systems, pages 234–248, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
8. F. Boussinot. Fairthreads: mixing cooperative and preemptive threads in c. Concurrency and Computation: Practice and Experience, 18:445–469, 2006.
9. F. Boussinot and F. Dabrowski. Safe Reactive Programming: the FunLoft Proposal. In MULTIPROG’08, pages –, Sweden, 2008.
10. F. Boussinot and J.-F. Susini. The sugarcubes tool box: A reactive java framework. Softw. Pract. Exper., 28(14):1531–1550, Dec. 1998.
11. L. Mandel and C. Pasteur. Réactivité des systèmes coopératifs : le cas de ReactiveML. In D. Pous and C. Tasson, editors, JFLA - Journées francophones des langages applicatifs, Aussois, France, Feb. 2013. Damien Pous and Christine Tasson.
12. A. A. Matos, G. Boudol, and I. Castellani. Typing noninterference for reactive programs. The Journal of Logic and Algebraic Programming, 72(2):124 – 156, 2007. Programming Language Interference and Dependence.
13. M. Serrano, F. Boussinot, and B. Serpette. Scheme fair threads. In Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP ’04, pages 203–214, New York, NY, USA, 2004. ACM.

### PhD position in Computer Science / Systems Biology, university of Lille, France

We are looking for a PhD student to work in the BioComputing group (University of Lille, France) on formal methods (especially inspired by logic and semantics of programming languages) for modeling and static analysis of biological systems. More precisely, the thesis entitled “Computational Models of Intestinal Glucose Absorption for Diabetes Prediction”, aims at developing new computational methods for the prediction of glucose intestinal absorption at the physiological and cellular level in order to improve the understanding of diabetes pathology. In addition of having a background in formal methods, we expect candidates interested in health sciences and biology. For more details, see here.

The thesis will be co-supervised by Cédric Lhoussaine and François Pattou (Professor of Surgery). The starting date will be September or October 2019. Potential candidates are encouraged to contact Cedric Lhoussaine as early as possible. The deadline for application is 1st of May.

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

The Department of Computer Science of the Università degli Studi di Verona in beautiful Verona, Italy, EU, has an opening for a postdoctoral researcher position in automated reasoning. The position is for one year, full-time on research (no teaching duties), flexible in terms of research topic, and with a competitive salary. Recent PhD graduates in Computer Science or related fields, scientists at the postdoc level who wish further experience towards a tenure-track position, or who need a bridge between positions, faculty on paid leave of absence for six months who wish to extend it to twelve, and active in any topic in automated reasoning, are invited to get in touch by e-mail with Maria Paola Bonacina. Applications will be considered as soon as received. An official application with the University will have to be filed in the window between April 26 - May 16.

### UNSW Sydney Seeking PhD Students

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 scholarships to multiple motivated PhD students who want 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 PhD 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 bachelor degree (minimum 4 years) or a bachelor and a masters degree in Computer Science, Mathematics, or similar.

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

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

• in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, Coq, or Agda, and/or
• with programming languages and verified or certifying compilers, and or
• in verified applications technology such as CakeML
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, email us a copy of your CV, cover letter, transcripts, and contact information for two referees.

This round of applications closes on the 19th of April 2019.

The seL4 code and proof, and the Cogent project, are open source.

Still studying? We also have internship opportunities!

### PhD Position on SMT for Security Analysis at Uppsala University

The Department of Information Technology, Uppsala University, opens a fully paid PhD student position in Computer Science, on SMT Reasoning for Security Analysis. The main advisor of the PhD student will be Philipp Rümmer. The topic of the PhD position is (i) to develop and extend SMT technology tailored to security analysis, in particular methods and tools for relevant theories such as strings, fragments of word equations, and regular expression constraints, and to (ii) investigate and improve SMT-based methods for security analysis, possibly including approaches like whitebox fuzzing, model checking, symbolic execution, and variants of taint tracking.

About the project: The funding for the PhD position is part of the ambitious framework project WebSec: Securing Web-driven Systems, funded by the Swedish Foundation for Strategic Research (SSF) and dedicated to principled security and privacy for the web. The project is a collaboration between Chalmers in Gothenburg (project leader: Andrei Sabelfeld) and Uppsala University (PI: Philipp Rümmer), and the PhD student will have the opportunity to work together with several world-leading groups at both universities: the Embedded Systems, Algorithmic Program Verification, and Optimization group in Uppsala, and the Information Security group at Chalmers. Information about WebSec is given here.

Requirements: The candidate should have a Master of Science in computer science, computer engineering, or equivalent, with a solid grasp in SMT or constraint solving, security, formal methods, and language technology such as compiler construction. Good programming skills and communication skills are required in this project. We expect the student to have demonstrated ability to do research, as seen through his/her MS thesis. Excellent skills in spoken and written English are an absolute requirement.

For more details and instructions on how to apply see the position description. More information on what support you can expect is given on this web page.

### Researcher positions (postdoc) within the ERC Consolidator grant “Certified Quantum Security”

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

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

The ideal candidate would have experience in:

• Semantics
• Theorem proving
• Verification of classical cryptography
• Quantum cryptography
• Quantum computation / communication
Of course, expertise in all those areas is very rare, so candidates who are strong in some of those areas and are interested in the others are encouraged to apply!

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

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

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

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

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

### Post-doctoral position, Inria Nancy - Grand Est

A post-doctoral position is available in the Caramba team at Inria Nancy - Grand Est.

The goal of this project is to formally prove algorithms and code used by the GNU MPFR library.

Candidates should have a strong background in formal proof and in the C programming language.

Applications should be submitted before June 6 here.

Sophie Tourret