Association for Automated Reasoning

Newsletter No. 133
December 2020

On the future of the AAR

Ulrich Furbach, AAR vice-president

Dear member of the Association for Automated Reasoning,

As Vice-president of AAR I have to assume the duties of the President (http://aarinc.org//bylaws) following the passing of our President Larry Wos. Together with the current board members we started a discussion on how to proceed with AAR.

The situation is as follows: AAR currently has 1316 members and funds of $2,889.37 which are on a bank account of CADE Inc. and earmarked for AAR. AAR is no formal or registered association and it has no regular income, because the membership fees are waived. The only activity worth mentioning at present is the publication of the newsletter. This is very successful (thanks to Sophie Tourret) and certainly should be continued.

Currently the board members together with the CADE trustees and the IJCAR Steering Committee are discussing to what extent AAR could act as an umbrella organisation for other conferences. There is a large number of conferences and workshops related to automated reasoning and some of them already expressed their interest in having such an umbrella.

This discussion is ongoing and I suggest postponing necessary new elections to the board of AAR until we have a clear view on how to proceed. It goes without saying that I will keep you up to date about all this.

Best regards

Herbrand Award 2021: 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

A nomination is required for consideration for the Herbrand Award. Nominations can be submitted at any time. The deadline for nominations to be considered for the Herbrand Award 2021, which will be given at CADE-28, is

April 30 2021
Nominations pending from previous years must be resubmitted in order to be considered.

For more details, please check the Herbrand Award webpage.

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 via e-mail to

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

ETAPS Doctoral Dissertation Award - Call for Nominations

The European Joint Conferences on Theory and Practice of Software Association has established a Doctoral Dissertation Award to promote and recognize outstanding dissertations in the research areas covered by the four main ETAPS conferences (ESOP, FASE, FoSSaCS, and TACAS).

Doctoral dissertations are evaluated with respect to originality, relevance, and impact to the field, as well as the quality of writing. The award winner will receive a monetary prize and will be recognized at the ETAPS Banquet.

Eligibility
Eligible for the award is any PhD student whose doctoral dissertation is in the scope of the ETAPS conferences and who completed their doctoral degree at a European academic institution in the period from January 1st, 2020 to December 31st, 2020.

Nominations
Award candidates should be nominated by their supervisor. Members of the Award Committee are not allowed to nominate their own PhD students for the award.

Nominations consist of a single PDF file (extension .pdf) containing:

All documents must be written in English. Nominations are welcome regardless of whether results that are part of the dissertation have been published at ETAPS.

Nominations should be submitted via EasyChair.

The deadline for nominations is January 17th, 2021.

Award Committee

Contact
All questions about submissions should be emailed to the chair of the award committee, Caterina Urban.

Conferences

CADE-28: The 28th International Conference on Automated Deduction, call for Papers

July 11-16, 2021, Pittsburgh, USA
in cooperation with ACM SIGLOG

CADE will carefully monitor the development of the COVID-19 pandemic, and take guidance from from the health authorities, to determine whether CADE-28 will be physical or online.

CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond STEM, implementations, and the use/contribution of automated deduction in AI, are solicited. CADE-28 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction.

Important Dates (Conference)

The full call for papers, including submission informations, is available on easychair

More information is available on the conference's web page, and on the online CfP.

ITP2021: 12th International Conference Interactive Theorem Proving, call for papers and workshops

June 29-July 1, 2021, Rome, Italy
co-located with LICS and ICTCS

ITP will carefully monitor the development of the COVID-19 pandemic, and take guidance from the health authorities, to determine whether ITP21 will be held physically, virtually or in a hybrid manner.

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.

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:

Important Dates

Call for workshops
Researchers and practitioners are invited to submit proposals for co-located workshops on topics relating to interactive theorem proving. Workshops can target the ITP community in general, focus on a particular ITP system, or highlight more specific issues or recent developments. Proposals for in-depth tutorials or tool introductions are also welcome.

Co-located events will take place on 28 June and 2 July and will be held on the same premises as the main conference. In case of needs, we are ready to discuss and try to accommodate requests for two-day workshops. Conference facilities are offered free of charge to one of the organizers and one of the invited speakers. Workshop-only attendees will enjoy a significantly reduced registration fee.

Detailed organizational matters such as paper submission and review process, or publication of proceedings, are up to the organizers of individual workshops. All accepted workshops will be expected to have their program ready by 4 June, 2021.

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

Proposals should be submitted by email, no later than 11 January, 2021. Selected workshops will be notified by 15 January, 2021.

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

CiE 2021: Computability in Europe 2021, Connecting with Computability, call for papers

July 5 - 9, 2021, virtual

Due to the current pandemic CiE 2021 will be held as a virtual conference.

CiE 2021 is the seventeenth conference organized by the Association Computability in Europe. The Computability in Europe conference (CiE) series has built up a strong tradition for developing a scientific program which is interdisciplinary at its core bringing together all aspects of computability and foundations of computer science, as well as the interplay of these theoretical areas with practical issues in CS and other disciplines such as biology, mathematics, history, philosophy, and physics. For more information about the CiE conferences and the Association CiE, please have a look here.

CiE 2021 will be the second CiE conference that is organized as a virtual event and aims at a high-quality meeting that allows and invites active participation from all participants. It will be hosted virtually by Ghent University.

Women in Computability
The Computability in Europe conference series has a long tradition in setting up a Women in Computability program. For CiE 2021 we plan a Women in Computability workshop combined with an online mentoring program. For more details on the Special Interest Group Women in Computability, see here.

Important Dates

The notifications of acceptance for informal presentations will be sent a few days after submission.

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

ICFCA 2021: 16th International Conference on Formal Concept Analysis , call for papers

June 29 - July 2, 2021, Strasbourg, France

Formal Concept Analysis emerged in the 1980's from attempts to restructure lattice theory in order to promote better communication between lattice theorists and potential users of lattice theory. Since its early years, Formal Concept Analysis has developed into a research field in its own right with a thriving theoretical community and a rapidly expanding range of applications in information and knowledge processing including visualization, data analysis (mining) and knowledge management and discovery.

The ICFCA conference series aims at bringing together researchers and practitioners working on theoretical or applied aspects of Formal Concept Analysis within major related areas such as Mathematics and Computer and Information Sciences and their diverse applications to fields like Software Engineering, Linguistics, Life and Social Sciences, etc.

Topics Main topics of interest include, but are not limited to:

Important Dates

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

LICS 2021: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, call for papers

June/July 2021, Rome (to confirm), Italy
co-located with ITP and ICTCS

The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric.

Suggested, but not exclusive, topics of interest include: 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, knowledge representation and reasoning, lambda and combinatory calculi, linear logic, logic programming, logical aspects of AI, 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.

Covid-19
The organizers are carefully monitoring the development of the COVID-19 pandemic, and take guidance from the health authorities, to determine whether LICS 2021 will be held physically, virtually or in a hybrid manner.

Important Dates
Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by anywhere on earth (AoE).

Deadlines are firm; late submissions will not be considered.

All submissions will be electronic via easychair.

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

COORDINATION 2021: 23rd International Conference on Coordination Models and Languages, call for papers

June 14-18, Malta

Modern information systems rely increasingly on combining concurrent, distributed, mobile, adaptive, reconfigurable and heterogeneous components. New models, architectures, languages and verification techniques are necessary to cope with the complexity induced by the demands of today’s software development. Coordination languages have emerged as a successful approach, in that they provide abstractions that cleanly separate behaviour from communication, therefore increasing modularity, simplifying reasoning, and ultimately enhancing software development. Building on the success of the previous editions, this conference provides a well-established forum for the growing community of researchers interested in models, languages, architectures, and implementation techniques for coordination.

Topics of Interest

Deadlines

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

ICALP 2021: 48th International Colloquium on Automata, Languages, and Programming, call for papers

July 13-16, 2021, Glasgow, Scotland, UK

ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). As usual, ICALP will be preceded by a series of workshops, which will take place on 12 July 2021.

