➕ Springer is recognised as a long-standing, reputable publisher and publishing with LNCS/Springer is a sign of quality in a lot of disciplines.
➕ This is important for how publications are evaluated in grant application panels, national research evaluation panels, and University promotion/appointment panels. These panels are broadly composed and may not include people who have heard of CADE, IJCAR, LIPIcs or Schloss Dagstuhl. But they will have heard of Springer. The difference in scale is evident from the venue statistics provided by DBLP:
➕ Springer provides faster indexing and a larger number of indexing services than LIPIcs:
➖ The costs associated with these services need to be covered and are paid for through library subscriptions and Gold Access charges.
➕ Our current deal for Springer Open/Gold Access for conference proceedings of CADE, IJCAR, TABLEAUX and FroCoS is moderately priced (200 Euros) and includes sponsorship for CADE and IJCAR which amounts to 10 free papers. The costs are a bit higher than for LIPIcs but not significantly so and a fraction of the costs of individual author Open Access charges.
➕ The Green Access option would remove author publication costs. Green Access means that authors are allowed to make their papers available via their home pages or their institution's repositories. For many authors Green Access is enough.
➕ Minimal editorial work for PC Chairs.
➖ Type-setting: It is unfortunate that the author guideline/style files don't seem to agree with the style files that are eventually used in production. Some authors understandably get very worked up about this, since they have put so much effort in the preparation of the final versions of there papers. But all journals do type-setting that will make some changes which are normally cosmetic and small. If bugs are introduced during typesetting then these are identified by the authors and fed back to the publisher. I don't have problems with the type-setting in LNCS. An experience with the publishing process for a conference in another discipline (not LIPIcs) has been an eye opener how well-organised and hands-off Springer type-setting and copy-editing is in actual fact. Improving instructions and reducing type-setting changes that depart from author style files is however something we should continue to raise with Springer.
➕ It will be unfair on our communities to be disadvantaged while we all use our energy to make sure LIPIcs is recognized in committees. These things can take many years, generations even, to achieve. LIPIcs is still small, even in Computer Science.
➕ Some of our main competitor conferences (CAV, TACAS) continue to publish with Springer. It might put CADE at a disadvantage if we move to LIPIcs while they remain with Springer.
➕ It would be awkward if CADE moves to LIPIcs, but IJCAR stays with Springer. Similar, it would be awkward if CADE and IJCAR both move to LIPIcs, but FroCoS and Tableaux stay with Springer. So a move would only be feasible if CADE, IJCAR, FroCoS, and Tableaux all move to LIPIcs. But it is not clear whether LIPIcs would agree with that.
Conclusion
All in all, while we can secure a good Open Access Deal with Springer and since rankings, impact factors and publisher visibility/reputability play such a large role in the way that money is allocated, who gets tenure, who is promoted, etc, having LIPIcs publications will not be as beneficial as having Springer publications. Although such criteria should not play a role in evaluations, in practice they do. It is our responsibility to think of our young researchers, people without tenure and active researchers applying for grants and do what is best for them and the field.
LIPIcs is a high-quality publisher of conference proceedings. It has many advantages compared to the status quo. Below are some arguments in favor of LIPIcs.
➕ All articles published by LIPIcs are Open Access.
➕ The interaction with authors and conference chairs is professional and efficient.
➕ The same style file is used for submission and publishing. Authors know exactly how their article will look like when it will be published.
➕ Opt-in changes. The LIPIcs typesetters will propose changes if they encounter issues. However, it is up to the authors to decide which of these changes to apply. If authors don't respond, then the article will be published as submitted. This is a big contrast to Springer, which makes seemingly random modifications that authors need to detect and report.
➕ The cost per article is 60 euro, which is substantially cheaper compared to alternatives.
➕ LIPIcs focuses on quality, while Springer focuses on quantity and cheap labor.
➖ LIPIcs does not produce a HTML version of the paper, which is part of the reason why they can offer a lower price. LIPIcs assumes that papers are on average 20 pages, including bibliography and appendices. If the average page count is higher (which is not the case for CADE/IJCAR), then a slightly higher price needs to be paid.
➕ The LIPIcs timeline is somewhat shorter compared to other publishers. This provides more flexibility for the reviewing window. It also ensures that the proceedings are available during the conference (which is not always the case with Springer).
➕ Related conferences have been moving to LIPIcs in recent years. Examples are FSCD (2016), ITP (2019), CP (2021), and SAT (2022). Note that various conferences that are ranked higher than CADE (according to Best Computer Science Conferences) moved to LIPIcs. For example, CADE is ranked 824 while SAT is ranked 441 and CP is ranked 557.
Conclusion
It's disheartening to observe how Springer shifted its operational strategy to prioritize profit over quality. This was markedly evident when they outsourced typesetting and correction tasks to a cheap-labor country. Moverover, Springer expanded the LNCS proceedings indiscriminately, welcoming conferences of all tiers that are willing to put their papers behind the paywall. This strategy, aimed at augmenting revenue streams from universities and funding agencies, has eroded the prestige once associated with LNCS in particular and Springer in general.
In stark contrast stands LIPIcs, a non-profit publisher that champions uncompromising quality standards and a staunch commitment to Open Access. Switching to LIPIcs enhances the author experience and elevates the quality of the proceedings. It's time to align with our related conferences in embracing publishers like LIPIcs, who are shaping the future of academic publishing through their integrity and dedication to accessibility and quality.
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.
The members of the board of trustees until the 2023 elections were:
The terms of the elected trustees Marijn Heule, Andrew Reynolds, and Renate Schmidt ended. The term of office of Brigitte Pientka as CADE-29 programme chair ended after the CADE conference, and Christoph Benzmüller is joining the board of trustees as IJCAR 2024 program co-chair.
In the 2023 elections, three new trustees had to be elected.
The following candidates were nominated and their statements, in alphabetical order, are below:
The election was carried out using the Condorcet Internet Voting Service (CIVS), and the Condorcet completion Minimax-PM. Participants of the last three CADE/IJCAR conferences (who paid registration fees at at least one of the conferences) were invited to vote, and a total of 301 ballots were sent out on September 5. By September 25, 79 CADE members had voted through CIVS, which translates to a participation rate of 26.2% (as compared to 26.7% in 2022, 26.7% in 2021, 34.5% in 2019, 21.1% in 2018, 9.1% in 2017, 11.2% in 2016).
The results of the election can be viewed on CIVS:.
The three candidates elected are Jasmin Blanchette, Carsten Fuhs, and Renate Schmidt.
The new board of trustees is therefore:
On behalf of CADE Inc., I would like to thank Marijn Heule and Andrew Reynolds for their service on the board of trustees since 2017. I would like to congratulate Jasmin Blanchette and Carsten Fuhs, who will join the board as new elected trustees, and Renate Schmidt on being reelected. Finally, I would also like to thank Uwe Waldmann for running in the elections.
My research focuses on the automation of higher-order logic. I work mainly on the proof assistant Isabelle/HOL and the automatic theorem prover Zipperposition. My goal is to make proof assistants less laborious to use by improving their build-in automation and by integrating automatic provers.
I have a history of service in the community. I have chaired IJCAR, CPP (Certified Programs and Proofs), ITP (Interactive Theorem Proving), and TAP (Tests and Proofs). I have also served as a CADE trustee from 2016 to 2019 and, ex officio, in 2021 and 2022. I have attended most installments of CADE and IJCAR since 2009 and consider it my home conference.
As a CADE trustee, I would work towards ensuring that CADE and IJCAR remain open to a wide range of deduction techniques and feature a healthy mixture of theory and practice. I believe this is best achieved by having at least two program chairs who have complementary backgrounds.
I would also argue in favor of systematizing the CADE practices. Program chairs should have clear guidelines and templates they can work with. Important matters such as the use (or not) of rebuttals should be settled by the board of trustee, instead of being left to each year's chairs to decide. A permanent repository of knowledge for use by program chairs should be set up, containing instructions about processes, template emails, etc.
Finally, we must increase the conference's impact and prestige. According to the CORE index (which has an impact on many researchers' careers), CADE and IJCAR are ranked A ("excellent conference"). There are specific measures we could take to obtain the top grade, A* ("flagship conference"). I would be in favor of doing what it takes to achieve this.
I am honoured by the nomination to serve on the CADE board of trustees. CADE and IJCAR are among the main conferences that I regularly attend. I have published at both conferences, been on the PC of CADE-29 in 2023, and served on the expert committees for the Bill McCune PhD award since its inception in 2020.
My own research is firmly rooted in automated reasoning and deduction, with push-button termination analysis, inference of complexity bounds and checking program equivalence in various computation formalisms as my main foci. Thus, my research connects the use of methods and tools in automated deduction (e.g., SAT and SMT solvers) with applications in program analysis. I am one of the main developers of the program verification tool AProVE.
I am currently serving as Publicity Chair in the Steering Committee of the neighbouring International Conference on Formal Structures for Computation and Deduction (FSCD). I think that the co-location of CADE and FSCD in Rome in 2023 with 24 joint registrations has been a big success: it has allowed for cross-fertilisation between our closely related communities and for reducing the need for frequent long-distance travel with its downsides on individual level in the short term and on planetary level in the medium term. Therefore, I would advocate for further co-location of CADE with related conferences such as FSCD or CAV in the coming years.
In a similar vein, I strongly believe that the option of hybrid participation and also presentation as implemented at CADE/FSCD in Rome should be upheld. This lowers the entry barrier for participants and authors who cannot spend financial and time resources on a week far away from home obligations. Reasons may include being a parent or carer, living in the developing world, being a taught student considering going into research, or simply being interested only in specific presentations.
There have been concerns that the online option of a hybrid event might dissuade many professional researchers from attending in person. However, the lively in-person interaction at CADE/FSCD in 2023 seems to indicate that these concerns are unfounded. At the same time, an observation at FSCD 2023 was that 10% of the presentations would not have been possible without the option for remote presentation. This shows that a hybrid event can increase the quality of the programme and broaden the reach of the conference without detrimental effects on the overall conference experience for in-person participants.
In regards to the publication model of CADE, I consider making the conference proceedings available as open-access publications, as in 2023, to be the right way forward. To keep the financial entry barrier for authors low and to ensure that the quality of submission remains the sole criterion for publication, I think that it is important that funding by CADE for authors to cover open-access fees should continue to be available as needed. Here a sensible balance needs to be struck between attendance fees paid by all participants and open-access publication fees paid by the authors.
Finally, I am in favour of initiatives that support young researchers who are trying to establish themselves in the CADE community and in academia. This includes the Woody Bledsoe Student Travel Award for making attendance of CADE possible for students and the Bill McCune PhD award for distinguishing the contributions of a recent PhD thesis in automated reasoning, thus helping to kickstart the academic career of a promising researcher in the CADE community towards a permanent position.
As a previous member of the CADE Board of Trustees I appreciate its importance in securing good conference locations, appointing PC Chairs, constituting award committees, ensuring the success of various other activities in our area and providing leadership and representation for the area of automated reasoning. I have experience in chairing the CADE, FroCoS and TABLEAUX conferences and am PC-CoChair of IJCAR 2024. I am also founding organiser of the PAAR workshop series and am Editorial Board member/Associate Editor of the Journal of Automated Reasoning, the Artificial Intelligence Journal and the Journal of Artificial Intelligence Research.
This varied experience gives me a broad perspective on issues and concerns in our community and will allow me to continue be a strong advocate for the interests of automated deduction, its future and integrity in all our processes. I would be honoured to serve on the CADE Board of Trustees for another term.
My background: My main research involves the development and theoretical analysis of reasoning methodologies and automated reasoning tools as well as applying these in areas such as artificial intelligence, knowledge representation, agent-based systems and mathematics. At present a very strong focus of my work is the development of tools 1) for forgetting, content extraction, abductive learning and query answering in the context of ontology-based languages, and 2) for tableau synthesis, uniform interpolation and automated correspondence theory in the context of non-classical logics.
I feel honored to be nominated for the CADE Board of Trustees. Working mainly on saturation-based proof calculi and systems, I consider CADE my home conference. I had my first CADE paper in 1996, visited almost every CADE since 1990, and participated in 8 of the last 11 CADE and IJCAR program committees.
I am generally happy with the development of CADE in the last decades. The regular alternation between CADE and IJCAR, the co-locations with other conferences, and the large range of workshops are important to foster cooperations with researchers from neighboring communities. Measures to support and promote young scientists help to keep the field of automated deduction alive and should be continued. To remain the leading conference in our field, the spectrum of possible topics for CADE must stay broad and theoretical papers, practical papers, and application papers must be equally welcome. In order to attract scientists from outside Europe, it is also important that CADE takes place on other continents on a regular basis
There seems to be a general consensus that moving to open access CADE proceedings was the right decision, both because it improves the accessibility of our research and because some funding agencies insist on it. When we look at the details, however, we encounter conflicting interests. While for some authors the visibility of the publication and the publisher's prestige are paramount, others place a greater emphasis on low publication fees and would prefer do not feel screwed by the publisher's copy editors. We must find a reasonable compromise in this matter.
The International Joint Conference on Automated Reasoning (IJCAR 2024) is soliciting proposals for satellite events such as workshops, tutorials and competitions.
Researchers are invited to submit proposals on any topic related to automated reasoning, from theoretical foundations to tools and applications.
The satellite events will take place before the IJCAR conference on Monday & Tuesday, July 1-2, 2024.
Proposals can have up to three pages and should consist of the following two parts.
The organisers of satellite events are expected to create and maintain a website for the event; handle paper selection, reviewing and acceptance; draw up a tentative programme of talks; advertise their event through specialist mailing lists; prepare the informal pre-proceedings (if applicable) in a timely fashion; plan for remote participation (if applicable); and arrange post-proceedings if any.
The IJCAR organising committee will handle promotion of the event on the main conference website; integration of the event's programme into the overall timetable; registration of participants; arrangement of an appropriate meeting room; and provision of lunch and coffee breaks for participants.
Important Dates
Proposals should be sent directly to Sophie Tourret by email.
[*] A zoom connection can be provided on demand.
The 30th Conference on Automated Deduction will take place in Stuttgart (Germany). The conference chair is Stephan Schulz and the tentative dates for the conference are late July or August 2025.
UNESCO has proclaimed January 14th as World Logic Day, a global day dedicated to supporting the development of logic through teaching, research, and the public dissemination of the discipline. To this end, we would like to invite all of you to organize events -- possibly small ones -- around January 14, 2024, to celebrate this special day.
The coordination of World Logic Day 2024 is -- for the 4th time -- in the hands of the Conseil International de Philosophie et des Sciences Humaines (CIPSH) and its member organization, the Division for Logic, Methodology and Philosophy of Science and Technology of the International Union of History and Philosophy of Science and Technology (DLMPST/IUHPST):
We have learned over the last years that online meetings are easier to finance, better for the environment, and considerably more inclusive. So consider both in person and online events.
Events will be listed on the CIPSH website.
To be added to that list, follow the instructions here or write a short email.
This year, iFM 2023 and its associated events will be held in Leiden, The Netherlands, on 13-16 November 2023. The four-day event consists of the main conference iFM 2023, the workshop on Formal Methods for Autonomous Systems (FMAS 2023), a PhD Symposium and an artifact session. The programme will include the following keynote and invited speakers:
More information is available on the conference's web page.
We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend.
The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.
More information is available on the workshop's web page.
This special issue aims at providing an overview of recent work in automation of expressive non-classical logics, AI-related applications thereof, and discussions of perspectives in explicit symbolic knowledge representation and reasoning in contemporary AI applications regarding, but not limited to, the following topics:
Technical contributions (of up to 20 pages), abstracts (4 pages), e.g., on doctoral theses or habilitations, system descriptions (4-6 pages), project reports (4-6 pages), or discussion articles (4-8 pages), are welcome. All submissions will be peer-reviewed.
Extended submission deadline: December 18, 2023.
The full CfP can be found here (but please ignore the old deadline).
If you have any questions, please do not hesitate to contact Alexander Steen.
IJCAR is the premier international joint conference on all topics in automated reasoning.
IJCAR 2024 is the merger of leading events in automated reasoning:
Topics
IJCAR 2024 invites submissions related to all aspects of automated or interactive logical reasoning, including foundations, implementations, and applications. Original research papers and descriptions/evaluations of working automated deduction systems or proof assistant systems are solicited.
IJCAR topics include the following:
Important Dates (partly tentative)
More information is available on the conference's web page.
TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2023 was held from 12 to 15 June at ETSInf, Universitat Politècnica de València, Spain. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference.
List of Topics
The scope of the post-proceedings is the same as the scope of the
conference: the theory and practice of type theory. In particular, we
welcome submissions on the following topics:
Submission Guidelines Submission is open to everyone, also to those who did not participate in the TYPES 2023 conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, and be original, i.e. neither previously published, nor simultaneously submitted to a journal or a conference.
Deadlines
For information about TYPES 2023, see the conference website.
The FoIKS symposia provide a biennial forum for presenting and discussing theoretical and applied research on information and knowledge systems. The goal is to bring together researchers with an interest in this subject, share research experiences, promote collaboration and identify new issues and directions for future research.
FoIKS 2024 solicits original contributions (as well as extensions of previously published contributions) dealing with any foundational aspect of information and knowledge systems. This includes submissions that apply ideas, theories or methods from specific disciplines to information and knowledge systems. Examples of such disciplines are discrete mathematics, logic and algebra, model theory, information theory, (parameterized) complexity theory, algorithmics and computation, statistics, and optimisation, among, of course, many others.
The FoIKS symposia are a forum for intensive discussions. Speakers will be given sufficient time to present their ideas and results within the larger context of their research. Furthermore, participants will be asked to prepare a first response to another contribution in order to initiate discussion.
Suggested topics
The suggested topics include, but are not limited to:
Important Dates
All deadlines are at 23:59 UTC-12 (AoE, "anywhere on earth").
More information is available on the symposium's web page.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced technologies to address their specification, design, verification, validation, and certification processes. For example, there is an increasing need for autonomous systems in deep space missions including NASA’s Moon to Mars exploration plans. The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, other government agencies, academia, and industry, with the goal of identifying challenges and providing solutions towards achieving assurance for such critical systems. The focus of this symposium is on formal techniques for software and system assurance for applications in space, aviation, robotics, and other NASA-relevant safety-critical systems. This year’s symposium extends the focus to safety assurance of machine learning enabled autonomous systems, formal methods for digital transformation, and accessibility for new industries.
Topics of Interest:
Important Dates:
More information is available on the symposium's web page.
FLOPS aims to bring together practitioners, researchers and implementers of declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.
FLOPS solicits original papers in all areas of declarative programming:
FLOPS promotes cross-fertilization among different styles of declarative programming. Therefore, research papers must be written to be understandable by a wide audience of declarative programmers and researchers. In particular, each submission should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant for its area, and comparing it with previous work. Submission of system descriptions and declarative pearls are especially encouraged.
Important Dates
All deadlines are Anywhere on Earth (AoE = UTC-12).
More information is available on the symposium's web page.
The SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software but does not exclude the analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation.
Topics of interest include, but are not limited to:
Important Dates
More information is available on the symposium's web page.
The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric.
Suggested, but not exclusive, topics of interest include:
Important Dates for Papers
Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is anywhere on earth (AoE).
More information is available on the symposium's web page.
Overview
FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logic, models of computation, semantics and verification in new challenging areas.
The suggested, but not exclusive, list of topics for submission is:
Important Dates
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
More information is available on the conference's web page.
CiE 2024 will be an anniversary event. It is the 20th conference organized by CiE (Computability in Europe), in the same place as the first edition, Amsterdam.
CiE is a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.
Conference Topics
The CiE conferences serve as an interdisciplinary forum for research in all aspects of computability, foundations of computer science, logic, and theoretical computer science, as well as the interplay of these areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics.
Special Sessions
There will be 6 special sessions, including:
Important Dates:
More information is available on the conference's web page.
ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). As usual, ICALP will be preceded by a series of workshops, which will take place on July 7.
Topics
Papers presenting original research on all aspects of theoretical computer
science are sought. Typical, but not exclusive, topics of interest are:
Important dates and information
More information is available on the conference's web page.
GALOP is an international workshop on formal models for compositional program interaction and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials.
Areas of interest include, but are not limited to:
Important Dates
Started in 2002, the CLA workshops provide an open, free access forum for interdisciplinary research concentrated around combinatorial and quantitative aspects of mathematical logic and their applications in computer science.
Topics within the scope of CLA include:
Important dates
More information is available on the workshop's web page.
Rewriting is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application domains. It also has good properties as a metalogical framework for representing logics. Several successful languages based on rewriting (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of WRLA is to bring together researchers with a common interest in rewriting and its applications, and to give them the opportunity to present their recent work, discuss future research directions, and exchange ideas.
Topics of Interest
The topics of the workshop include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers.
Scope
Contributions are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive areas of
interest are:
Important Dates
More information is available on the workshop's web page.
The DL workshop is the major annual event of the description logic research community. It is the forum in which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences. The 37th edition will be held in Bergen, Norway from June 18th to June 21st.
Workshop Scope
We invite contributions on all aspects of description logics, including, but not limited to:
Important Dates
More information is available on the workshop's web page.
The ANU Logic Summer School is an annual event that offers a two week long programme of lectures on mathematical, philosophical, and computational aspects of logic. The school is primarily geared at late undergraduate and masters students, but is open to all, including postgraduate and PhD students, postdocs, and participants from industry.
More information is available on the school's web page.
The IMDEA Software Institute invites applications for tenure-track (Assistant Professor) faculty positions. We are primarily interested in recruiting excellent candidates in the areas of: Machine Learning, including Formal Reasoning about ML Systems, Explainable AI, Data Analysis at Large Scale, etc.; Software Engineering; Systems in general, including Distributed Systems, Embedded Systems, Databases, etc.; Cyber-Physical Systems; and Privacy. Exceptional candidates in other topics within the general research areas of the Institute will also be considered. Tenured-level (Associate and Full Professor) applications are also welcome.
The primary mission of the IMDEA Software Institute is to perform research of excellence at the highest international level in software development technologies. It is one of the highest-ranked institutions worldwide in its main topic areas.
Selection Process
The main selection criteria are the candidate's demonstrated ability and commitment to research, the match of interests with the Institute's mission, and how the candidate complements areas of established strengths of the Institute. All positions require a doctoral degree in Computer Science or a closely related area, earned by the expected start date. Candidates for tenure-track positions will have shown exceptional promise in research and will have displayed an ability to work independently as well as collaboratively. Candidates for tenured positions must have an outstanding research record, recognized international stature, and demonstrated leadership abilities. Experience in graduate student supervision is also valued at this level.
Applications should be completed using the application form here.
Please select reference "2023-10-faculty-call" at the beginning of the form. For full consideration, complete applications must be received by December 15, 2023, although applications will continue to be accepted until the positions are filled.
Working at the IMDEA Software Institute
The Institute is located in the vibrant area of Madrid, Spain. It offers an ideal working environment, combining the best aspects of a research center and a university department. Its researchers can focus on developing new ideas and projects, in collaboration with world-leading, international faculty, post-docs, and students. Researchers also have the opportunity (but no obligation) to teach university courses. The Institute offers institutional funding and also encourages its members to participate in national and international research projects. The working language at the Institute is English.
Salaries at the Institute are internationally competitive and established on an individual basis. They include social security provisions in accordance with existing national Spanish legislation, and in particular access to an excellent public health care system.
Further information about the Institute's current faculty and research can be found here
The IMDEA Software Institute is an Equal Opportunity Employer and strongly encourages applications from a diverse and international community and underrepresented groups. The Institute complies with the European Charter for Researchers.
The Department of Mathematics and Computer Science of the University of Cagliari will shortly open calls for two research fellowships for 12 months within a multidisciplinary research project on the study of networks and graph structures.
We are seeking for candidates with a background in one of these topics:
Background in the analysis of networks under their different theoretical and applied aspects are highly valued.
The positions will be opened at the Department of Mathematics and Computer Science of the University of Cagliari.
The official calls will be advertised before the end of 2023, but we encourage potential interested applicants to get in touch with us to express their interest.
There is no specific deadline, but we encourage applicants to express their interest before October 31st, 2023.
Brief description of the project
GraphNet: models, computation and estimation in networks and graph analysis is an interdisciplinary research project with the global objective of integrating and developing mathematical, statistical and computer science tools to provide a thorough comprehension of the complex association between graph theory and network science. The primary project's aim is to bridge together the abstract mathematical structure of graphs and the computational and inferential approaches in the description of real-world networks arising from applications. We will deal with 3 objectives: theoretical aspects of graph structures, analysis of case studies, and implementation of appropriate computational and visualization tools.
The university of Southampton is looking to hire new academic staff in four research areas including "Theoretical Computer Science" understood broadly (Programming Language Semantics, Functional Programming, Theorem Proving, Logic & Foundations of CS).
More about Southampton University and the post can be found here.
The deadline for application is October 30, 2023
If you are interested, or know promising early career researchers who maybe, please direct all emails to Ekaterina Komendantskaya.
The research group Logic in Philosophy and Artificial Intelligence (Christian Straßer, Ruhr-University Bochum) has an opening for two PostDoc-positions (3y and 2y). Deadline: 30. October 2023.
Position 1 (3y) is embedded in the LoDEx project (Logical methods for Deontic Explanations), a joint project between the Ruhr-University Bochum (PI: Christian Straßer), the University of Luxembourg (PI: Leon van der Torre) and the TU Vienna (PI: Agata Ciabattoni).
Position 2 (2y) is funded by the Ruhr University Bochum.
Description: Position 1 (LoDEx). ANR: 2461.
This position is a three-year, 100%-funded PostDoc position (TV-L 13), starting February 2024.
The candidate will be working as a member of the WEAVE project “Logical methods for Deontic Explanations” (LoDEx). The project’s general aim is to develop formal frameworks for generating explanations in the context of ethical and legal reasoning. These "deontic explanations" facilitate our comprehension of the underlying reasons for the application of specific norms within a particular context, illuminating why adherence to these norms is crucial.
The PostDoc position focuses on the use of formal argumentation for the modeling of deontic explanations. Such a model comes with many challenges. One is that in order to be more perspicuous and convincing, explanations should take into account what the explainee believes and values, i.e., their epistemic and axiologic horizon. Another challenge is the contrastive nature of explanations, since why-questions are often framed contrastively ('Why should I do A rather than B?'). Formal argumentation offers a good basis for modeling explanatory exchanges, e.g., in terms of dialogues. The candidate will also interact with a PhD student working on applications of deontic explanations to bioethical problems.
The candidate should have familiarity with either of the following (and ideally several):
Description: Position 2. Defeasible Reasoning. ANR: 2394.
This position is a two-year, 100%-funded PostDoc position (TV-L 13), starting February 2024.
The candidate will be working on formal models of defeasible reasoning, in particular those based on nonmonotonic logic and formal argumentation.
Possible areas of specialization include:
The position comes with a teaching requirement, namely 2 courses per teaching term.
research Environment.
The positions will be embedded in a rich research environment, incl.
connections to
Family-friendly initiatives are in place, such as an international spouse program, and excellent on-campus children day care and sports facilities.
Job requirements. You hold a PhD degree in Philosophy, Computer Science, Mathematics, or a discipline related to the listed topics.
You have an interest in the above listed themes of the research. Knowledge of German language is not required.
We welcome candidates with a wide variety of backgrounds and perspectives and we especially encourage candidates from underrepresented groups to apply.
For any queries, please contact Christian Straßer.
Application.
Your application should contain the following documents:
If you are interested, we invite you to apply by 30th of October.
Interviews will be held shortly thereafter online.
Please send your application to this email address.
Graz University of Technology is looking for a candidate with proven scientific expertise who will represent the field of "Foundations of Computer Science" in research and teaching. Applications from any subfield of theory are welcome.
Prof. Jasmin Blanchette is looking for PhD students (4 years) and postdoctoral researchers (3 years) who will work at the Ludwig-Maximilians-Universität in Munich, Germany. They will be hosted by the Chair of Theoretical Computer Science and Theorem Proving led by Prof. Jasmin Blanchette. The work will be supervised by Blanchette together with external experts and will be funded by the ERC project Nekoka.
Proof assistants (also called interactive theorem provers) have a long history of being very tedious to use. The situation has improved markedly in the past 10–15 years with the integration of first-order automatic theorem provers that increase proof automation. And recently, there have been exciting developments for more expressive logics, with the emergence of automatic provers based on optimized higher-order proof calculi. The Nekoka project’s aim is to make two of these calculi, higher-order SMT and lambda-superposition, a great fit for logical problems emerging from the verification of software and mathematics.
Nekoka is the logical successor of the Matryoshka project, which led to the development of lambda-superposition and its implementation in the E and Zipperposition provers. The Nekoka topics range from extending higher-order SMT and lambda-superposition to integrating them in general-purpose proof assistants (e.g., Isabelle, Lean) and software verification platforms (e.g., F*, TLA+ Proof System) to using the resulting automation in case studies related to quantum information theory and a big data framework.
For the postdoc positions, we are also interested in applicants who have their own research agenda compatible with the general aims of Nekoka.
The positions are categorized as TV-L E13 according to the German salary scale. The starting date is flexible. Please contact Jasmin Blanchette for more information or if you want to apply. Applications should include
See the job ad for details.
Oxford University’s Computer Science Department is hiring four new faculty. The positions are open to all areas of computer science and the closing date is 12 noon UK time on 13 December 2023.
For more information, see here.
The Institute of Computer Science of the Czech Academy of Sciences (ICS CAS) is opening two tenure track positions:
Expected starting date (for both calls): upon agreement.
Researchers focusing on Logic in Computer Science (broadly construed) are very welcome to apply within the general call. Researchers focusing on Logic and Artificial Intelligence (broadly construed) are very welcome to apply within the AI-specific call as well. Interested candidates are invited to consult the webpages of the ICS CAS Logic Group and get in touch with the group with informal inquiries.
The Logic Uncertainty Computation and Information (LUCI) Lab at the University of Milan, Italy will shortly be advertising calls for up to six full-time postdoctoral researchers. We will be seeking applications with strong skills in
Please see the LUCI website for further details about the Lab members and our research.
The lab is planning to post the call for applications for at least some of the positions before the end of 2023, but they encourage potential applicants to get in touch with them to express their interest.
The PhD positions include full tuition waiver and a very competitive scholarship. Aarhus University provides international students with a safe and stable environment, a high standard of living and a wealth of social opportunities. Besides having an excellent reputation that enables our PhD graduates to find outstanding employment prospects, Aarhus University offers attractive working conditions, research support and campus resources. See here and here for more information.
This project is supported by the Danish DIREC research center. It is a collaboration between Aarhus University, the Alexandra Institute and Concordium ApS. The aim of the project is work towards secure implementations of Blockchain Voting Governance Protocols and Internet Voting Protocols.
Voting and blockchains are intimately connected. Voting is used in blockchains for consensus, governance, and decentralized organizations. Conversely, elections are based on trust, which means that election systems ideally should be based on algorithms and data structures that are already trusted. Blockchains provide such a technology. They provide a trusted bulletin board, which can be used as part of some voting protocols. Moreover, voting crucially depends on establishing the identity of the voter to avoid fraud and to establish eligibility verifiability.
Decades of research in voting protocols have shown how difficult it is to combine the privacy of the vote with the auditability of the election outcome. It is easy to achieve one without the other, but hard to combine both into one protocol. Thus, the topic of this research proposal is to investigate voting protocols and their relation to blockchains.
The team will work on (machine-checked) security proofs of these protocols and their implementations, for instance using tools such as ConCert and SSProve which are built on the Coq proof assistant.
Diego Marmsoler is seeking to appoint a Postdoctoral Research Associate that wants to apply formal methods for building correct, safe, and secure systems. The post is part of the growing Security and Trust of Advanced Systems Group. The group has a broad expertise in developing and applying formal methods tools in general and in working and extending Isabelle/HOL in particular.
The advertised position is part of the EPSRC funded project "Secure Smart Contracts with Isabelle/Solidity" and is available from 01/01/2024 to 31/12/25. The successful applicant will work with me on the development of tools and techniques for the verification of Smart Contracts. This includes the development of a calculus for the verification of smart contracts, its implementation in Isabelle/HOL, as well as applying it for the verification of real-world smart contracts. For more information about the project please visit the project website.
You can apply online. Application closes 14/11/23.
If you do have any questions please contact Diego Marmsoler by email.
A fully funded three-year PhD or postdoc position (E-13 on the German TV-L scale, full time, no teaching obligation) is available at the Theoretical Computer Science lab of Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Germany, with starting date between now and April 2024. The position is affiliated with a large interdisciplinary project involving FAU labs in computer science, linguistics, and law, funded by the German Federal Chamber of Notaries (Bundesnotarkammer). The project is aimed at providing automated support for notarial procedures using methods from formal logic, machine learning, and computational linguistics.
The position at the Theoretical Computer Science lab, supervised by Lutz Schröder, is concerned with formal logical modelling and reasoning. We are thus looking for a candidate with an MSc or PhD in computer science or mathematics, ideally with a background in logic, in particular modal or description logics.
The position is embedded into a large and active research group with a highly collaborative spirit. Erlangen's technical campus is situated within pleasant Franconia, and close to the vibrant city of Nuremberg. Please send applications or further inquiries to Lutz Schröder
The University of Innsbruck invites applications for a 4 year PhD position in the Computational Logic research group. Candidates must hold a master degree in computer science or mathematics. Knowledge of term rewriting and automated deduction is desired. Candidates close to obtaining a master degree are also invited to apply. Knowledge of German is not required. The position is an official university position with 15 February 2024 as starting date. The main task will be to pursue research leading to a dissertation. The position comes with teaching obligations of 2 hours per semester. The minimum gross salary (stipulated by collective agreement) for this position amounts to € 1639 / 2458 per month (14 times).
The official job advert (code MIP-13828) appeared here.
Applications (including CV, list of presentations, motivation letter, possible research topics) must be submitted electronically, until October 26, 2023.
Informal inquiries may be addressed to Aart Middeldorp
The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and 1976, is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living.
Further information is available from the following links:
Martin Davis, from which comes the D of the DPLL algorithm for SAT solving that we all know, passed away early this year. You can find his eulogy here.