The Herbrand Award for Distinguished Contributions to Automated Reasoning is the award established by CADE Inc. to honour a person or group of people for their exceptional work in the field of Automated Deduction. The award is named after the french mathematician Jacques Herbrand, and is given out annually at the respective CADE or IJCAR conference.
The Herbrand Award has been given in the past to:
At most one Herbrand Award will be given in each year. Nominations for the Herbrand award can be submitted at any time; the deadline for nominations to be considered for the Herbrand Award 2025, which will be given at CADE'30, is
February 28 2025Nominations pending from previous years must be resubmitted in order to be considered.
Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent via e-mail to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
In its meeting on December 16 2024, the CADE Inc. board of trustees has decided to update the procedure for deciding on the Herbrand award. The new award procedure, which applies from 2025, has two stages: nomination and decision by the Herbrand award committee. The award committee is established by the CADE Inc. board of trustees ahead of the nomination deadline.
The following rules apply for the nomination phase:
In 2025, the Herbrand award committee consists of the following people, listed here in alphabetical order:
The board of trustees reserves the option to exclude or replace committee members after receiving the nominations, in case a conflict of interest involving nominees and members of the award committee is identified.
For more details, please check the Herbrand Award webpage.
Automated Reasoning is the area of Computer Science dedicated to applying reasoning in the form of logic to computing systems. The Bill McCune PhD Award in Automated Reasoning distinguishes each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The award is named after the American computer scientist William Walker McCune, known for his contributions in the fields of Automated Reasoning, Algebra, Logic, and Formal Methods. He was the implementer of OTTER, Prover9 and Mace 4, automated tools for first-order reasoning which are known to this day for their accuracy and robustness. He was also known for his generosity towards research colleagues and as a great supporter of young researchers in the field.
Eligibility
Eligible for the award are those who successfully defended their PhD
Nomination
Candidates for the award must be nominated by their supervisor(s) and one additional independent researcher
who
reviewed/examined the thesis. Nominations are to be submitted via email,
by February 24, 2025 (Anywhere on Earth).
The nomination must consist of one compressed file (.zip) containing:
Procedure
The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of
Automated Reasoning.
Expert Committee
The Expert Committee, consisting of leading researchers in Automating Reasoning, is formed by the board of
CADE Trustees
with the aim to reflect the broad diversity in the area of Automated Reasoning. It is announced with the call
for
nominations, and thus formed before this call. The decision on the award is taken by the Expert Committee. The
Expert
Committee can seek additional expertise, even after the submission deadline for nominations. Expert Committee
members
cannot nominate a PhD student. Expert Committee members cannot contribute an independent report seconding a
nomination.
The Expert Committee for the Bill McCune PhD Award 2025 consists of the following people:
CSL is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
Co-located workshops
Two workshops are co-located with CSL, and will take place on Monday, February 10:
More information is available on the conference's web page.
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 computer science and mathematics, and implementations of automated reasoning systems are solicited. CADE-30 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction.
Important Dates (AoE)
More information is available on the conference's web page.
The TYPES meetings are a forum to present new and ongoing work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming.
Topics of interest include (but are not restricted to):
Important Dates (AoE):
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. This will be the 16th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988.
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 (AoE):
More information is available on the conference's web page.
The Programme Committee invites submissions for contributions on all aspects of logic, language, and computation. Work of an interdisciplinary nature is particularly welcome. The programme will include two plenary tutorials, four plenary invited lectures and two parallel tracks of contributed talks. In addition, there will be two topical workshops. More details will soon be made available via the TbiLLC website (see top).
Topics of interest include (but are not restricted to):
Important Dates (AoE):
More information is available on the conference's web page.
The scope of SAT 2025 includes all aspects of the theory and applications of propositional satisfiability broadly construed. This includes paradigms such as Boolean optimization using, e.g., MaxSAT and pseudo-Boolean (PB) solving, quantified Boolean formulas (QBF), satisfiability modulo theories (SMT), model counting, constraint programming (CP), and integer linear programming (ILP) for problems with clear connections to Boolean-level reasoning. This year the 31st International Conference on Principles and Practice of Constraint Programming (CP) will be co-located with SAT and will have deadlines and reviewing process synchronized with SAT 2025.
Topics of interest include (but are not restricted to):
Important Dates (AoE):
We invite proposals for workshops to be held immediately before the main conferences in Glasgow, UK. Workshops offer an opportunity for in-depth discussions, hands-on experiences, and focused exploration of specific areas connected to constraint programming, SAT solving, and related topics.
Given the co-location of the CP and SAT conferences, we especially encourage proposals for workshops of interest to both communities. Some example topics from recent years are pragmatics of constraint reasoning, constraint modelling and SAT/SMT encodings, counting and sampling, logic-based methods in ML, CP-SAT solving, proof complexity, certifying algorithms, and logic and search. Proposals of interest to a single community, either on previously covered topics or new topics, are also welcome.
While you are free to have a traditional workshop with submitted papers, we also encourage new ideas and formats that could foster more interaction from your audience. We encourage in particular short papers and position papers, a lightweight review process, and poster sessions.
Important Dates (AoE):
For inquiries and submissions, please contact the workshop chairs Zeynep Kiziltan and Marc Vinyals.
MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.
Topics of interest include (but are not restricted to):
Important Dates (AoE):
More information is available on the conference's web page.
Since the first conference In Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:
Affiliated Events
Important Dates (AoE):
More information is available on the conference's web page.
FMCAD 2025 is the twenty-fifth edition in a series of conferences on the theory and applications of formal methods in hardware and system verification. The conference encompasses a wide range of topics related to formal aspects of computer-aided system design, including verification, specification, synthesis, and testing and provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems.
FMCAD 2025 includes the FMCAD Student Forum and is co-located with VSTTE 2025.
FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer-aided design. Topics of interest include (but are not restricted to):
Important Dates (AoE):
More information is available on the conference's web page.
More and more mathematical information is digitally processed, generated, communicated, stored, and curated. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. Besides the CICM main program soliciting formal CICM submissions there will be associated workshops with separate submission options.
Topics of interest include (but are not restricted to):
Important Dates (AoE):
LFSA 2025 is a satellite event of CICM 2025. LSFA is an International Symposium on Logical and Semantic Frameworks with Applications launched in 2006. Logical and semantic frameworks are formal languages that represent logics and languages, as well as computational, AI and deductive systems. These frameworks provide mathematical foundations for the formal specification of systems and programming languages, supporting tool development and reasoning.
The LSFA series is a platform that fosters collaboration, bringing together theoreticians and practitioners. LSFA aims to promote techniques and results from the theoretical side, ranging from well-established ones such as lambda calculus and type theory to state-of-the-art ones such as machine learning, and provide feedback on integrating, implementing and using such methods and results from the practical side.
Important Dates (AoE):
More information is available on CICM 2025 and LSFA 2025 web pages.
We invite all members of the international AI research community to submit their best work to the 28th European Conference on Artificial Intelligence, which will take place in the historic city of Bologna from October 25 to 30, 2025.
We welcome submissions on all aspects of AI. Submissions will be subject to double-blind peer review by the programme committee. They will be evaluated based on relevance, clarity, significance, originality, soundness, reproducibility, scholarship, and quality of presentation.
The conference is planned as an in-person event. Each accepted paper will get assigned either an oral presentation slot or a combined poster/spotlight presentation slot. The presentation modality is not intended to reflect perceived scientific quality of the paper, so this assignment will be made in a randomised fashion (subject to programme constraints).
Submissions on all aspects of AI are welcome. This includes in particular:
Important Dates (AoE):
More information is available on the conference's web page.
The aim of JELIA 2025 is to bring together active researchers interested in the use of logics in Artificial Intelligence, in order to discuss current research, results, problems, and applications of both theoretical and practical nature. JELIA strives to foster links and facilitate cross-fertilization of ideas among researchers from various disciplines, among researchers from academia and industry, and between theoreticians and practitioners.
Topics of interest include (but are not restricted to):
Important Dates (AoE):
More information is available on the conference's web page.
The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) brings together researchers interested in all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods.
Topics of interest include (but are not restricted to):
Important Dates (AoE)
More information is available on the conference's web page.
RuleML+RR 2025 is a leading international joint conference in the field of rule-based reasoning. One of the main goals of RuleML+RR is to build bridges between academia and industry in the area of semantic reasoning.
RuleML+RR 2025 aims to bring together researchers and practitioners interested in the foundations and applications of rules and reasoning. It provides a forum for stimulating cooperation between different communities focused on the research, development, and applications of rule-based systems. We solicit high-quality papers related to theoretical advances, novel technologies, and applications that involve rule-based representation and reasoning or other declarative forms of artificial intelligence.
Topics of interest include (but are not restricted to):
The conference will also include the following events:
Important Dates (AoE):
More information is available on the conference's web page.
Software plays an increasingly important role in scientific and engineering disciplines. Climate modeling, weather prediction, drug discovery, the design of buildings, vehicles, and aircraft, simulations of astrophysical phenomena, and prediction of seismic activity are some of the many applications. Verification of such software presents numerous challenges, e.g.: the programs are large, complex, and utilize multiple CPU and GPU concurrency interfaces; precise reasoning about real or floating-point operations is often required; there is often no oracle; and correctness may require reasoning about deep mathematical concepts such as convergence and stability. This workshop will focus on verification techniques that address these challenges, including approaches based on deductive reasoning, model checking, symbolic execution, abstract interpretation, and static analysis.
The workshop will take place as part of ETAPS 2025, on Sunday, May 4, 2025, at McMaster University in Hamilton, Canada. We aim to bring together researchers from both the scientific computing and the software verification communities. Through invited talks and presentations of peer-reviewed papers, participants will learn about the correctness challenges developers face, as well as a variety of verification approaches for tackling those challenges.
We are interested in all aspects of the verification problem for scientific software, including, but not limited to:
Important Dates
More information is available on the workshop's web page.
Blockchain is a novel technology to store data in a decentralized way. Although the technology was originally invented to enable cryptocurrencies, it quickly found applications in several other domains.
Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are stored on the blockchain and that run on the network. They can interact with the ledger’s data and update its state. These scripts can express the logic of possibly complex contracts between users of the blockchain. Thus, Smart Contracts can facilitate the economic activities of blockchain participants.
Since blockchains are often used to store financial transactions, bugs may result in huge economic losses and thus it is now of utmost importance to have strong guarantees of the behaviour of blockchain software. These guarantees can be brought by using Formal Methods. Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools is relevant: consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to write smart contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc.
Topics of interest include (but are not restricted to):
Important Dates
More information is available on the workshop's web page.
The aim of this workshop is to bring together experts in proof theory with specialists in formal mathematics and automated theorem proving, in order to facilitate an interdisciplinary exchange of ideas on the mutual benefit that these areas can have on one another. On the one hand, the workshop will focus on how methods from proof theory, such as advanced techniques aimed at extracting computational content from large scale nonconstructive proofs in mainstream mathematics, can be implemented and partially automated within theorem provers. In the other direction, we will explore whether the rich variety of logical systems developed by proof theorists could benefit the world of formal mathematics by both simplifying and streamlining the formalisation process.
We welcome 30 minute contributed talks on any topic broadly within the scope of the workshop. We are particularly interested in work that explores the following themes and their intersection:
Presentations from research students and early career researchers are particularly encouraged. To propose a talk, please submit your title and abstract by email to one of the organizers. We put no restrictions on the originality or publication status of submissions. There will be no formal proceedings.
Important Dates
Details about registration, along with local information, are available from the main ESSLLI webpages. As a part of ESSLLI, our workshop benefits from the funding opportunities offered for PhD students for the whole event. More information is available on the workshop's web page.
For 23 years, the Oregon Programming Languages Summer School has been devoted to teaching the principles of programming languages to students and professionals. Although the topics vary from year to year, the unifying theme is the importance of fundamental theory to the design and implementation of programming languages, the development of program verification tools, and the application of advanced programming languages to practice. The summer school attracts participants from around the world, and is often able to subsidize the participation of qualified attendees with limited resources. More than a thousand participants have attended OPLSS since its inception in 2002. The summer school is sponsored by the National Science Foundation, and by generous grants from numerous companies over the years.
The program takes place over two weeks, with ample time for group and private study, and to take advantage of the many recreational opportunities around Eugene. The sessions are non-overlapping, so participants will have the opportunity to attend all lectures. Each lecture is 80 minutes, including time for questions.
The registration deadline is March 14, 2025.
More information is available on the school's web page.
Machine learning (ML) and logical reasoning have been the two foundational pillars of AI since its inception, yet it is only in the past decade that interactions between these fields have become increasingly prominent. Notably, ML has had a dramatic impact on SAT and SMT solvers, as demonstrated by the award-winning SATzilla, MapleSAT, and Z3alpha solvers. Our tutorial aims to inspire new interdisciplinary research by bridging the gap between ML and logical reasoning research communities. We will introduce the broader AI community to ML techniques that have been used in the context of logical reasoning solvers, with a sharp focus on approaches that are successful and promising. We will also host a panel discussion on how LLMs may shape this area going forward.
Rather than pure end-to-end learning, successful ML approaches tend to be tightly integrated with symbolic solvers. The central thesis of our tutorial, supported by numerous successful cases, is that ML excels best when it is used to sequence, select, initialize, and configure proof/rewrite rules that solvers implement. One prominent example that we will highlight is the use of ML for learning branching heuristics, both online for particular instances using reinforcement learning (RL) and offline training a neural network policy across representative instances from a particular application.
There will be theory, hands-on lab, and panel discussion on the use of ML for solvers.
More information is available on the tutorial's web page.
A Special Session on Proof Assistants will be held as part of the 2025 North American Annual Meeting of the Association for Symbolic Logic. The whole ASL meeting will take place May 13-16, while the special session on proof assistants will take place on the last two days May 15 & 16.
There is some limited capacity for contributed talks (duration approx. 20 minutes). The deadline for contributed talk submissions is Thursday, February 27, 2025. Abstracts should be sent to Jonathan Weinberger and Patricia Johann. Reviewing of abstracts will be lightweight.
More information is available on the meeting's web page.
VerifyThis is a series of program verification competitions, which has taken place annually since 2011 (with the exception of 2020). Previous competitions in the series have been held at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015-2024. The challenge problems and solutions of previous competitions are available in the archive.
The aims of the competition are:
The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
To be able to offer a broad and diverse set of verification challenges, we are collecting submissions of ideas for verification challenges and problems. We welcome both problems of academic interest as well as challenges based on themes that are relevant in industry.
The competition proceeds in three rounds. In each round, participants are given 60 - 120 minutes to implement and prove specified properties of a given algorithm and/or data structure. They are free to use any verification tools they choose. Challenges are typically concerned with proving functional properties of the code in question (at least some part of a challenge involves expressing and proving properties specific to the algorithm/data structure in question). It is common for problems to have multiple parts, e.g. to prove some basic properties first, perhaps for a simplified case, and to progress to more-advanced goals.
We are currently looking for problem submissions! If you have recently encountered an interesting challenge in your work where formal techniques could be applied, please don't hesitate to submit it. Typical challenges have clear input-output specifications and often incorporate one or more of the following: heap allocation, concurrency, arithmetic reasoning. A challenge usually describes a problem using natural language together with some pseudocode, and then provides a list of properties or "verification tasks" of varied levels of difficulty. Contributors are encouraged to look at the Archive of previous problems.
An award will be given for any submission used in the competition. To avoid spoiling the competition for others, we ask that you keep the subject of your submission private. However, note that problem authors are allowed to participate in the competition!
A submission should consist of:
Contributors are encouraged to look at the archive of previous problems. Submissions should be sent by email to Jenna DiVincenzo and Thomas Wies. The submission deadline is February 7th, 2025. We look forward to receiving your ideas!
More information can be found on the competition website.
The Naval Postgraduate School (NPS) is accepting applications for a Faculty Associate - Research in the Department of Computer Science (non-tenure track). We are especially interested in candidates with strong recent experience in software development for data science/AI/ML, especially with background and/or interest in natural language processing and linguistics. In particular, the work is centered around representation and reasoning in first-order logic and beyond.
We seek applicants with the following skills and experience:
We aim to fill the position by July 2024 and will begin reviewing applications starting 01 June 2024. Please find more information about the requirement and how to apply on this link.
Feel free to contact Adam Pease for more information.
We are pleased to announce that a PhD project is open with Dr. Charles Grellois (primary supervisor) and Dr. Harsh Beohar at the University of Sheffield. The title is the following: “Model-Checking of Functional Programs: from Theory to a Theorem Prover Implementation” (3.5 years). For more details on the project and how to apply, please visit this link.
Candidates are encouraged to get in touch by email. The application deadline for applicants is 5pm Wednesday 29th January 2025.
We invite applications for a four-year PhD studentship on the Leverhulme-funded project "ECUMENICAL: Proof-theoretic semantics for non-classical and modal logics," led by Dr. Elaine Pimentel, Prof. David Pym, and Prof. Luiz Carlos Pereira at UCL Computer Science, UK.
This interdisciplinary studentship, situated at the intersection of informatics, mathematics, and philosophy, is open to UK (home) students. The research will focus on developing proof-theoretic semantics for non-classical and modal logics, constructing the necessary abstract mathematical meta-theory, and investigating the implications of inferentialist semantics for systems verification. The project will build on recent advancements at UCL, including connections between the proof-theoretic foundations of logic programming and base-extension semantics, with potential exploration of applications to simulation modelling and its inferentialist interpretation.
The successful candidate will work closely with Dr. Elaine Pimentel (Computer Science), Prof. David Pym (Computer Science and Philosophy), and Prof. Luiz Carlos Pereira (Philosophy, UERJ Brazil). The student will be based within the Programming Principles, Logic, and Verification group at UCL Computer Science.
Application deadlines are the 3rd of February 2025 (for a May 2025 start) and the 1st of July 2025 (for an October 2025 start). More information can be found on the University's web page.
The department has expertise in quantum programming languages and quantum computing, with a strong focus on leveraging methods from type systems, programming language theory, category theory, and theorem proving.
Interested candidates are encouraged to contact Frank (Peng) Fu directly. The application deadline for Fall 2025 is February 1, 2025.
For more information about the Ph.D. application process, see the admission page.
The Programming Language Foundations Lab at ETH Zürich is looking for strong students that want to do research at the foundations of programming language theory, in program verification and separation logic, with a focus on Rust. Some experience with formal methods and PL theory is expected (e.g. from a suitable course); knowledge of interactive theorem provers or Rust is greatly appreciated but not required. Candidates need to have a master's degree.
Interested candidates should send an email to Refl Jung. Please explain why you are interested in a PhD in this field and what your prior experience is. Also include a CV and possible contacts for recommendation letters. Applications are considered on a rolling basis, so there is no fixed end date for this call, but if you want to be sure the position is still open then please submit your applications until the end of February, 2025.
See the Group's webpage for further information.
We seek to hire a full-time postdoctoral researcher in the area of formal methods for security and privacy. The University offers:
The successful candidate is expected to contribute to the PROVTOPIA project, which focuses on counteracting disinformation via Secure and Private Provenance Verification of Media Content. The candidate will work under the umbrella of the Crises research group under the direction of Dr. Rolando Trujillo. Include in your application the following documents:
Deadline for applications is 15 February 2025. Early applications are highly encouraged, though, as they will be processed upon reception. You can contact Dr. Rolando Trujillo for more information.
Virginia Tech's Systems Software Research Group (https://www.ssrg.ece.vt.edu) invites applications for paid internships from undergraduate and graduate students on a verified compilation project. The project goals include building a formally verified framework for the Linux eBPF mechanism, including language, type system, and a verified compiler, for writing safe and correct eBPF programs.
Preferred qualifications:
The starting date and time frame is flexible. Please contact Swarn Priya with a resume or for any questions.
The MaREL research team (part of the LIRMM laboratory, a leading French research laboratory) specializing in Software Engineering is looking to recruit a new permanent member holding a PhD or an equivalent doctoral degree. The MaREL team aims to recruit for an Associate professor/Lecturer-Researcher (Maître de conférences) - Affiliated with the University of Montpellier, part of the MaREL team and the Computer Science Department of the Faculty of Sciences at the University of Montpellier.
The MaREL team is a research group within the LIRMM laboratory. It focuses on software engineering, particularly the automation of tasks related to all stages of the software lifecycle. The team seeks to strengthen its research areas, especially in the application of statistical and symbolic artificial intelligence techniques to address challenges in software development, maintenance, and evolution. Expertise in applying these techniques to problems such as software re-engineering for migration towards software product lines or microservices, or program verification, will be highly valued. The team is also actively involved in industry transfer activities.
Please contact please contact Abdelhak-Djamel Seriai (head of the MaREL team) if you want more information about the application's process.
Hasuo Laboratory at the National Institute of Informatics, Tokyo, Japan invites applications for postdoc and senior researchers. The candidates will pursue collaboration with Bart Jacobs (Nijmegen), Joost-Pieter Katoen (Aachen), and Sam Staton (Oxford). The positions are for 4.5 years max.
This is a call for researchers at the JST ASPIRE project without specified topics. Relevant backgrounds include (but are not restricted to) formal methods, mathematical semantics, category theory, software science, programming languages, mathematical logic, control theory, machine learning, and optimization. Familiarity with formal logic is mandatory.
Please consult the project's webpage for scopes, details, and how to apply.
Ph position are also available. Please consult this webpage for more information.
We look forward to applications from junior and senior researchers with aspiring minds. Thanks a lot for your consideration!
The Department of Computer Science at the University of Surrey is seeking to recruit a full-time postdoctoral research fellow to work on a range of topics in the areas including:
The successful applicant will work in a multidisciplinary team, as well as a large team of academic (Imperial, MPI-SWS, Cornell, IMDEA) and industrial collaborators (Arm, NVIDIA, Galois), researchers and PhD students.
Applicants must have or be close to obtaining a PhD in Computer Science.
The application deadline for applicants is January 31st, 2025. You can apply on the University's web page. For informal enquiries and further information please contact Brijesh Dongol or Gregory Chockler.
The Faculty of Sciences of the Université libre de Bruxelles (ULB) invites applications for a full-time academic position in Computer Science to begin October 1st, 2025. All areas of Computer Science will be considered. Candidates who can strengthen an existing team within our department are particularly encouraged to apply.
The Computer Science Department of ULB is a leading research and dynamic education center. Located in the capital of Europe, it offers a wide range of funding and research opportunities. Brussels is a cosmopolitan city with an excellent quality of life and easy access to all major cities in Europe. The position involves both teaching and research and some commitment to administrative tasks.
For more information, (e.g. concerning courses to be taught or the research carried out in the Department), please contact Mr John Jacono, Head of the Computer Science Department.
The application deadline for applicants is March 15, 2025. You can apply on the University's web page.
The Faculty of Mathematics, Informatics and Mechanics of the University of Warsaw (MIM UW) invites applications for the positions of Assistant Professor in Computer Science, starting on 1st October 2025 or 1st February 2026.
MIM UW is one of the leading Computer Science faculties in Europe. It is known for talented students (e.g., two wins and multiple top tens in the ACM International Collegiate Programming Contest) and strong research teams, especially in algorithms, logic and automata, algorithmic economy, and computational biology. There is also a growing number of successful smaller groups in diverse areas including cryptography, databases and knowledge representation, distributed systems, and machine learning. Seven ERC grants in Computer Science are running at MIM UW at the moment.
In the current call, 7 positions are offered (follow the links for more details):
The deadline for applications is February 14, 2025. For further information about the procedure, requirements, conditions, etc., please contact Filip Murlak or Oskar Skibski.
Cryspen is on a mission to build high-assurance software and formal verification tools that make the world a safer place. We're looking for passionate Proof Engineers to join our collaborative team and help us achieve that goal.
Are you proficient in Rocq (ex Coq) or F* or Lean or HOL? Have you built or maintained large proof artifacts? Do you have experience in improving proof automation or developing verification tools? Are you eager to apply formal verification to real-world software?
If your answer is yes, apply and tell us more about your experience and your interests.
For more information about the jobs, please visit the job offer's page.