COVID-19: We will monitor the global travel situation and consider whether the conference will be physical, virtual or hybrid. If there is a physical component, remote participation for both speakers and attendees will also be an option.

Topics
Papers presenting original research on all aspects of theoretical computer science are sought. Typical but not exclusive topics of interest are:

Track A: Algorithms, Complexity and Games

Track B: Automata, Logic, Semantics, and Theory of Programming

Important dates

Deadlines are firm; late submissions will not be considered.

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

FSCD 2021: 6th International Conference on Formal Structures for Computation and Deduction, call for papers

July 17 - July 24, 2021, Buenos Aires, Argentina
In-cooperation with ACM SIGLOG and SIGPLAN

Due to the Covid 19 pandemic situation, the 2021 edition of FSCD and its satellite workshops will be held online.

FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation, semantics and verification in new challenging areas.

The suggested, but not exclusive, list of topics for submission is:

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

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

SPIN 2021: 27th International Symposium on Model Checking of Software, call for papers

July 14-15, 2021, Aarhus, Denmark

The 27th 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 the analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms (classical and quantum), tool development, including for modern hardware (parallel and distributed), and empirical evaluation.

Topics of interest include, but are not limited to:

Important Dates

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

DLT 2021: 25th International Conference on Developments in Language Theory, call for papers

August 16-20, 2021, Porto, Portugal

DLT is an International Conference Series under the auspices of the European Association for Theoretical Computer Science (EATCS). The purpose of this conference is to bring together members of the academic, research, and industrial community who have an interest in formal languages, automata theory, and related areas.

COVID-19: We will monitor the global travel situation and consider the conditions the conference will be held.

Topics
Typical topics include, but are not limited to

Important Dates

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

Workshops

FORMALISE 2021: 9th International Conference on Formal Methods in Software Engineering

May 23-24, Madrid, Spain,
co-located with ICSE 2021

