The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning is presented to
Natarajan Shankar
in recognition of his highly influential work in several areas of automated reasoning,
notably in formalization of proofs, cooperation of interactive theorem proving and
decision procedures, and applications to verification."
The Herbrand award committee 2022 consisted of Franz Baader (Chair), Pascal Fontaine, Radu Iosif, and Silvio Ghilardi.
The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
Alexander Bentkamp
for his dissertation “Superposition for Higher-Order Logic"” supervised by Prof. Wan Fokkink, Dr. Jasmin Blanchette, and Dr. Uwe Waldmann. The thesis was selected for its substantial contributions to the field of Automated Reasoning, with the development of a complete set of theoretical tools to generalize the superposition calculus to higher-order logic. In particular, the thesis introduced a new family of well-founded ordering on terms, the embedding path orderings, which are instrumental to lift the calculus from first-order to higher-order logic while retaining refutational completeness. The development of those orderings and of the calculus itself had immediate impact on automated higher-order theorem provers with outstanding empirical results as well as a very successful performance in tool competitions.
Presented at IJCAR 2022, the 11th International Joint Conference on Automated Reasoning.
The McCune award committee 2022 consisted of Nikolaj Bjorner, Pascal Fontaine, Carsten Fuhs, Marijn Heule, Cláudia Nalon, Andrew Reynolds, Philipp Rümmer, Martina Seidl, Viorica Sofronie-Stokkermans, and René Thiemann.
In the summer of 1972, Alain Colmerauer and his team in Marseille developed and implemented the first version of the logic programming language Prolog. Together with both earlier and later collaborations with Robert Kowalski and his colleagues in Edinburgh, this work laid the practical and theoretical foundations for the Prolog and logic programming of today. Prolog and its related technologies soon became key tools of symbolic programming and Artificial Intelligence.
The Year of Prolog celebrates the 50th anniversary of these events and highlights the continuing significance of Prolog and Logic Programming both for symbolic, explainable AI, and for computing more generally.
This celebration will culminate with the award of the inaugural edition of the ALP Alain Colmerauer Prolog Heritage Prize for recent practical accomplishments that highlight the benefits of Prolog-inspired computing for the future. The Prize will be presented at the Prolog Day Symposium on November 10, 2022, in Paris, France.
Eligibility
Any individual or group of individuals can nominate themselves or
their institution(s)/organization(s) for the Prize.
Selection
The Prize will be given for depth, novelty, and proven or potential
impact. A shortlist of up to five nominations will also be selected in
the process.
Endowment
The winner(s) will receive a certificate and a cash Prize of 2,000
Euros. The expenses of the shortlisted nominees will be covered up to
1,000 Euros, supported by the Artificial Intelligence Journal.
Timeline
Given the importance of proofs for, among other things, the usability of SMT solvers (see for example Chantal Keller's and Pascal Fontaine's guest columns' on the matter), the lack of a standard for SMT proofs is a long overdue issue for the community to address. It complicates adoption, both from users and from solver developers, and creates monolithic infrastructures that don't transfer easily between solvers.
Almost a year ago, a discussion took place on the SMT-LIB google groups about a hypothetical Proof Validation track on SMT-COMP, which would need a standard for SMT proofs. The discussion quickly diverged into the usual competing views about proof formats, proof calculi, proof granularity, and so on. In trying to reach common ground, the SMT community has started a joint effort to move towards a standard. A group was formed and meetings started to take place. The first one was in June this year, the next one will be in July and there will be an in-person session dedicated to this discussion at the SMT workshop, in Haifa, Israel.
Here is a summary of the discussions in the first meeting:
Proofs vs traces (for scalability)
A point of discussion was about focusing on producing detailed proofs or on producing coarse proofs ("traces").
On the one hand, the latter would be simpler and cheaper to generate, which would address the issue of solvers choking when generating proofs. On the other hand these proofs would be harder to check, possibly as hard as solving the original problem. A staged approach would mitigate this issue by enriching the coarse proof offline ("elaboration"). SAT proofs leverage this for example for elaborating DRAT into LRAT. SMT proofs would be much more challenging since not having preprocessing or theory lemma proofs would require redoing these possibly expensive steps, as well as having instrumented proof producing versions of the solving. Elaboration tools should probably be based on fine-grained-proof-producing SMT solvers.
Proof structure and BNF for a proof format
A crucial point in the discussion was whether a proof should be a list of commands (representing proof steps with explicit conclusions) or a single proof term. The former incentives local reasoning, with each command expected to be independently checkable (can be very helpful for, say, parallel proof checking or more localized error flagging). Proof terms on the other hand may facilitate writing proofs when you do not want to generate intermediate conclusions (with proof rules being functions from premises). A flexible approach could be to have commands but whose premises could be either ids of other commands or proof terms (so that proofs can be inlined when one so desires).
Deciding on the above is a requirement to define a BNF for proof formats. The natural thing would be to define the proof BNF on top of SMT-LIB. This is for example what the proof formats Alethe (see Figure 2 here) and Jochen Hoenicke's (see Grammar here) do.
Logical framework and standard proof calculus
On the one hand, settling on a fixed proof calculus is difficult given the well-known differences of solving methods in SMT. On the other hand, providing just a framework makes it harder for users, requiring specialization in their proof usage for the calculus of each solver (if you do not want to support the framework itself). This is specially important for other uses of proofs than to just check them, which would naturally be specialized per calculus.
If we were to define a standardized calculus, however, it would be essential to have tooling to convert into this standardized calculus. Moreover, the granularity (and the number of rules) of this calculus would impact the trade-off between proof size and efficiency of proof checking, as well as the conversion effort.
A tentative agreement seemed to form on using SMT-LIB 3 to model the semantics of the proof format (and possibly of a standard calculus). A key point is that the framework should be carefully designed so that it does not have breaking changes afterwards, which would break the integration with tools using SMT proofs.
If you would like to participate in the discussions, you can join this google groups or this Zulip chat (the latter is more general but has a dedicated #smtproofs stream).
Also of note, this year SMT-COMP has a proof *exhibition* track, where teams submitted proof-producing SMT solvers and proof checkers for the proofs they emit. There is no fixed proof format. A qualitative assessment will be made on the entrants and will be issued, together with the results from all tracks, during the SMT workshop. You can also follow the news from the SMT-COMP website.
FLoC 2022 brings together twelve major international conferences, 70+ workshops, and several special events.
See the program here.
For those that do not yet know EuroProofNet, it is the European research network on digital proofs. EuroProofNet aims at boosting the interoperability and usability of proof systems. You can register here (follow the link "apply" on the main page).
The EuroProofNet Automated Theorem Provers Working Group (WG2) is organizing its kickoff meeting co-located with the 8th Workshop on Practical Aspects of Automated Reasoning (PAAR 2022), taking place at FLoC in Haifa, Israel, at August 11-12, 2022. While PAAR 2022 is a two-day event, the working group meeting will essentially be on the second day of PAAR (August 12). See here and here for further details.
A preliminary program, including plenary presentations, invited talks and discussion sessions is available on the meeting's webpage. The meeting will be primarily in-person, but the organizers plan to implement a hybrid format so that all interested EuroProofNet members can participate via a video call (Details TBA).
EuroProofNet can support the in-person participation of WG members. If you want to apply for travel funding support, please send a brief statement about your motivation and topical fit (max. half a page), together with a justified travel cost estimation (e.g., via screenshots or invoices for flights), to Pascal Fontaine and Alexander Steen until the deadline (see below).
Confirmed speakers
Important dates
Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences.
More information is available on the conference's web page.
LPNMR 2022 aims to bring together researchers from LPNMR core areas and application areas of the aforementioned kind in order to share research experiences, promote collaboration and identify directions for joint future research.
Registration is now open.
More information is available on the conference's web page.
FSTTCS 2022 is organised by IARCS, the Indian Association for Research in Computing Science, in association with ACM India. It is a forum for presenting original results in foundational aspects of Computer Science and Software Technology.
List of Topics
Track A
Important Dates
More information is available on the conference's web page.
FM 2023 is the 25th international symposium in a series organised by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The FM symposia have been successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral research. FM 2023 will be both an occasion to celebrate and a platform for enthusiastic researchers and practitioners from a diversity of backgrounds to exchange their ideas and share their experiences.
Topics of Interest
FM 2023 will highlight the development and application of formal methods
in a wide range of domains including trustworthy AI, software,
computer-based systems, systems-of-systems, cyber-physical systems,
security, human-computer interaction, manufacturing, sustainability,
energy, transport, smart cities, healthcare and biology. We particularly
welcome papers on techniques, tools and experiences in interdisciplinary
settings. We also welcome papers on experiences of applying formal methods in industrial settings, and on the design and validation of formal method tools.
The topics of interest for FM 2023 include, but are not limited to:
Important Dates
More information is available on the symposium's web page.
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education.
CPP 2023 will welcome contributions from all members of the community. The CPP 2023 organizers will strive to enable both in-person and remote participation, in cooperation with the POPL 2023 organizers.
Topics of Interest We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP:
Important Dates
More information is available on the conference's web page.
Since 1994, the RAMiCS conference series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond.
Depending on the Covid-19 situation, it will take the form of a physical conference, a virtual conference, or a hybrid between the two.
Topics:
We invite submissions in the general fields of algebras relevant to computer science and applications of such algebras. Topics include but are not limited to:
Important Dates:
More information is available on the conference's web page.
For the first time, STACS 2023 will consist of two tracks, A and B, to facilitate the work of the program committee(s).
Lists of Topics
Authors are invited to submit papers presenting original and unpublished research on theoretical aspects of computer science. Typical areas include:
Important Dates
Fundamentals of Software Engineering (FSEN) is an international conference that aims to bring together researchers, engineers, developers, and practitioners from academia and industry to present and discuss their research work in the area of formal methods for software engineering. Additionally, this conference seeks to facilitate the transfer of experience, adaptation of methods, and where possible, foster collaboration among different groups. The topics of interest cover all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry and promoting their integration with practical engineering techniques.
Topics of Interest The topics of this conference include, but are not restricted to, the following:
Important Dates (AoE)
More information is available on the conference's web page.
Information for real-life AI applications is usually pervaded by uncertainty and subject to change, thus demands non-classical reasoning approaches. At the same time, psychological findings indicate that human reasoning cannot be completely described by classical logical systems. Sources of explanations are incomplete knowledge, incorrect beliefs, or inconsistencies. A wide range of reasoning mechanisms has to be considered, such as analogical or defeasible reasoning, possibly in combination with machine learning methods. The field of knowledge representation and reasoning offers a rich palette of methods for uncertain reasoning both to describe human reasoning and to model AI approaches.
The aim of this series of workshops is to address recent challenges and to present novel approaches to uncertain reasoning and belief change in their broad senses, and in particular provide a forum for research work linking different paradigms of reasoning. A special focus is on papers that provide a base for connecting formal-logical models of knowledge representation and cognitive models of reasoning and learning, addressing formal and experimental or heuristic issues. Previous events of the Workshop on "Formal and Cognitive Reasoning" and joint workshops took place in Dresden (2015), Bremen (2016), Dortmund (2017), Berlin (2018), Kassel (2019), Bamberg (2020, online), and Berlin (2021, online).
We welcome papers on the following and any related topics:
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 application documentation to ease the justification of design choices and the review of code and proofs.
Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logic 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.
Topics: constructive mathematics constructive analysis computable analysis exact real number computation
CCC is a workshop series that brings together researchers applying logical methods to the development of algorithms, with a particular focus on computation with infinite data, where issues of continuity, computability and constructivity play major roles. Specific topics include exact real number computation, computable analysis, effective descriptive set theory, constructive analysis and topology, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and other continuous data, which are of increasing importance in safety-critical applications and scientific computation.
Participation is welcome in person or online.
The workshop invites all contributions relating to computation where issues of continuity, computability and constructivity play major roles. Specific areas of interest include:
Deadlines
More information is available on the workshop's web page.
Software and proof verification has grown significantly in the last 15 years. Growth has come to the point where verification systems are complex and manually proving the soundness of those verification systems sometimes exceeds what a single research group can understand and verify as correct.
Even formally defining soundness can be challenging and its definition is varying from system to system. Specific research groups can have very specific notions of soundness they focus on, but those can diverge from what the users expect, especially if the users come from a different verification environment or they are approaching verification for the first time.
Participants to Unsound will be able to share their experience and exploits on how different verification tools can either be broken or expose confusing behavior, likely to be unexpected by users. We think this would be greatly beneficial not only because it will help all of us to iron out those unsoundnesses but also because it will facilitate understanding of the foundational differences between the assumptions of the various research lines.
The current academic environment encourages us to talk about the success case of our work. In this workshop we want to address and learn from failure cases and we want to reinforce the bedrock of our understanding. In practice, when we divert our focus to a specific aspect of verification we may (understandably) be less precise. For example, a line of research focusing on aliasing control in OO may be less precise when considering the implication in other areas, like termination. We believe that learning from the issues of many verification projects can broaden the attention of researchers to topics which so far escaped their focused area of research; e.g., from only type correctness to also avoiding stack overflows.
We believe that this environment would be particularly beneficial for young researchers that are in search of open questions in verification. This may provide a motivation to deep dive into the details of any particular tool, or to expand their individual area of expertise to get a wider and more objective and critical view of the whole area of verification.
We also wonder if in our fast expansion we accidentally glossed over some fundamental issue in verification, and if our mistake has now become engraved into the established wisdom and it is sometimes uncritically assumed as a valid reasoning stepping stone.
We are particularly interested in sources of unsoundness that are accidentally shared by many different unrelated research lines, and to develop an understanding on why this is the case.
The workshop would be its first instance and is meant to be welcoming for both people with strong theoretical skills, as well as people who just like hacking things. We do not expect fully polished submissions and we will not have formal proceedings. Students are especially welcome to attend.
Examples for possible contributions would be:
Deadline: 2022-09-01 (23:59 AOE)
More information is available on the workshop's web page.
The increasing adoption of Artificial Intelligence techniques in safety-critical systems, employed in real world scenarios, requires the design of reliable, robust, and verifiable methodologies. Artificial Intelligence systems employed in such applications need to provide formal guarantees about their safety, increasing the need for a close interaction between the Artificial Intelligence and Formal Methods scientific communities.
To witness this increasing need, tools and methodologies integrating Formal Methods and Artificial Intelligence solutions are getting more and more attention. The workshop is the main official initiative supported by the OVERLAY group. The event aims at establishing a stable, long-term scientific forum on relevant topics connected to the relationships between Artificial Intelligence and Formal Methods, by providing a stimulating environment where researchers can discuss about opportunities and challenges at the border of the two areas.
Important goals of the workshop are (i) to encourage the ongoing interaction between the formal methods and artificial intelligence communities, (ii) to identify innovative tools and methodologies, and (iii) to elicit a discussion on open issues and new challenges.
Topics of interest include (but are not limited to):
Contributed papers can present recent results at the border of the two fields, new research directions, challenges and perspectives. Presentation of results recently published in other scientific journals or conferences is also welcome.
Important Dates
More information is available on the workshop's web page.
The following speakers have accepted to give courses at VTSA 2022:
Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science. It includes the lectures, daily coffee breaks and lunches as well as a school dinner. EuroProofNet will refund the travel and accommodation of a number of participants. Please express your interest with your application. Attendance is limited to 40 participants.
Please apply electronically by sending to Jennifer Müller:
The deadline for application is July 20th, 2022. Notification of acceptance will be given by July 22nd, 2022.
More information is available on the school's web page.
Term Rewriting is a simple but powerful model of computation with numerous applications in computer science and mathematics. It is heavily used in symbolic computation, formal reasoning, and program verification. Rewriting-based techniques are useful in many other fields as well, for instance, in quantum computing, biology, music...
The 13th International School on Rewriting (ISR 2022) will take place at Ivane Javakhishvili Tbilisi State University, Tbilisi, Georgia. The school is aimed at students, researchers and practitioners interested in the use or the study of rewriting and its applications and offers two parallel tracks:
Registration
For the registration visit the Easychair system.
The registration fee is 200/250 Euro for students (early till July 31/late till August 31) and 350/400 for non-students (early till July 31/late till August 31), which will include access to school materials, coffee breaks, and social events (excursion and banquet). The registration fee for an accompanying person is 150 Euro and includes only social events.
Participants affiliated with Georgian and Ukrainian universities will have the registration fee waived. Further support will be announced if funds get available.
More information is available on the school's web page.
The ICTAC conference series aims at bringing together researchers and practitioners from academia, industry and government to present research and exchange ideas and experience addressing challenges in both theoretical aspects of computing and the exploitation of theory through methods and tools for system development. ICTAC also aims to promote research cooperation between developing and industrial countries.
The intended audience of the school includes master and PhD students as well as young researchers from the fields of computer science and mathematics. The following lectures agreed to deliver classes at the school:
Registration
For the registration visit the Easychair system.
The registration fee is 200/250 Euro for students (early till July 31/late till August 31) and 350/400 for non-students (early till July 31/late till August 31), which will include access to school materials, coffee breaks, and social events (excursion and banquet). The registration fee for an accompanying person is 150 Euro and includes only social events. Participants affiliated with Ukrainian universities will have the registration fee waived. Further support will be announced if funds get available.
More information is available on the school's web page.
The 4th International Autumn School for Proof Theory in Utrecht is arranged under the auspices of The Proof Society, and is sponsored by the Dutch Research Council, Universities of Amsterdam and Utrecht, and the Kurt Gödel Society. The Proof Society has recently been formed to support the notion of proof in its broadest sense, through a series of suitable activities; to be therefore inclusive in reaching out to all scientific areas which consider proof as an object in their studies; to enable the community to shape its future by identifying, formulating and communicating its most important goals; to actively promote proof to increase its visibility and representation.
The aim of the Autumn school is to cover basic and advanced topics in proof theory. The focus of the fourth edition will be proof theory of modal logic, computational content of proofs, proof complexity, proof theory of set theory, and philosophical aspects of proof. Other areas such as constructivism and reverse mathematics will be represented through research talks at the following workshop. The intended audience is advanced master students, PhD students, postdocs and experienced researchers in mathematics, computer science and philosophy.
The Autumn school is co-located with a workshop on proof theory in Utrecht (11-12 November). We invite proposals for contributed talks at the workshop. These can be on published or unpublished work, as well as work in progress. Best talk presented by a student will receive an award from The Proof Society.
The Autumn school will consist of 5 courses:
More information is available on the school's web page.
As part of the « Autonomous Train » innovation program, Railenium offers a research engineer in formal methods to work on intelligent rail signaling systems.
John Wickerson and Alastair Donaldson have an opening for a two year postdoc on specification and verification of heterogeneous systems, and their programming languages. See here for details.
Feel free to contact either Alastair or John if you're interested in applying and would like to chat informally first.
Michael Benedikt has a postdoc position at Oxford available.
The ideal fit would be for a project with Milos Nikolic at Edinburgh on nested data. Don't be scared if you don't know what nested data is, or if it has a frighteningly applied ring to it! The project is quite broad. For theory, see the POPL 2021 paper here.
This part of the project relates to interpolation/Beth definability, including ongoing work with Pierre Pradic at Swansea and Christoph Wernhard at Dresden. Background in proof theory or model theory (not necessarily both) would be necessary.
On the applied side, the project relates to the Trance system, which we have overviewed at VLDB (e.g here, related to query compilation), and to a paper on applications to bio.
Milos Nikolic also has a PDRA position on the grant; for someone who wants to work more on the system side, we could discuss whether Oxford or Edinburgh is the best fit.
The PDRA position could also fit a researcher with a background relevant to other topics under investigation at Oxford, particularly:
The projected start date for the post is Sept 22, which I know is quite soon; but there is flexibility on that. If you know anyone who might be interested, please forward; also happy to discuss with anyone who wants to drill down on the workplan.
Vincent Rahli would like to invite applications for both:
The postdoctoral researcher and PhD students will contribute to an EPSRC-funded project aiming at designing and formally verifying distributed systems, in particular Byzantine fault-tolerant distributed systems as used for example in blockchain technology.
The start date is flexible, ideally around October 2022.
The environment:
The School of Computer Science has large and thriving Theory and Security research groups. Among our research interests related to this project are for example:
Both groups are very active, organising regular seminars, informal meetings, and actively participating in many events such as the Midlands Graduate School or the Cyber Security PhD Winter School. For more information see here and here.
How to apply:
Interested people are encouraged to contact Vincent Rahli by email to discuss their research interests and details of the positions. Further information on how to apply to the PhD position is provided here.
David Baelde and colleagues are looking for engineers and postdocs to work on Squirrel, a proof assistant dedicated to proving cryptographic protocols. They have a broad range of projects in mind, ranging from pure OCaml development to involved protocol formalizations, with several theoretical questions in between. If you'd like to work on some of these aspects for one or more years, please get in touch with them!
More details can be found here.
MSR Cambridge UK is hiring a post-doctoral researcher to collaborate on automatic tools for development and deployment of cloud-scale AI/ML systems. There is a wealth of research opportunities and challenges in scheduling and optimization, constraint solving, program synthesis, local search, and other areas.
Contact: Andrey Rybalchenko
There is a PhD position open at Chalmers University of Technology, Gothenburg, Sweden, on the topic of Smart Contract Verification. The title of the position is: "Formal Verification of Blockchain Applications". The announcement is linked here.
The Faculty of Mathematics of the University of Vienna advertises a Tenure-Track Professorship for the field of Mathematical Logic. They are looking for an outstanding early career scientist working in mathematical logic.
The application deadline is 13 September 2022.
More information about the application procedure can be found here.
The University of Vienna is an equal opportunity employer and values diversity. The University strives to increase the share of women in professorial positions. Given equal qualifications, preference will be given to female applicants.
Keywords: theorem proving, programming languages, operating systems, formal verification, dependent types, theory of contracts
Project RIOT-fp is an Inria Challenge with the objective of developing future-proof operating system libraries [1,3] for application to IoT: RIOT. Our PhD project is interested in one of the futures of RIOT: RIOT-rs, implemented in Rust. This computing base provides access to a vast ecosystem of analysis, code generation, verification and proof tools. It offers us to rethink a system software validation process that would suit both system programming and verification requirements (as one may expect from using, e.g., a theorem prover).
The notion of contract [2] is one such interface between the development and verification of system programs. A contract allows, on one hand, to formally document the hypothesis and guarantees of system modules, functions, artifacts, with respect to global safety ad security requirements. Contracts can be sufficiently abstract and comprehensible for system programmers, and adequately refined to meet the strongest requirements of mechanized verification.
Our project will focus on the development of such a modular validation flow by case-studying the core of RIOT's implementation in Rust. We define and exercise this workflow to characterize and validate global requirements ranging from race-condition, deadlock avoidance, priority management and schedulability, and/or memory isolation, fault isolation, information flow control.
The project will be implemented with teams Tea and Celtique at Inria, Rennes, in close collaboration with RIOT-fp teams in Paris. It requires a Master degree with solid background in proof theory and mathematical logic, programming languages and type theory, as well as motivation and interest in both the implementation and verification of operating systems. Prior knowledge and experiences with Rust and either Coq, Iris and/or Lean, F* will stand out.
Please visit this website for detailed information and for application.
References
Two PhD positions funded by the ANR projects BLaSST and ICSPA on subjects around formal proofs for set-based specification languages are available at Inria Nancy.
More details on the two subjects, as well as information about how to apply, are available at the URLs indicated above. The theses are meant to start in the fall of 2022, the exact starting date is negotiable. Stephan Merz will be very happy to answer any question about the two thesis offers.
There is an open position for a researcher in Formal Verification at Hensoldt Cyber GmbH in Munich, Germany.
This involves formal verification of software and/or hardware using Isabelle/HOL and assorted tools, both doing actual verification work and expanding the state of the art in this domain.
For more information, have a look at the job offer here, where you can also apply directly.
If there are any questions, feel free to contact Jaap Boender
The Department of Computer Science at University of Sheffield has an open position of Lecturer or Senior Lecturer in Cybersecurity. Details can be found here.
Note that "formalisation and proof of system security properties" is listed as a topic of interest. Women are particularly encouraged to apply. All applicants will be given equal consideration.
PostDocs
Jonni Virtema is looking for two PostDocs to join the Verification group of the University of Sheffield to work with him in his DFG funded project "Logical approach to quantum mechanics and contextuality".
All candidates interested in working in the general topic of logics and complexity theory utilising numerical features and real valued data are encouraged to apply.
The project topics range from logical foundations of probabilistic data and complexity theory utilising real numbers to logical approach to quantum information theory utilising the newly discovered connections to probabilistic team semantics. Candidates with expertise in finite model theory, logic in computer science, or foundations of quantum information theory are in particular encouraged to apply.
Interested candidates are encouraged to contact Jonni Virtema directly by email for further details. For more details on the topic, the candidate may refer to the subsection "Probabilistic Logics and Metafinite Model Theory" at this website.
The full advert is available here.
PhD
Jonni Virtema is looking for a motivated PhD student to join the Verification group of the University of Sheffield. The topic of the PhD project is quite flexible, but should relate to temporal logics for verification (for more details, see here).
PhD topics related to logical foundations of probabilistic data and complexity theory utilising real numbers is also possible, please contact Jonni Virtema directly for details.
The Studentship will cover tuition fees at the UK rate and provide a tax-free stipend at the standard UKRC rate (currently GBP 15,609 for 2021/22) for three and a half years. International students are eligible to apply, however will have to pay the difference between the UK and Overseas tuition fees.
Interested candidates are encouraged to contact Jonni Virtema directly by email for further details. For more details on the topic, the candidate may refer to the subsection "Logics for Verification" at this website.
DTU Compute, the section for Software Systems Engineering of the Technical University of Denmark is looking for a bright and motivated PhD student for a 3-year PhD position. The research topic is the hybrid (static+runtime) verification of concurrent and distributed applications (details below).
The project is funded by DFF.dk, and is in collaboration with Motorola Solutions Danmark A/S, the University of Malta, and Imperial College London.
It is an excellent opportunity to be involved in advanced research on concurrent and distributed systems, with important practical applications.
Project Description
The project goal is to develop new methods and tools to verify the correctness of distributed applications, by combining static verification (e.g. type-checking) and runtime verification (monitoring). We will tackle scenarios where heterogeneous software components are expected to interact correctly but cannot be fully verified before deployment: this is a common scenario in microservices, IoT, and edge computing. The main research questions are: how can we model these heterogeneous systems? How can we combine static and runtime verification, and what guarantees can we achieve? Can we implement these research results as prototype tools to aid software development?
Responsibilities and Qualifications
If you join this project, you will become a member of the DTU Compute
research section on Software Systems Engineering. You will also
join the DTU Compute PhD school and take part in its courses and
activities. As part of your PhD training and research activities, you will have research stays at the academic collaborators’ universities. Links:
Your main tasks within this project will be:
Your duties will also include some Teaching Assistance work at DTU, and (if you wish) the co-supervision of BSc and MSc student projects related to your research.
To be considered for the position, you need some familiarity with formal methods for programming languages (e.g. type systems) and/or for distributed systems (e.g. process calculi, model checking). You will need to document these skills by listing the relevant university courses you took, or the relevant experience you have.
It will be an advantage if you can also document good programming skills (preferably including functional programming).
To begin the PhD position, you must have a two-year master's degree (120 ECTS points) or a similar degree with an academic level equivalent to a two-year master's degree. You can apply prior to obtaining the degree, providing the expected graduation date.
Assessment and Further Details The assessment of the applicants will take place in early September 2022.
For the application details, see here.
For further information and inquiries, please contact Alceste Scalas.
You can read more about DTU Compute and the DTU Compute Research Section on Software Systems Engineering by following the links.
If you are applying from abroad, you may find useful information on working in Denmark here.
1 Year (renewable) post-doc position in Logic within BRIO Project to work with the Logic, Uncertainty, Computation and Information (LUCI) Group, Department of Philosophy, University of Milan.
Project:
This project aims to develop logics for the verification of properties of interest in the development and use of machine learning systems in Artificial Intelligence. In particular, the aim is to develop methods for demonstrating or verifying models that simulate the probabilistic structures underlying supervised, unsupervised and/or reinforcement learning methods and to check for biases and assess their risks.
The project activities consist of:
Profile of the Researcher
The ideal candidate has obtained a PhD in Logic or related field (Philosophy/AI/CS/Mathematics), with knowledge of least two of the following disciplines:
How to apply & deadline
The deadline for application is on 09th September 2022 at 23:59 CET (strict – please note that late applications cannot be considered). Please follow carefully the instructions available on the official call
Online interviews are scheduled on 19th September 2022 at 10:00 CET.
For any informal inquiry please write to Giuseppe Primiero.
The group of André Platzer, the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems, in the Department of Informatics at KIT is recruiting a PhD student or postdoc (TVL E13, full-time). Our research develops the logical foundations for cyber-physical systems and practical theorem proving tools for analyzing and correctly building such systems, including the theorem prover KeYmaera X, verified runtime monitoring ModelPlex, verified compilation, and verified safe machine learning techniques. Our techniques are used to analyze the safety of autonomous cars, airplanes and collision avoidance protocols in aerospace applications, robotics, and train control.
Key requirements for successful applications:
The successful candidate is able to quickly get into new research areas and will be responsible for actively engaging in novel research questions, publishing and communicating research results, advising junior students, assisting in research grants, implementation of research results in formal methods tools, and demonstrating their applicability in cyber-physical systems applications.
Faculty / Division: Alexander von Humboldt Professor on Logic of Autonomous Dynamical Systems
Institute: Institute of Information Security and Dependability (KASTEL)
Starting Date: Immediately
Contact Person: André Platzer (email)
This is a call for interest for PhD and postdoctoral research at Yoni Zohar’s group in Bar-Ilan University.
The positions will focus on Satisfiability Modulo Theories (SMT) methods for verification of smart contracts, as well as for bit-precise reasoning.
The work will be done in collaboration with the University of Iowa and Stanford University.
Qualifications
The ideal applicants would have:
Interested applicants should send their CV, including a list of publications, in PDF to Yoni Zohar together with the names of at least two references.
Starting date is planned for 2022-2023.