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
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 2021Nominations 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.
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.
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)
More information is available on the conference's web page, and on the online CfP.
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.
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
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
More information is available on the conference's web page.
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.
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).
All submissions will be electronic via easychair.
More information is available on the symposium's web page.
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 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
Important dates
More information is available on the colloquium's web page.
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.
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 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.
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.
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.
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.
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:
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
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.
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
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.
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.
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.
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.
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.
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:
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:
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.
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
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
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
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.
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.
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.
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.
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.
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.
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:
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.
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
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.
Job Description
The Opportunity:
(TAS) programme, funded through the UKRI Strategic Priorities Fund and
delivered by the Engineering and Physical Sciences Research Council
(EPSRC). The TAS programme brings together research communities and
key stakeholders to drive forward cross-disciplinary, fundamental
research to ensure that autonomous systems are safe, reliable,
resilient, ethical and trusted.
The appointee to this post, in the area of NLP, will be supervised by Prof Alex Lascarides, and also work closely with Prof Alan Bundy, Dr Ajitha Rajan and Prof Subramanian Ramamoorthy who leads the Research Node. This post will be based in the School of Informatics, University of Edinburgh.
The post is primarily open to someone with a background and PhD in in AI, Machine Learning or similar area, and practical experience with machine learning for NLP and image processing.
Your skills and attributes for success:
All enquiries should be directed to Prof Ram Ramamoorthy. Feedback is only provided to interviewed candidates.
Click here for a copy of the full job description.
As a valued member of our team you can expect: An exciting, positive, creative, challenging and rewarding place to work. We give you support, nurture your talent and reward success. You will benefit from a competitive reward package and a wide range of staff benefits, which includes a generous holiday entitlement, a defined benefits pension scheme, staff discounts, family friendly initiatives, flexible working and much more. Access our staff benefits page for further information and use our reward calculator to find out the total value of pay and benefits provided.
The University of Edinburgh holds a Silver Athena SWAN award in recognition of our commitment to advance gender equality in higher education. We are members of the Race Equality Charter and we are also Stonewall Scotland Diversity Champions, actively promoting LGBT equality.
If invited for interview you will be required to evidence your right to work in the UK. Further information is available on our right to work webpages
The University is able to sponsor the employment of international workers in this role. If successful, an international applicant requiring sponsorship to work in the UK will need to satisfy the UK Home Office’s English Language requirements and apply for and secure a Tier 2/Skilled Worker Visa. About Us As a world-leading research-intensive University, we are here to address tomorrow’s greatest challenges. Between now and 2030 we will do that with a values-led approach to teaching, research and innovation, and through the strength of our relationships, both locally and globally. About the Team Informatics is the study of how natural and artificial systems store, process and communicate information. Research in Informatics promises to take information technology to a new level, and to place information at the heart of 21st century science, technology and society. The School enjoys collaborations across many disciplines in the University, spanning all three College, and also participates as a strategic partner in the Alan Turing Institute and, with Heriot-Watt University, in the Edinburgh Centre for Robotics.
The School provides a fertile environment for a wide range of studies focused on understanding computation in both artificial and natural systems. It attracts students around the world to study in our undergraduate and postgraduate programmes, and currently has approximately 1000 undergraduate students, 320 MSc students and 350 PhD students. Informatics is one of seven schools in the College of Science and Engineering, at the University of Edinburgh. It is recognised for the employability of its graduates (demand exceeds supply), its contributions to entrepreneurship, and the excellence of its research. Since the first Research Assessment Exercise in 1986, Informatics at Edinburgh has consistently been assessed to have more internationally excellent and world-class research than any other submission in Computer Science and Informatics. The latest REF 2014 results have again confirmed that ours is the largest concentration of internationally excellent research in the UK. This contributes to our ranking in the top 15 CS departments world-wide according to the latest Times Higher Education ranking.
We aim to ensure that our culture and systems support flexible and family-friendly working and recognise and value diversity across all our staff and students. The School has an active programme offering support and professional development for all staff; providing mentoring, training, and networking opportunities. The School of Informatics holds a Silver Athena SWAN award, in recognition of our commitment to advance gender equality in higher education and research.