The software industry needs tools and methods to deliver high-quality software. Much progress has been achieved from the early days of software development; still, nowadays, even considering the state of the art of the technologies used, the success of software projects is often not guaranteed. Many of the approaches used for developing large, complex software systems are still not able to ensure the correct behavior — and the general quality — of the delivered product, despite the efforts of the (often very qualified and skilled) software engineers involved. This is where formal methods can play a significant role. Indeed, they have been developed to provide the means for greater precision and thoroughness in modeling, reasoning about, validating, and documenting the various aspects of software systems during their development. When carefully applied, formal methods can aid all aspects of software creation: user requirement formulation, design, implementation, verification/testing, and the creation of documentation.

After decades of research though, and despite significant advancement, formal methods are still not widely used in industrial software development. We believe that closer integration of formal methods in software engineering can help increase the quality of software applications, and at the same time highlight the benefits of formal methods in terms also of the generated return on investment (ROI).

The main objective of the conference is to foster the integration between the formal methods and the software engineering communities, to strengthen the — still too weak — links between them, and to stimulate researchers to share ideas, techniques, and results, with the ultimate goal to propose novel solutions to the fraught problem of improving the quality of software systems.

Topics of interest
Areas of interest include but are not limited to:

Important dates

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

F-IDE 2021: 6th Workshop on Formal Integrated Development Environment

May 24-28, 2021 -- held online
Affiliated with NASA Formal Methods 2021

High levels of safety, security, and 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 and/or an 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.

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

Important Dates

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

LAMAS & SR 2021: International Workshop on Logical Aspects of Multi-Agent Systems and Strategic Reasoning, call for papers

May 3 or 4 (TBA), 2021, London, United Kingdom,
Satellite workshop of AAMAS 2021,

Logics and strategic reasoning play a central role in multi-agent systems. Logics can be used, for instance, to express the agents' abilities, knowledge, and objectives. Strategic reasoning refers to algorithmic methods that allow for developing good behavior for the agents of the system. At the intersection, we find logics that can express existence of strategies or equilibria, and can be used to reason about them.

The LAMAS&SR workshop merges two international workshops: LAMAS, which focuses on all kinds of logical aspects of multi-agent systems from the perspectives of artificial intelligence, computer science, and game theory, and SR, devoted to all aspects of strategic reasoning in formal methods and artificial intelligence.

Over the years the communities and research themes of both workshops got closer and closer. LAMAS&SR unifies LAMAS and SR under the same flag, formally joining the two communities in order to expose each of them to a wider range of work relevant to their research.

LAMAS&SR is thus interested in all topics related to logics and strategic reasoning in multi-agent systems, from theoretical foundations to algorithmic methods and implemented tools.

The topics of the workshop include, but are not limited to:

IMPORTANT DATES: Paper submission: 10 Feb, 2021 (AoE) Author Notification: 10 March, 2021 Camera Ready: 24 March, 2021 Workshop: May 3 or 4, 2021 (TBA)

Please visit the website for further details.

Lean Together 2021, Call for Participation

January 4-7, 2021, online

At this meeting we discuss ongoing projects in formalized mathematics and software verification, as well as infrastructure and outreach for Lean and its community. We welcome speakers and participants from other proof assistant communities, as well as people who are inexperienced with proof assistants but want to learn more.

More detailed scheduling information will appear on the website soon. We hope that you'll save the dates and attend some or all of the sessions!

Check out the website and if you have any questions please contact the organizers:

Journal Special Issues

CCC: Continuity, Computability, Constructivity, From Logic to Algorithms 2019 & 2020, LMCS Special Issue, call for submissions

After two years of successful work in the EU-MSCA-RISE project "Computing with Infinite Data" (CID) and two excellent Workshops CCC 2019 in Ljubljana (Slovenia) and CCC 2020 ( online), we are planning to publish a collection of papers dedicated to the meetings, to the project and to the subject in general as a Special Issue in the open-access journal Logical Methods in Computer Science.

Topics
The issue should reflect progress made in Computable Analysis and related areas, and is not restricted to work in the CID project or presented at the Workshop. Submissions are welcome from all scientists on topics in the entire spectrum from logic to algorithms including, but not limited to: Exact real number computation, Correctness of algorithms on infinite data, Computable analysis, Complexity of real numbers, real-valued functions, etc. Effective descriptive set theory, Constructive topological foundations, Scott's domain theory, Constructive analysis, Category-theoretic approaches to computation on infinite data, Weihrauch degrees, Randomness and computable measure theory, Other related areas.

Important Dates

If you intend to submit a paper for the special issue, please inform us by sending an email to Daniel Graça or Alex Simpson by 31 January 2021. You will then receive concrete submission instructions about how to submit your paper to this special issue. Please prepare your manuscript using the LMCS LaTeX style which can be downloaded here. Submissions will be reviewed according to the usual high standards of LMCS.

Annals of Mathematics and Artificial Intelligence: Special Issue on Theoretical and Practical Aspects of Unification, call for submissions

