The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning is presented to
in recognition of his outstanding contributions to satisfiability solving, including innovative applications, methods for formula pre- and in-processing and proof generation, and a series of award-winning solvers, with deep impact on model checking and verification.
Presented at IJCAR 2024, the 12th International Joint Conference on Automated Reasoning.
The Herbrand Award Committee 2024 consisted of Maria Paola Bonacina (Chair), Franz Baader, Jasmin Blanchette, and Daniel Le Berre.The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for her dissertation “Formally Verifying Algorithms for Real Quantifier Elimination” supervised by Prof. Dr. André Platzer. The thesis was selected for its strong theoretical and practical contributions to formally verified quantifier elimination for the first-order logic of real arithmetic. Quantifier elimination is a crucial technique for automated reasoning, specifically for propositions about real numbers, yet notoriously hard to implement efficiently and correctly. The thesis tackles the problem rigorously, by formalization and formal verification in the Isabelle/HOL theorem prover, providing an additional layer of correctness assurances over conventional pen-and-paper approaches. The thesis formalizes virtual substitution as an incomplete yet practically relevant quantifier-elimination technique and provides a verified executable implementation via code generation that is experimentally competitive with unverified state-of-the-art implementations. In addition to virtual substitution, the thesis also considers complete quantifier-elimination algorithms. In particular, it provides the first quantifier-elimination algorithm for the full multi-variate setting that is formally verified in Isabelle/HOL, an important step towards the verification of the more optimized state-of-the-art algorithms.
Presented at IJCAR 2024, the 12th International Joint Conference on Automated Reasoning.
The Bill McCune PhD Award Committee 2024 consisted of Carsten Fuhs (chair), Haniel Barbosa, Pascal Fontaine, Laura Kovács, Cláudia Nalon, Philipp Rümmer, Martina Seidl, Viorica Sofronie-Stokkermans, René Thiemann, and Sophie Tourret.The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand, Bill McCune, and Skolem Award selection committee, instituting new awards, etc.
Nominations for two CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2024.
The current members of the board of trustees are (in alphabetical order):
The terms of Cláudia Nalon and Stephan Schulz end. Cláudia Nalon may be nominated for a second term, whereas Stephan Schulz has already served two consecutive terms and cannot be nominated this year.
The term of office of Christoph Benzmüller as IJCAR 2024 programme chair ends after the IJCAR conference. As outgoing ex-officio trustee, Christoph Benzmüller is eligible to be nominated as elected trustee.
In summary, we are seeking to elect two trustees.
Nominations can be made by any CADE member, either by e-mail or at the CADE business meeting at IJCAR 2024; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2021-2024. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations can be provided up to the upcoming CADE business meeting, via email to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
Nominations are invited for the 2024 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2023 and 31 December 2023 are eligible for nomination for the award.
Important Dates
The deadline for submission is 1 July 2024.
Nominations
Nominations should be submitted by the candidate or the
supervisor via Easychair.
Procedure
Please submit a pdf file containing:
The Award
The 2024 Ackermann award will be presented to the recipient(s)
at CSL 2025.
The award consists of a certificate, an invitation to present
the thesis at the CSL conference, the publication of the
laudatio in the CSL proceedings, an invitation to the winner
to publish the thesis in the FoLLI subseries of Springer LNCS,
and financial support to attend the conference.
Ackermann Jury
The jury consists of:
IJCAR is the premier international joint conference on all topics in automated reasoning.
IJCAR 2024 is the merger of leading events in automated reasoning:
Invited Speakers
Important Dates
Co-located Events
There will be ten workshops and two system competitions associated with IJCAR 2024:
More information is available on the conference's web page.
In 2024, the three following conferences will be held together:
The 51st EATCS International Colloquium on Automata, Languages and Programming (ICALP 2024) is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS).
The Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024) is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed.
The 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) 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 logic, models of computation, semantics and verification in new challenging areas.
Important Dates
Co-located Events
There will be fourteen workshops associated with LICS/ICALP/FSCD 2024:
More information is available on the conferences' web page.
Quantum Physics and Logic is an annual conference that brings together academic and industry researchers working on the mathematical foundations of quantum computation, quantum physics, and related areas. The main focus is on the use of algebraic and categorical structures, formal languages, type systems, semantic methods, as well as other mathematical and computer scientific techniques applicable to the study of physical systems, physical processes, and their composition. Work applying quantum-inspired techniques and structures to other fields, such as linguistics, artificial intelligence, and causality, is also welcome.
Important Dates
More information is available on the conference's web page.
The International Conference on Space Mission Challenges for Information Technology (SMC-IT) and the Space Computing Conference (SCC) gather system designers, engineers, computer architects, scientists, practitioners, and space explorers with the objective of advancing information technology, and the computational capability and reliability of space missions. The forums will provide an excellent opportunity for fostering technical interchange on all hardware and software aspects of space missions. The joint conferences will focus on current systems practice and challenges as well as emerging hardware and software technologies with applicability for future space missions.
Systems in all aspects of the space mission will be explored, including flight systems, ground systems, science and flight data processing, engineering and development tools, operations, telecommunications, high-performance space computing, radiation-tolerant computing devices, reliable electronics, robotics, intelligent systems and machine learning, distributed autonomy, networking and communications, and space-qualifiable packaging technologies. The entire information systems lifecycle of mission development will also be covered, such as conceptual design, engineering tools development, integration and test, operations, science analysis, and quality control.
Co-Located Events
In addition to the keynotes and main SMC-IT and SCC technical tracks,
the conference will feature the following workshops:
More information is available on the conference's web page.
CAV 2024 is the 36th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems.
Important Dates
Co-located Events
There will be ten workshops associated with CAV 2024:
More information is available on the conference's web page.
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.
ITP 2024 will be organized as a hybrid event.
Important Dates
Co-located Events
More information is available on the conference's web page.
The conference brings together researchers from various fields of logic with applications in computer science. Student sessions will be organized.
Topics of Interest
Conference topics include, but are not limited to:
Important Dates
More information is available on the conference's web page.
LPNMR is a forum for exchanging ideas on declarative logic programming, non-monotonic reasoning, and knowledge representation. The aim of the conference is to facilitate interactions between researchers and practitioners interested in the design and implementation of logic-based programming languages and database systems, and those working in knowledge representation and non-monotonic reasoning. LPNMR strives to encompass theoretical and experimental studies that have led or will lead to advances in declarative programming and knowledge representation, as well as their use in practical applications.
LPNMR 2024 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.
Topics of Interest
Conference topics include, but are not limited to:
Important Dates
More information is available on the conference's web page.
Since it was started in Hiroshima, Japan in 1997, ICFEM has provided a forum for both researchers and practitioners to discuss and exchange their experience and results in research on theories, methods, languages, and supporting tools for integrating formal methods into conventional software engineering technologies to provide more effective and efficient approaches to large-scale software engineering. The goal of this conference is to bring together industrial, academic, and government experts in both formal methods and software engineering to help advance the state of the art.
At its first return to Hiroshima since 1997, ICFEM 2024 will celebrate the 25th anniversary of the ICFEM conference series. Researchers, practitioners, tool developers, and users are all welcome to submit papers and participate in the conference. We look forward to your contributions and participation.
Topics of Interest
Conference topics include, but are not limited to:
Important Dates
More information is available on the conference's web page.
FROM aims to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and/or by creating or using software tools that apply theoretical contributions. Formal methods emphasise the use of mathematical techniques and rigour in developing software and hardware. They can be used to specify, verify, and analyse systems at any stage in their life cycle: requirements engineering, modeling, design, architecture, implementation, testing, maintenance and evolution. This assumes on one hand the development of adequate mathematical methods and frameworks and on the other hand the development of tools that help the user effectively apply these methods and frameworks.
The program of the symposium includes invited lectures and regular contributions. Submissions on the general topics of formal methods, theoretical computer science, logic and applications are welcome.
Topics of Interest
The topics of interest for FROM 2024 include, but are not limited to:
Important Dates
More information is available on the conference's web page.
The IEEE International Conference on Tools with Artificial Intelligence (ICTAI) is a leading IEEE-CS annual scientific meeting for three decades. It provides a major international forum where the creation and exchange of ideas related to artificial intelligence are fostered among academia, industry, and government agencies. The conference facilitates the cross-fertilization of these ideas and promotes their transfer into practical tools, for developing intelligent systems and pursuing artificial intelligence applications. The ICTAI encompasses all technical aspects of specifying, developing and evaluating the theoretical underpinnings and applied mechanisms of the AI-based components of computer tools such as algorithms, architectures and languages.
Topics of Interest
The topics of this conference include, but are not restricted to, the following:
Important Dates
More information is available on the conference's web page.
SBMF is devoted to the development, dissemination, and use of formal methods for the construction of high-quality computational systems. It is now a well-established event with an international reputation. It regularly receives submissions and participants from all over the world.
SBMF aims to provide a venue for the presentation and discussion of high-quality work in formal methods.
Topics of Interest
Conference topics include, but are not limited to applications of formal methods to:
Important Dates
More information is available on the conference's web page.
Principles of Programming Languages (POPL) is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation, or application of programming languages.
Important Dates
More information is available on the conference's web page.
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
More information is available on the conference's web page.
Recent rapid growth of AI has shown the potential to revolutionize most of the everyday aspects of human lives. The field of AI is traditionally divided into a number of subfields such as Machine Learning, Knowledge and Reasoning, Planning and Scheduling, SAT solving, Computer Vision (and others) that are usually pursued individually. But the challenges of real-world applications are often too hard for a single AI approach. Hence there is a need for Composite AI, which integrates several different AI approaches that complement each other to solve the problem. Development of Composite AI system is still a bit immature and mostly ad-hoc. The workshop aims at bringing together researchers and practitioners from different AI subfields to discuss challenges that they currently face and to initiate a discussion about the benefits and challenges of Composite AI.
Topics of Interest
Workshop topics include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
We invite PhD students working in the broad research areas covered by ECAI to participate in the Doctoral Consortium (DC) of ECAI-2024. The DC is an opportunity to meet and interact closely with other PhD students in your field. The DC also offers an opportunity to receive feedback on your work, and to get advice on managing your career.
Accepted PhD students will have the opportunity to present their work to peers attending the conference, in the form of oral and/or poster presentations. The accepted abstracts will be published on the DC website and the list of accepted PhD students will be included in the ECAI-2024 proceedings.
Besides student presentations, the DC programme will feature invited talks by established researchers in AI and a panel discussion focusing on career management.
Important Dates
All information is available on the consortium's web page.
NMR is the premier forum for results in the area of nonmonotonic reasoning. Its aim is to bring together active researchers in this broad field within knowledge representation and reasoning (KRR), including belief revision, uncertain reasoning, reasoning about actions, planning, logic programming, preferences, deontic reasoning, argumentation, causality, and many other related topics including systems and applications (see NMR page).
Topics of Interest
As in previous editions, NMR 2024 aims to foster connections between the different subareas of nonmonotonic
reasoning and provide a forum for emerging topics. We especially invite papers on systems and applications, as
well as position papers and papers addressing benchmark issues. The workshop will be structured by topical
sessions fitting to the scopes of accepted papers.
Important Dates
More information is available on the workshop's web page.
Computational models of argumentation are approaches that deal with the representation and interaction of arguments and counterarguments. These models can be applied in all areas that benefit from automatic decision-support such as medicine, accounting, chemistry, and law. Many of these models were inspired by works within the fields of non-monotonic reasoning and logic programming and therefore share the sometimes considerable computational complexity of these approaches.
Algorithmic aspects of computational models of argumentation are an important area, as witnessed by the popularity of the International Competition on Computational Models of Argumentation (ICCMA). This workshop aims at complementing the competition by providing a forum to present and discuss both systems and algorithms dealing with all aspects of computational argumentation, in particular those approaches addressing the tracks of the competition. A first workshop had been organised in 2016, a second one in 2018, a third one in 2020 and a fourth one in 2022.
This workshop welcomes technical contributions in all areas dealing with algorithms and systems of formal argument.
Topics of Interest
Topics of interest include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
Continuing the tradition of the previous years, FMCAD 2024 is hosting a Student Forum that provides a platform for students at any career stage (undergraduate or graduate) to introduce their research to the wider Formal Methods community, and solicit feedback.
Each student will give a short presentation and present their poster in the poster session.
Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing, and must be within the scope of FMCAD.
Topics of Interest
Topics of interest include (but are not limited to):
Important Dates
All information is available on the forum's web page.
Logic and strategic reasoning play a central role in multi-agent systems. Logic can be used, for instance, to express the agents' abilities, knowledge, and objectives. Strategic reasoning refers to algorithmic methods that allow for the development of good behavior for the agents of the system. At the intersection, we find logics that can express the existence of strategies or equilibria and can be used to reason about them. The LAMAS&SR workshop merges two international workshops: LAMAS (Logical Aspects of Multi-Agent Systems), 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 (Strategic Reasoning), 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, with a significant overlap in the participants and organizers of both events. For this reason, the two events have been unified under the same flag, formally joining the two communities. As such, the LAMAS&SR workshop aims to bring together researchers working on different aspects of either logic or strategic reasoning in computer science, artificial intelligence, and multi-agent systems research, both from a theoretical and a practical viewpoint.
Topics of Interest
The topics covered by LAMAS&SR include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
Reconfigurable Transition Systems (RTS) are dynamic relational structures (graphs) that evolve along its execution, in the sense that their accessibility relation, their set of nodes or their labelling change when their edges are crossed. These structures have proven to be suitable to compactly represent complex reactive and reconfigurable behaviours. Namely, the ability of reacting or readapting under the influence of certain events is a very distinctive feature of many diverse situations and objects. An autonomous vehicle that changes its route due to a new strike occurring, the behaviour of a software component after a memory disposal, or a DNA mutation as the result of a viral infection, are different examples that witness the importance of modelling about changes in a determined situation. Practical user cases have aroused the interest of the logic community in the study of variants of RTS, by developing formal methods to properly reason about such situations.
This workshop aims to bring together the whole community of researchers working on different ways to model reconfigurable and reactive systems from a formal perspective. This includes theoretical approaches (like hybrid logics, reactive frames, model-update logics), or formalisms designed for specific purposes (like separation logic in software verification, dynamic epistemic logic in AI planning, and others). Also, our goal is to devise novel approaches and potential applications, and share a common perspective on the discipline.
Topics of Interest
The scope of the workshop includes (but it is not limited to):
Important Dates
More information is available on the workshop's web page.
The European Summer School on Artificial Intelligence (ESSAI) is the premier school on Artificial Intelligence in Europe. It is held every year by the European Association for Artificial Intelligence (EurAI) together with the Advanced Course on Artificial Intelligence (ACAI), and it will be organized jointly with the 4th TAILOR Summer School on Artificial Intelligence.
ESSAI 2024 will offer many courses covering all areas of Artificial Intelligence and being taught by top experts in the field. Every course will consist of 5 lectures of 90 minutes each spread over one week. The courses will be solicited through an open call for proposals and will be selected by an international program committee. ACAI 2024 will offer invited tutorials (of 2x90min each) on a topic to be announced.
The provisional schedule of the school is available here.
Application
Deadlines
More information is available on the school's web page. If you have any questions, please reach out to the Local Chair Manolis Koubarakis.
Several professors at Nanyang Technological University are jointly advertising for several open PhD and postdoc positions in PL/FM at the School of Computer Science and Engineering, Nanyang Technological University (NTU), Singapore.
PhD positions are fully funded, and will be for the January 2025 or August 2025 intake at SCSE, NTU.
Details of the postdoctoral positions vary, but they are open to candidates with PhD-level qualifications in a range of topics in PL/FM. Please see below for further information on individual openings; interested candidates should contact us directly.
Luke Ong, Professor
We invite motivated and well-qualified candidates to work on Bayesian Statistical Probabilistic Programming, as
part of a research programme funded by the National Research Foundation, Singapore.
The appointees will work in the Probabilistic Programming Lab, where research is carried out on a wide range of topics, especially in the interface of programming languages, machine learning, and Bayesian statistics, but also in allied areas in semantics of computation, formal methods and verification, and in logic and algorithms.
Bayesian Statistical Probabilistic Programming lies in the interface of programming languages, machine learning, and Bayesian statistics. These positions will suit researchers with expertise in one (or more) of the three areas, and are interested and committed to collaborating with experts in the other areas.
Further details are available here.
Yang Liu, Professor
I have fully-funded PhD positions available for PL/SE/Security on web3 security (smart contract and runtime
monitoring), AV security and robustness, and Large Language Model (LLM) applications: applying LLM for FM
(specification/property generation, proof automation), LLM for security (vulnerability detection via static
analysis or fuzzing, vulnerability repair), LLM for SE (multi-agent software development), LLM security (prompt
injection, jailbreak, defence against LLM attacks).
Conrad Watt, Assistant Professor
I have fully-funded PhD positions available for PL research, broadly construed, related to the WebAssembly
programming language and virtual machine. A successful applicant will have the opportunity to work closely with
WebAssembly's industrial standards body and inform the future direction of the language.
I am also looking to recruit postdocs with experience in mechanised theorem proving and programming language semantics, to work on advanced extensions and applications of the WasmCert-Isabelle mechanisation of WebAssembly and related artefacts. A key theme of this work will be driving industrial adoption of verified artefacts - for example, see here. Experience with Isabelle/HOL would be highly desirable. Funding is available for up to 4 years of full-time employment.
Yong Kiam Tan, (incoming) Assistant Professor
I am interested in applications of deductive verification and interactive theorem proving in automated
reasoning, compilers (CakeML), randomized algorithms, hybrid systems, and cryptography. I am recruiting up to
three PhD students and three postdocs for these topics under a new Singapore NRF fellowship project.
Please visit this webpage for contact and other details.
Conrad and Yong Kiam would also like to draw attention to A*STAR's graduate scholarships. These competitive national awards offer enhanced support for exceptional PhD applicants, who we would jointly supervise in a project related to the intersection of WebAssembly and CakeML. Please contact us for more details.
We are looking to expand our research capacity in Logic/Semantics/Programming Languages/Verification at the University of Southampton and are looking to fill several academic positions at junior (fellowship), mid-career (lectureship) and senior (professor) levels. The links below give general specifications for the posts. Interested candidates are invited to contact Professor Ekaterina Komendantskaya to discuss the posts and opportunities at the University of Southampton.
We are excited to announce the availability of three postdoctoral researcher positions within the "CyPhAI: Formal Analysis and Design of AI-intensive Cyber-Physical Systems" project. We seek to develop mathematically rigorous methodologies for the modeling, verification, testing, monitoring, and control of cyber-physical systems (CPS) where artificial intelligence (AI) plays a pivotal role. This pioneering project is a collaborative effort between Japan teams led by Prof. Kohei Suenaga (Kyoto University) and Prof. Masako Kishida (NII) and the France team led by Prof. Thao Dang (CNRS), emphasizing international collaboration and interdisciplinary research in AI-CPS.
In this project, you will help advance the research in formal methods and control theories for AI-CPS and closely work with the leading researchers in Japan, Prof. Kohei Suenaga at Kyoto University in Kyoto or Prof. Masako Kishida at the National Institute of Informatics (NII) in Tokyo. You will also have opportunities to participate in several annual project workshops held in France or Japan to collaborate with the France team as well as other Japan teams.
Candidates must have or be near the completion of a PhD with research in relevant fields and demonstrate a track record of research publications, conference presentations, and software programming skills. Research experience in interdisciplinary collaborations is highly valued. The positions are heavily research-oriented. Selected candidates will be expected to independently conduct research tasks including but not limited to the following:
We welcome applications from foreign (non-Japanese) nationals. This project is funded by the Core Research for Evolutionary Science and Technology (CREST) program from Japan Science and Technology Agency (JST). Positions are to be filled on a rolling basis with flexible start dates. The initial contract will end at March 2025 with the possibility of extension up to March 2026, when the project will conclude. Compensation is determined on the basis of your qualifications according to the employment regulations in Kyoto University or NII, with social insurances covered by the hiring institutions.
Position Descriptions
Application Process
Please send your application by email with
the subject "CREST Job Application". Your application must include:
We will reach out for further materials and interview arrangements if your application aligns with our project needs.
If you have questions regarding the positions, please send your inquiries by email with the subject "CREST Job Inquiry".
Contact: Tayssir TOUILI
A PhD position is available in the "Institut de Recherche en Informatique Fondamentale" (IRIF), Paris, France.
The recruited PhD student is expected to investigate and develop novel techniques, algorithms and tools for malware detection. The ultimate goal is to build a malware detector that beats the existing commercial malware detection tools.
More details can be found here.
How to apply:
The position is available immediately. Candidates must have a master in computer science.
The candidate must send a CV, university grades, recommendation letters, and a motivation letter to Tayssir TOUILI.
The Cosynus team at LIX, CNRS & Ecole Polytechnique, France, invites applications for two 3-year PhD positions in formal methods for the analysis of robustness and explainability of neural networks. These positions are fully funded by the SAIF project (Safe Artificial Intelligence through Formal Methods) of the French National Research Programme on Artificial Intelligence PEPR IA.
The successful candidates will work under the supervision of Sylvie Putot and Eric Goubault and have the opportunity to interact with the other members of the SAIF consortium. The research topics can be refined based on the common interests of the candidate and the supervisors, and can be either more theoretically or practically oriented.
Candidates should have a strong background in computer science with an interest in formal methods, abstract interpretation/set-based methods, artificial intelligence, and possibly the application to cyber-physical and controlled systems.
The application should contain a motivation letter, an academic CV with transcripts, the contact information of two academic references (name, e-mail, and connection to the applicant), and be sent by e-mail at Sylvie Putot and Eric Goubault.
More information on the context of the thesis, practical conditions and the research topics can be found here.
Application deadline: June 25, 2024.
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 Mathematical Insights into Algorithms for Optimization (MIAO) group headed by Jakob Nordstrom, which is active at both the University of Copenhagen and Lund University on either side of the Oresund Bridge.
The MIAO research group has a unique profile in that we are doing cutting-edge research both on the mathematical foundations of efficient computation and on state-of-the-art practical algorithms for real-world problems. This creates a very special environment, where we do not only conduct in-depth research on different theoretical and applied topics, but where different lines of research cross-fertilise each other and unexpected and exciting synergies often arise. Much of the activities of the group revolve around powerful algorithmic paradigms such as, e.g., Boolean satisfiability (SAT) solving, Groebner basis computations, integer linear programming, and constraint programming. This leads to classical questions in computational complexity theory—though often with new, fascinating twists—but also involves work on devising clever algorithms that can exploit the power of such paradigms in practice. Our most recent new line of research is on how to verify the correctness of state-of-the-art algorithms for combinatorial optimization. Such algorithms are often highly complex, and even mature commercial solvers are known to sometimes produce wrong results. Our work on designing a new generation of certifying combinatorial solvers, which output not only an answer but also a machine-verifiable mathematical proof that this answer is correct, has already led to several prestigious international awards, but many more exciting problems are still waiting to be solved!
We are fortunate to be part of the Algorithms and Complexity Section at DIKU, which is world-leading in algorithms and complexity theory. DIKU hosts the Basic Algorithms Research Copenhagen (BARC) centre joint with the IT University of Copenhagen (ITU), and we also have extensive collaborations with the Technical University of Denmark (DTU) and with 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. While the focus in on foundational research, we do have a track record of surprising algorithmic discoveries leading to major industrial applications.
These positions are available for period of 3-5 years, depending on the current education level of the applicant. All our PhD positions are fully funded, employed positions (including travel money) that come with an internationally competitive salary. The starting date is flexible, but will be in October 2024 or thereafter.
The application deadline is July 1, 2024. Please see the full advertisement for more information and instructions how to apply. Informal enquiries are welcome and can be made to Jakob Nordstrom.
Do you want to carry out a PhD in program verification and proof assistants? And help to scale it up to the verification of realistic systems software?
You will be working on the semantics and verification of systems software (libraries for concurrency, efficient data structures, compilers, and/or operating systems) using type systems, separation logic, and proof assistants. As part of this PhD project, you will contribute to one or more topics:
As a PhD candidate you will use and contribute to the Iris and Coq projects. You will be supervised by Robbert Krebbers.
As a PhD candidate you will spend 10% of your time on contributing to teaching, and you will have the opportunity to develop yourself by taking courses, visiting summer schools, etc.
The start of the project is flexible, preferably in autumn 2024. If you have not fully completed your Master's studies but are excited about this position, please do not hesitate to apply or to contact us.
The application deadline is June 20, 2024. Please see the full advertisement for more information and instructions how to apply. Informal enquiries are welcome and can be made to Robbert Krebbers.
The University of Konstanz is one of eleven Universities of Excellence in Germany. Since 2007 it has been successful in the German Excellence Initiative and its follow-up programme, the Excellence Strategy.
The newly established research group in Formal Methods for Software Engineering at the University of Konstanz, led by TT-Prof. Emanuele D’Osualdo, is inviting applications for a PhD position or a Postdoctoral position in Formal Methods, Verification and Programming Languages:
Doctoral and Postdoctoral researchers have a status as employee with a salary according to the German federal employee scale TV-L E13.
The focus of the group is:
We look forward to receiving your application, consisting of a cover letter, list of references, curriculum vitae, copies of degrees, and, if applicable, list of publication, until June 30, 2024 (not strict). The starting date is as soon as possible. Please see the full advertisement for more information and instructions how to apply. Informal enquiries are welcome and can be made to Emanuele D’Osualdo.
One or two three-year PhD positions at the University of Lille, starting on September 1, 2024, as part of a European project.
These positions will focus on the intersection of:
Candidates should have, or be close to completing, a master’s degree in computer science or mathematics.
If you are interested in applying, please email David Nowak with a brief description of your background and research interests, along with your CV. Your CV should include the names and contact details of two references.
Candidates should have an excellent research track record and publications at top conferences in programming languages (e.g., POPL and ICFP) and/or security (e.g., CCS and CSF).
Candidates are expected to work collaboratively on topics of joint interest and to help co-advise students, but can also dedicate some of their time to their own independent projects. My research interests include, but are not limited to: formal verification, proof assistants (particularly Coq and F*), type systems, effects, monads, functional programming, parametricity, PL semantics, property-based testing, secure compilation, security against speculative side-channel attacks, noninterference, compartmentalization, capability machines, machine-checked crypto proofs, etc. You can find more details here.
MPI-SP is a relatively new research institute founded in 2019 and is part of the Computer Science research area of the Max Planck Society. We are located on the campus of Ruhr University Bochum, in the Rhein-Ruhr metropolitan region of Germany, one of Europe's largest academic hub. The working language of MPI-SP is English, and no knowledge of German is required for this job.
Do not hesitate to contact Cătălin Hrițcu if you are interested in this position.
The Research University in the Helmholtz Association creates und imparts knowledge for the society and the environment. It is our goal to make significant contributions to mastering the global challenges of mankind in the fields of energy, mobility, and information. For this, over 9000 employees of KIT cooperate in a broad range of disciplines in research, academic education, and innovation.
The Institute for Program Structures and Data Organization (IPD) within the Division II – Informatics, Economics, and Society – with its KIT Department of Informatics is seeking to fill, as soon as possible, the position of a University Professorship (W3) ``Programming Languages and Program Analysis''.
The professorship is intended to strengthen and expand KIT's expertise in the field of programming languages and software engineering. Research areas for this professorship include, for example, methods for the program analysis of security or correctness properties, the design and implementation of quantum programming languages or domain-specific languages, innovative concepts for parallel programming or compiler technologies.
In teaching, the professorship will contribute to the education of students of Informatics and other engineering courses at KIT. Significant participation in undergraduate teaching is expected.
The professorship will execute university tasks with a teaching obligation of 9 hours per week per semester and should participate in the KIT Center "Information - Systems - Technologies (KCIST)". In addition, active participation in the academic tasks of the KIT Department of Informatics and in the self-administration of the KIT in Division II as well as participation in the collegial institute management of the IPD is expected.
A distinguished scientist with excellent scientific qualifications and an international reputation in his or her field is sought. Skills in the acquisition of third-party funding and the management of scientific working groups are expected, as well as very good didactic skills.
Employment is subject to Art. 14, par. (2) of the KIT Act in conjunction with Art. 47 LHG Baden-Württemberg (Act of Baden-Württemberg on Universities and Colleges).
We prefer to balance the number of employees (f/m/d). Therefore, we kindly ask female applicants to apply for this job. Recognized severely disabled persons will be preferred if they are equally qualified. As a family-friendly university, KIT offers part-time employment, leaves of absence, a dual career service, and coaching to support the work-life balance.
Applications with the usual documents (curriculum vitae, list of publications, diplomas/certificates, teaching evaluations, presentation of previous and planned research and teaching activities, research, teaching and cooperation concept, presentation of own contributions in the above-mentioned fields, acquired third-party funds, statement on scientific honesty) are to be sent to the Karlsruhe Institute of Technology (KIT) by July 7, 2024, compiled in one PDF document by e-mail to Division II, Head of Division Professor Michael Decker. For further information, please contact Professor Dr. Ina Schaefer.
It is a pleasure and an honor to take over the edition of this newsletter, and I would like to thank the AAR board for trusting me in that role. Sophie Tourret took on this role for 7 years, and, together with her predecessors, has ensured that the newsletter became what it is today. I will do my best to keep its quality at the (high) level that the community deserves.
While most relevant calls for papers, workshops, etc., usually find their way to my mailbox, please feel free to bring to my attention any information you would like to see featured in the newsletter by writing an email. The newsletter is also a good place to post relevant job opportunities, book publications, new software, and open letters to the automated reasoning community.