In 2020, Annals of Mathematics and Artificial Intelligence (AMAI) celebrates its 30th anniversary. Over the years, the journal has promoted better understanding of the application of quantitative, combinatorial, logical, algebraic and algorithmic methods to artificial intelligence areas as diverse as decision support, automated deduction, reasoning, knowledge-based systems, machine learning, computer vision, robotics and planning. AMAI special issues are intended to be collections of original research papers reflecting the intersection of mathematics and a focussed discipline demonstrating how each has contributed greatly to the other. A further goal of the journal is to close the gaps between the fields even further. Papers should report on current research in the appropriate areas, as well as more retrospective papers in which progress has been ongoing over a period of time.

The purpose of this special issue of AMAI is to promote research on theoretical and practical aspects of unification. 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. The special issue is related to the topics of the 34th International Workshop on Unification - UNIF 2020. Participants of the workshop, as well as other authors are invited to submit contributions.

Examples of Topics
This special issue focuses on advanced results on the topics of unification in a broad sense, which include, but are not limited to, the following:

Submission
This special issue welcomes original high-quality contributions that have been neither published in nor simultaneously submitted to any journals or refereed conferences. Submissions will be peer-reviewed using the standard refereeing procedure of the Annals of Mathematics and Artificial Intelligence.

Submitted papers must be in English, prepared in LaTeX according to the guidelines of the journal.

PDF versions of papers should be uploaded at the submission page by January 31, 2021.

Please choose S704 - Unification - UNIF 2020 when you will be selecting the article type.

Guest Editors

Further Information

Special issue on Conceptual Structures 2020, Annals of Mathematics and Artificial Intelligence, call for papers

This Special Issue grew out of the International Conference on Conceptual Structures "Ontologies and Concepts in Mind and Machine" (ICCS 2020) and focuses on the formal analysis and representation of conceptual knowledge, at the crossroads of artificial intelligence, human cognition, computational linguistics, and related areas of computer science and cognitive science. Recently, graph-based knowledge representation and reasoning (KRR) paradigms are getting more and more attention. With the rise of quasi-autonomous AI, graph-based representations provide a vehicle for making machine cognition explicit to its human users. Conversely, graphical and graph-based models can provide a rigorous way of expressing intuitive notions in computable frameworks. The aim of the ICCS 2020 conference is to build upon its long-standing expertise in graph-based KRR and focus on providing modeling, formal, and application results of graph-based systems. The Special Issue welcomes contributions from a modeling, application, and theoretical viewpoint.

Topics include but are not limited to:

Deadline for paper submission: March 31, 2021

Please visit the website for further details.

Open Positions

Tenure Track Assistant/Associate Professor of Computer Science, Lewisburg, Pensilvania, USA

The Department of Computer Science at Bucknell University seeks applications for a tenure-track position at the rank of Assistant Professor or Associate Professor in Computer Science beginning August 2021. We seek applicants who demonstrate interest in reflective, multicultural, and inclusive teaching practices and who commit to collaborating with departmental colleagues and students. The successful candidate will teach in one or more areas of our core CS curriculum and will have opportunities to develop elective courses in their areas of expertise.

See the full details here.

Research position in Formal Verification (m/f/x) at HENSOLDT Cyber in Munich

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

We are buidling up a new research team, which is working on cutting-edge projects targeting the aspects formal verification, operating system design and cryptography with the focus on secure embedded systems. If you have a strong interest and/or background in secure operating system development, we would like to get in touch with you.

Tasks

Requirements

We are not only offering flexible and mobile working, but the opportunity to be involved in the development of cutting-edge security products in an international and innovative environment.

Did we spark your interest? Then we are looking forward to your application. If you have any questions on the vacancy please don't hesitate to contact us via mail.

Apply directly through the website.

Faculty position at Portland State University, USA

Candidates in the areas of programming languages or formal methods are enthusiastically encouraged to apply for the following position.

Assistant Professor of Computer Science

The Department of Computer Science at Portland State University invites applications for several Assistant Professor positions. Exceptional candidates will also be considered for appointment at the rank of Associate Professor.

Candidates in all areas of Computer Science will be considered, with a preference for applicants who will enhance or complement our existing areas of research expertise and/or whose work is aligned with the strategic visions of the department or the Maseeh College. The expected start date for these positions is September 2021, but earlier or later dates can be negotiated.

Please see here for further information on applying.

Assistant/associate professor positions at Aarhus University, Denmark

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

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

The application deadline is January 11th 2021.

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

2+ postdoc and 4+ Ph.D. positions in formal methods and control theory for AI-intensive cyber-physical systems in Kyoto or Tokyo, Japan

We are seeking 2+ postdoc researchers and 4+ Ph.D. candidates who collaborate with us in the project “CyPhAI: Formal Analysis and Design of AI-intensive Cyber-Physical Systems” funded by JST. The detail of the call can be found here.

This project aims at establishing mathematically-solid methodologies to model, verify, test, monitor, and control a cyber-physical system in which AI plays a crucial role (AI-CPS). Successful candidates will work with Kohei Suenaga (Kyoto University, Kyoto, Japan) or Masako Kishida (National Institute of Informatics, Tokyo, Japan) on this project. The contract will initially run until the end of March 2021, with the possibility of annual renewal at maximum 5 years.

Although this call is for members working in Japan, this project is a joint project with a team in France led by Thao Dang (CNRS). We will be working in tight collaboration with our colleagues in France.

The main research topic of Suenaga’s team will be learning for AI-CPS and verification of AI-CPS. The expected research topic includes (but is not limited to) the following:

  1. application of machine learning to synthesize the design of AI-CPS,
  2. efficient machine learning for AI components in AI-CPS, and
  3. (quantitative/statistical) model checking for AI-CPS.

The main research topic of Kishida’s team will be the control theory and method for AI-CPS. The expected research topic includes (but is not limited to) the following:

  1. application of machine learning for designing a controller and
  2. control for machine-learned components.

postdoctoral position at VERIMAG (Grenoble, France)

VERIMAG (public joint laboratory of CNRS and University of Grenoble Alpes) is seeking excellent candidates for a postdoctoral position on logical foundations and verification of distributed systems. The ideal candidate will have a PhD degree in Computer Science in one of the following areas:

The successful candidate will integrate the MOHYTOS group. The position is for one year with possibility of extension.

To apply send your CV, list of publications and references (letters of recommendation) to Radu Iosif.

PhD positions available, Imperial College London, UK

Prof. Philippa Gardner is looking for one or two PhD students, start date in October 2021, to join her Verified Software research group. A summary of possible research projects is given below.

The deadlines to apply for a PhD position in the Department are 8th January 2021 and 19th March 2021. The Department advises all students requiring funding to apply by the January deadline, although there may still be some funding available for applications received after January. Further details can be found here. A successful UK student will probably be funded through the standard Departmental competition for funds. A successful EU/overseas student will probably be funded by a combination of Departmental funding and my funding. In particular, I have additional funding which means that the EU/overseas students are able to go into the same competition for funding as the UK students.

Please do not hesitate to contact her directly by email if interested, cc’ing her administrator Teresa Carbajo Garcia.

Research in the Verified Software Group, Imperial
Philippa's group is involved with a wide range of theoretical and practical projects on symbolic testing and verification in particular, and on formal methods in general. They are summarised below. All have many opportunities for PhD projects.

Gillian: a multi-language platform for compositional symbolic analysis
The Verified Software Group has recently introduced Gillian [1], a multi-language platform for compositional symbolic analysis. It currently supports three flavours of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It is underpinned by a core symbolic execution engine, parametric on the memory model of the target language, with strong mathematical foundations that unifies symbolic testing and verification. Gillian has been instantiated to C and JavaScript, obtaining results on real-world code that demonstrate the viability of our unified, parametric approach.

Possible projects include: incorporating ideas from incorrectness separation logic to Gillian [2]; extending Gillian with events and concurrency [3]; underpinning Gillian with Coq certification; instantiating Gillian with C (we have just started, [1]) and Rust (we have hardly begun); and using the Gillian instantiations for symbolic testing and verification of real-world programs.

Concurrency
The Verified Software Group has worked on compositional reasoning about concurrent programs, introducing fundamental techniques underpinning modern concurrent separation logics [4]: logical abstraction; logical atomicity; and logical environment liveness properties. We have applied our reasoning to verify some of the most advanced concurrent algorithms.

There is still much to understand: for example, working with the fundamental theory; applying the work to real-world libraries; developing prototype analysis tools; or moving to the Coq-focused Iris project, whose foundations use some of our theory.

Distribution
The Verified Software Group has recently begun to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions [5].

We would be interested in finding someone to work in this area: for example, developing further the operational semantics and providing prototype tools to prove robustness results and discover litmus tests; or creating a program logic for distributed atomic transactions (our original motivation for the work) inspired by our previous work on program logics for concurrency.

References

  1. Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, PLDI'2020. Part 2 on verification and bi-abduction is being written now! We are giving a talk on Gillian at the conference Rebase, associated with ECOOP and OOPSLA, on 16th and 17th November, and at Facebook's Testing and Verification Symposium (FaceTAV), in December 2020.
  2. Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad (Imperial), Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and Jules Villard, CAV'20.
  3. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications, Gabriela Sampaio, Jose Fragoso Santos, Petar Maksimovic and Philippa Gardner, ECOOP'20
  4. A Perspective on Specifying and Verifying Concurrent Modules, Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner, Journal of Logical and Algebraic Methods in Programming, 2018
  5. Data Consistency in Transactional Storage Systems: a Centralised Approach, Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20

Post-doctoral positions, Imperial College London, UK

Prof. Philippa Gardner has openings for two post-doctoral research positions in her Verified Software research group at Imperial on `Gillian: Program Correctness and Incorrectness', funded by Facebook, and `Gillian: Coq-Certified Compositional Symbolic Analysis', funded by a national fellowship. Details of these projects are given below.

These positions are for three years. The start date is flexible in these uncertain times, up to September 2021. It is possible to start the positions remotely, although we are able to meet at Imperial when necessary so it might make sense to be in London. In fact, accommodation rents are currently very good (due to covid) so it is actually quite a good time to come to London.

If you are interested, please do not hesitate to contact her.

Gillian: Program Correctness and Incorrectness
We have introduced Gillian [1], a multi-language platform for compositional symbolic analysis. It supports three flavours of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It is underpinned by a core symbolic execution engine, parametric on the memory model of the target language, with strong mathematical foundations that unifies symbolic testing and verification. Gillian has been instantiated to the real-world languages C and JavaScript, obtaining results on real-world code that demonstrate the viability of our unified, parametric approach.

Meanwhile, O’Hearn [2] has observed that program correctness for describing the absence of bugs and program incorrectness for describing the presence of bugs are two sides of the same coin. He, Azalea Raad (Imperial) and others [3] have recently introduced incorrectness separation logic for reasoning about program incorrectness, in contrast with Hoare logic and separation logic for reasoning about program correctness. The underlying theory of Gillian resonates with the fundamental ideas of incorrectness logic, suggesting that Gillian has an unexplored potential for reasoning about both program correctness and incorrectness.

Our goal is to establish Gillian as a leading academic platform for integrated analysis of program correctness and incorrectness, by advancing the development of its existing analyses and incorporating the new ideas arising from incorrectness logic. This research position is for three years. It would suit someone with a strong background in formal methods (theory and/or practice), especially someone with experience in program analysis, testing or verification. It is funded by Facebook.

References

  1. Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, PLDI'2020. Part 2 on verification and bi-abduction is being written now! We are giving a talk on Gillian at the conference Rebase, associated with ECOOP and OOPSLA, on 16th and 17th November, and at the Facebook Testing and Verification Symposium in December, 2020.
  2. Incorrectness Logic, Peter O'Hearn, POPL'20.
  3. Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and Jules Villard, CAV'20.

Gillian: Coq-Certifiction of Compositional Symbolic Analysis
We have introduced Gillian [1], a multi-language platform for compositional symbolic analysis. It supports three flavours of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. Gillian has been instantiated to the real-world languages C (using the Coq-verified CompCert compiler) and JavaScript (using our own compiler), obtaining results on real-world code that demonstrate the viability of our unified, parametric approach.

The goal is to provide Coq-certification for the Gillian platform. Gillian is underpinned by a core symbolic execution engine, parametrised by the memory model of the target language, with strong mathematical foundations that unifies symbolic testing and verification. This core is ripe for Coq mechanisation since it has a general correctness result that depends on lemmas associated with particular Gillian instantiations. The challenge is to understand how to link this Coq mechanisation of the core engine to the Gillian platform: either by replacing the Gillian implementation with extracted Coq code; or by using Gillian to generate proof terms that can be certified by Coq in order to retain the Gillian optimisations.

This position is for three years, funded by Gardner's UKRI national fellowship. It would suit someone with strong experience with the Coq theorem prover, to enhance the current Coq expertise in the group. In particular, my PhD student Rao Xlaojia is part of the Imperial and Cambridge team doing WasmCert, a Coq-specification of Wasm [2]. There is also an opportunity to get involved with this WasmCert project if interested.

References

  1. Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, PLDI'2020. Part 2 on verification and bi-abduction is being written now! We are giving a talk on Gillian at the conference Rebase, associated with ECOOP and OOPSLA, on 16th and 17th November, and at the Facebook Testing and Verification Symposium in December, 2020.
  2. WasmCert-Coq, M. Bodin, P. Gardner, J. Pichon, C. Watt and R. Xiaojia.

Professor of Symbolic Computation, Linz, Austria

The Johannes Kepler University Linz is announcing the position of a professor of symbolic computation assigned to the Research Institute for Symbolic Computation (RISC), and to begin on October 1, 2021.

Deadline for applications: December 30, 2020.

For further details of the application call see here.

In case of questions concerning the position, do not hesitate to contact Peter Paule.

PhD Positions at Aarhus University on Algorithmic Verification & Programming Languages

The Department of Computer Science at Aarhus University, Denmark, offers several fully funded PhD positions in the areas of Algorithmic Verification & Programming Languages. The department has a strong presence in the areas of formal methods and programming languages and we are looking for talented students to work in the area.

Interested applicants are encouraged to contact the respective faculty for details.

Next deadline: Feb 1st, 2021.

Refer here for more information.

Fully funded PhD position at University of Sheffield on the formal verification of industrial robots

Andrei Poposcu is advertising a PhD position at University of Sheffield that can lead to high-impact work using a proof assistant. The PhD project is titled "Formal Specification and Verification of the Safe Interaction between Humans and Industrial Robots" and will be supervised by him and some experts in industrial robots from Sheffield's Advanced Manufacturing Research Centre (AMRC).

The position is for 42 months, is fully funded from EPSRC, and has no teaching obligations attached. The two constraints are that it is restricted to UK and EU students only, and has to start by 8 February 2021. Taking into account the Covid-19 pandemic, there may be the opportunity to start the PhD remotely and arrive in Sheffield at a later time, when it is safe to travel.

More details are shown here.

Andrei Popescu is also happy to answer any questions by email.

Tenure-track assistant professor in Systems Level Security at University of Copenhagen, Denmark

University of Copenhagen invites applications for a tenure-track assistant professorship in Systems Level Security.

The researcher will be part of the newly formed Security and Privacy Group spanning several research sections at the department. People working at the intersection of systems-level security and formal aspects of computer science (e.g., verification, type systems, programming languages, language-based security, formal methods and logic,) are encouraged to apply. Relevant research areas include hardware-assisted security, OS and hypervisor-level security, secure compilation, security aspects of IoT, cryptographic engineering, security engineering.

The full announcement is available here.

Deadline: Sunday 10 January 2021.

For further information contact Professor Jakob Grue Simonsen, or Head of Department: Professor Mads Nielsen. I can also provide information about the position.

Postdoctoral position in combinatorial optimization (including SAT solving and constraint programming) at University of Copenhagen

The Department of Computer Science (DIKU) at the University of Copenhagen invites applications for postdoctoral positions in combinatorial optimization.

The postdoc will be working in the Mathematical Insights into Algorithms for Optimization (MIAO) group headed by Jakob Nordstrom, which is doing research on theoretical analysis of and applied algorithm development for combinatorial optimization paradigms such as SAT solving, pseudo-Boolean optimization, constraint programming, and integer linear programming. MIAO belongs to the Algorithms and Complexity Section at DIKU, one of the leading groups in theoretical computer science in Europe, which is part of an exciting environment including the Basic Algorithms Research Copenhagen (BARC) centre, joint with the IT University of Copenhagen, and extensive collaborations with the Technical University of Denmark (DTU) and Lund University on the Swedish side of the Oresund Bridge, as well as with our many visitors. We aim to attract top talent from around the world to an ambitious, creative, collaborative, and fun environment. Using the power of mathematics, we strive to create fundamental breakthroughs in algorithms and complexity theory, but we also have a track record of start-ups and surprising algorithmic discoveries leading to major industrial applications.

The University of Copenhagen was founded in 1479 and is the oldest and largest university in Denmark. It is often ranked as the best university in Scandinavia and consistently as one of the top places in Europe. Within computer science, it is currently number 1 in the European Union (post-Brexit) according to the Shanghai Ranking.

This is a full-time employed position. The intended starting date is September 2021 but is negotiable, and the intended duration is 2 years. The University of Copenhagen is currently expanding strongly in computer science. We expect to keep having tenure-track openings in computer science in the coming years, and welcome postdoctoral researchers interested in exploring such opportunities.

The application deadline is January 24, 2021. See here for the full announcement with more information and instructions for how to apply. Informal enquiries are welcome and may be sent to Jakob Nordstrom.

PhD positions in theoretical computer science and/or combinatorial optimization at University of Copenhagen

The Department of Computer Science (DIKU) at the University of Copenhagen invites applications for PhD positions in theoretical computer science and/or combinatorial optimization.

The PhD students will be working in the Algorithms and Complexity Section at DIKU. This is one of the leading research groups in theoretical computer science in Europe, with a strong presence at top-tier conferences like STOC, FOCS, and SODA, and also with publications in premier AI conferences like AAAI, IJCAI, and NeurIPS. We are part of an exciting environment including the Basic Algorithms Research Copenhagen (BARC) centre, joint with the IT University of Copenhagen, and have extensive collaborations with the Technical University of Denmark (DTU) and Lund University on the Swedish side of the Oresund Bridge, as well as with our many visitors. We aim to attract top talent from around the world to an ambitious, creative, collaborative, and fun environment. Using the power of mathematics, we strive to create fundamental breakthroughs in algorithms and complexity theory, but we also have a track record of start-ups and surprising algorithmic discoveries leading to major industrial applications.

These PhD positions are full-time employed positions for a period of 3-5 years, depending on the education level of the candidate, and include an extended stay at some research institution abroad. The tentative starting date is September 2021, but this is negotiable.

The application deadline is January 24, 2021. See here for the full announcement with more information and instructions for how to apply. Informal enquiries are welcome and may be sent to Jakob Nordström, Rasmus Pagh, or Mikkel Thorup.

Funded MSc, PhD and postdoc positions in Program Reasoning and Verification at The University of British Columbia (Vancouver)

Alex Summers has a number of positions available on research topics connected with program correctness and (deductive) verification techniques and tools; these topics touch on programming language design and semantics, formal proof systems, logic and SMT solving in various combinations. Three representative topics are:

  1. A large ongoing effort to build verification support for the Rust language: the Prusti project.
  2. Formalising, explaining and debugging logical encodings suitable for automated SMT solving.
  3. Static analysis techniques for inferring formal specifications for partially-specified programs.

He plans to hire a combination of MSc and PhD students, for a start in September 2021; he may also hire up to one excellent postdoc candidate for a similar timeframe. MSc students at UBC perform research (and sometimes teaching) throughout their studies, and are paid a stipend in return; PhD student positions are also fully funded.

For both MSc and PhD students, the application process is to the department directly (naming one or more potential supervisors is encouraged), and the deadline for this year is December 15th. Details of the programmes and application process can be found here for MSc and here for PhD.

In case you have any questions or would like more information about my research, you can check out Alex Summers' webpage and you are welcome to email him.

Postdoc and PhD Positions @ Iowa State University, USA

Multiple fully-funded PhD positions and Postdoc positions are available in the Lab for Temporal Logic, which spans the Departments of Computer Science, Electrical and Computer Engineering, Aerospace Engineering, Mathematics, and the Virtual Reality Application Center. Application links are below.

About the Lab:
The Laboratory for Temporal Logic focuses on foundational advances to formal methods that carry through to really fly. The lab has developed techniques to enable better system specification and model-checking algorithms that scale to verify large, complex systems including NASA's automated air traffic control system and industrial verification problems at IBM. The lab's R2U2 verification engine is the only flight-certifiable RV tool capable of embedding in tight spaces post-deployment for real-time anomaly detection and mitigation triggering. R2U2 has flown on UAS, checked ATC ground stations, launched on rockets and small satellites, and embedded into NASA's Robonaut2 humanoid robot on-board the International Space Station.

See a news article about the lab's recent projects here.

See award abstracts for NSF grants funding the research here:

Postdoc Summary of Duties and Responsibilities
Candidate(s) will conduct world-class research in the area of formal methods, including design-time and/or runtime verification. Topics include defining new specification logic variants, formal requirements elicitation, proving algorithmic complexity and correctness, formal modeling, and algorithmic advances contributing to industrial-shaped instances of symbolic model checking, proving properties of runtime verification, and assuring development and operation of autonomous systems. Candidate is expected to contribute his/her own research ideas and collaborate with the laboratory to conduct independent research. Teaching and/or research-in-education opportunities are available if the candidate desires, but not required.

Program & College Description
The postdoc(s) and PhD students will have offices in Howe Hall, a $50 million state-of-the-art teaching and research complex including a Virtual Reality Application Center. The College of Engineering consists of 8 departments, with 250+ faculty members and annual research expenditures exceeding $88 million. ISU hosts a booming formal methods community, including many large research groups and prominent researchers working in various areas of formal verification across three departments: computer science, aerospace engineering, and electrical and computer engineering.

About Iowa State University and the Ames Community
Iowa State University is classified as a Carnegie Foundation Doctoral/Research University-Extensive, a member of the Association of American Universities (AAU), and ranked by U.S. News and World Report as one of the top public universities in the nation. Over 36,000 students are enrolled, and served by over 6,200 faculty and staff (see www.iastate.edu). Ames, Iowa is a progressive community of 60,000, located approximately 30 minutes north of Des Moines, and recently voted the best college town in the nation. Ames, Iowa has a legendary standing as a great place to live, regularly topping lists for e.g., opportunities for work-life balance, green living, and great infrastructure for cycling.

Postdoc Application Instructions
To apply for this position, please:

The start date is flexible, but we aim to fill the positions as soon as possible.

Applicants must have a PhD in Computer Science or a related subject at the time they start the position, be fluent in English, have good abilities to work in an international setting. The position is initially offered for one or two years, with opportunities for extensions. Salary and benefits at ISU are competitive and commiserate with experience. There are flexible options for remote work due to the COVID-19 pandemic.

If desired, there are several opportunities for growing the teaching section of the postdoc's CV; please specify if you want to explore this option. Possible courses for teaching experiences include a junior-level undergraduate C programming course on robust software engineering practices, numerical algorithms, and good code documentation in LaTeX; or an advanced course in Applied Formal Methods. ISU Center for Excellence in Teaching and Learning offers many opportunities for postdocs to learn state-of-the-art teaching best-practices. The ISU Center for Communication Excellence offers individualized training in written and oral communication skills to improve the quality of papers, proposals, and oral presentations. This is an excellent opportunity to enhance a CV for future academic positions.

PhD Application Instructions

Postdoc Position at Max Planck Institute for Informatics, Saarbrücken, Germany

The Automation of Logic group, led by Dr Christoph Weidenbach, is searching for a researcher to work with us on the next generation of automated reasoning procedures. We are interested in new ways for combining classical logics with theories in theory and practice.

The position is for up to five years. We will support the successful applicant to build his/her own subgroup and to get the right for PhD supervision at Saarland University. We expect a background in automated reasoning, preferrably including programming experience.

To apply for this post, please send your personal record (including CV, publication list, research statement) by email to Jennifer Müller. The deadline for the application is 28 February 2020.

The Editor's Corner

Happy end of the year festivities!