Editor's note: I would like to share with you this text, that I stumbled upon while searching for bibliographic references on the web. I enjoyed the reflections on the past and future of logics and automated reasoning it contains. Melvin Fitting kindly allowed me to reproduce it here. It is the acceptance speech he delivered upon receiving the Herbrand award in 2012. Since then, eleven years have passed. Do you recognise the direction he is pointing at in today's automated reasoning research?
***
[My thesis advisor was Raymond Smullyan. He likes to begin talks with, “Before I speak, there’s something I’d like to say.” Well, before I speak, there’s something I’d like to say. When, to my surprise, I was told about the Herbrand Award, I decided that for probably once in my life I’d make a speech. This became easier when I realized that a speech is just a talk without slides. I even wrote the speech out, and this is what I’m going to read to you now.]
I want to thank CADE for this wonderful and unexpected award. I am deeply grateful to be honored in this way.
As it happens, almost simultaneously with this award I am retiring from teaching. Not from research, but from regular, day to day teaching. I’ve been at it for 44 years now. There’s a story about a 16 year old boy who was asked what he would want, if he could have anything whatsoever. His answer: “I’d like to be 12 again, but knowing what I know now.” It’s a good answer; it embodies part of the human condition. Indeed, any two years n and k, with n < k would work just as well. We here are involved with automated deduction. Deduction is in a logic. I want to express some very general thoughts about our choices of logics. I have nothing profound to say, nothing you probably haven’t considered already. But I’m going to say it anyway.
In the nineteenth and early twentieth centuries philosophy often came in big, comprehensive systems. Fichte, Hegel, Schopenhauer, even Marx and Freud, and others. Perhaps the post-modernists can be counted as late outliers in this tradition. Big scale philosophers aspired to a complete world view. In the popular mind this approach was simply identified with philosophy. In 1940, Richard Rodgers and Lorenz Hart wrote a Broadway Musical called Pal Joey, perhaps their best. In it one character, based on the exotic dancer Gypsy Rose Lee, sings a song that contains the lines, “I was reading Schopenhauer last night, And I think that Schopenhauer was right.” The assumption was that a Broadway audience would at least know a little of what Schopenhauer was about—at least had heard the name.
Big philosophy is no longer in fashion. For one thing, it’s hard to know when you’re right. Late twentieth century and twenty-first century philosophy, by and large, is much more fragmented. Papers and books are on specialized topics and few, if any, try to be universal. For instance, a few years ago I heard Saul Kripke give a very nice, witty, and informative lecture on the word “the.” In fact, there is much to be said about the word “the”, but this is certainly at the opposite extreme from the big approaches of former times.
Formal logic follows the same curve as philosophy. In the late nineteenth and early twentieth centuries Frege, and especially Russell and Whitehead, created big logics. For mathematics, indeed for the sciences generally, they created large, all encompassing formal systems. Richard Montague is a late twentieth century outlier in this tradition, having created a kind of universal formal logic that could embrace intensional as well as extensional concepts.
But from the later period of the twentieth century to today, formal logic has fragmented. There are now many, many small logics, decidable if at all possible, each designed to treat a narrow area of human thought and its applications. You all know many items in the list. Modal logics. Epistemic Logics. Temporal logics. Many-valued logics. Many-valued Modal logics. Non-Monotonic logics, Substructural logics. Paraconsistent Logics. Dynamic Logics. Logics of Communication. Game Logics. Fuzzy Logics. Justification Logics. This is hardly complete. It’s a long list, and growing steadily. And those I mentioned are not single logics, but families of logics. Each family is devoted to a narrow aspect of reasoning and a specific intended subject matter, which is further narrowed down by a choice of logic within the family.
[I’m not slighting first-order logic. It is central, but in terms of my big/small classification, it’s not quite one and not quite the other. It is not decidable so it’s not small. But it is surprisingly tractable in a pragmatic sense, so it’s not big either. I’m sure we all know the saying, “First-order logic, and then order beer.]
The move to multiple specialized logics is a natural one from the point of those here. Any huge, general, “logic to rule them all” is complex, difficult to work with, impossible to automate. [And here a nod to FOL, which succeeds surprisingly well.] With a divide and conquer strategy we fragment the world of logic into more docile bits. At least to some extent. As we all know, proof methods that work splendidly for one general variety of logic may be inapplicable to another. Even decidable logics can have decision procedures that render the fact of decidability essentially useless. Still, progress is being made. And we are certainly—well, probably—moving closer to the way we reason ourselves.
When we do mathematics, what is the role of a big system such as Principia Mathematica, or Martin-Löf, or ZF? It tells us the minimum general assumptions that are needed for what we do. That’s important, but in mathematical practice we don’t actually start from there. We work in, say, group theory, or projective geometry, or topos theory, or functional analysis, and we start with assumptions and methods of reasoning peculiar to that area, plus some general machinery which we grab as needed. We don’t begin by asking, “what reasoning machinery must we use?” Instead we decide what we are reasoning about and pick the machinery accordingly. If this is so in mathematics, how much more so in everyday life where, all appearances to the contrary, we do apply reason.
The fundamental question we must address, in the face of this fragmentation of logics, is how to put it all back together. Think of the array of logics we work with as formal representations of ways we sometimes think. How do we manage to function daily, act coherently, and not explode periodically? Well, perhaps that’s a bit too much to ask, but let’s try anyway.
We could look for principles that allow logics to be combined, then combine the whole bunch once and for all. Of course, there is already some formal machinery for combining logics, but its primary use is to combine small logics into another manageable small logic. I don’t think anybody has pushed things much beyond that. As such it is a useful tool for the creation of small logics. But combine them all somehow? The outcome must be yet another big logic of the classic kind, but more complicated than anything previously considered. This does not seem to be a promising direction at all. And it does not seem to be how we behave ourselves, as what L. Frank Baum [the author of “The Wizard of Oz”] called, rather gruesomely, “meat men,” [contrasting with his “tin man”] .
We seem to operate pragmatically in the presence of multiple ways of reasoning. We somehow evaluate what method is most appropriate and go with it. We ignore ways of reasoning that seem, on their face, useless to the particular job. I have a new grandchild, and he is in the process of learning how to do this. Perhaps he will tell me about it someday, for I have forgotten the details. More likely he will not because it is not something that rises to the level of conscious thought. It is a kind of subroutine in our operating systems, routing problems to appropriate solution mechanisms. Or perhaps this is simply a plausible answer that my appropriate solution mechanism has come up with.
However it is done, we still have two basic problems for our understanding. What do we do when different, but still appropriate, reasoning mechanisms produce different results? The second problem is a special case, what do we do when a reasoning mechanism produces a result that is discovered to be false? (This is a special case because the world is a kind of logic, with experiments as searches for counter-examples.) Again, I don’t know how we handle this. Perhaps each of us has different ways of coping with these problems. I don’t believe we have one superior internal system that judges—this would be the one universal system again. It seems more likely that all this remains a local matter; somehow two conflicting results fight it out. Our overall rational behavior, such as it is, is the outcome of all this constant divide-and-conquer, strongest solution prevails battleground. At least, it’s the best I can come up with.
But it does suggest a challenge for the coming generations of formal logicians and researchers in automated deduction. We now have many reasoning systems, of varying degrees of strength, of diverse areas of applicability. How do we fit them together? And it should not be by our brute force. I don’t think we are up to the task of deciding, once and for all, what problems are appropriate for what mechanisms and who prevails under conflicts. We need to devise a learning strategy that can allot tasks, adjudicate conflicts, and accommodate the addition of new ways of reasoning. This itself would not be a logic, but something more akin to an operating system that learns by experience. One might begin with a few well- understood formal logics, and see what is needed to combine them, not formally, but pragmatically, operationally. They should remain separate, but things should be managed so that each submitted problem is, somehow, routed to the more appropriate logic, or logics if that is appropriate, conflicts between logics and between them and the world are somehow resolved, and the management system learns from its mistakes. What is learned is not logic, but how to choose which logic.
What sort of input would be required? At its best, it would be the description of a problem that somehow requires reasoning, stated in natural language. And what sort of output? Either a proof, or a description of a counter-model, ideally in natural language. Below the surface the right formal logic would be selected, or battled for, and its output made appropriate use of. In fact there is a plausible model for what is needed: the recent Watson program, designed to play the TV show Jeopardy. At the Turing 100 conference, immediately preceeding this one in Manchester, David Ferrucci gave a talk about the development of Watson. The ideas and architecture are more-or-less right for the task I outlined, and he said the design features are migrating to simpler computer systems. Perhaps soon such machinery will be available to this community. Perhaps soon enough.
Judea Pearl says, “... we utilize knowledge about irrelevance. We decompose problems into chunks that are only loosely connected.” Yes, but when we reason in mathematics relevance plays a role that is perhaps as big as irrelevance. This may carry over to the rather specialized task of selecting logics. I’m not talking about artificial intelligence generally, but about something much narrower. This is still a big job, since we already have many, many formal, automated logics. For that matter, it is a big job with just two, which is where one might begin. It’s not exactly logic. It’s logic management. I have no idea how to proceed. But it is worth thinking about.
Thank you for your attention.
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 April 06, 2023.
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 2023 consists of the following people:
The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting.
The Herbrand Award has been given in the past to:
A nomination is required for consideration for the Herbrand Award. Nominations can be submitted at any time. The deadline for nominations to be considered for the Herbrand Award 2023, which will be given at CADE-29, is
March 31 2023Nominations pending from previous years must be resubmitted in order to be considered.
For more details, please check the Herbrand Award webpage.
Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent via e-mail to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
The Vienna Center for Logic and Algorithms of TU Wien calls for the nomination of authors of outstanding theses and scientific works in the field of Logic and Computer Science, in the following two categories:
The main areas of interest are:
Awards
Eligibility
Nomination Requirements
Nominations must include:
Instructions for submitting self-nominations
Important dates
Contact
Please send all inquiries to this email address.
Websites with information on the award committee and the previous awardees: here and here.
The FSCD conference covers all aspects of Formal Structures for Computation and Deduction from theoretical foundations to applications. The annual FSCD conference comprises the main conference and a considerable number of affiliated workshops (expectedly, more than ten).
We invite proposals for locations to host the 10th FSCD International Conference to be held during the summer of 2025. The deadline for proposals is 27th May 2023 Proposals should be sent to the FSCD Steering Committee Chair Herman Geuvers. We encourage proposers to register their intention informally as soon as possible.
Previous (and upcoming) FSCD meetings include:
Selected proposals are to be presented at the business meeting of FSCD 2023 taking place in Rome in July 2023. The final decision about hosting and organising of FSCD 2025 will be taken by the SC after an advisory vote of the members of the community in attendance at the business meeting.
Proposals should address the following points:
ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of four annual conferences accompanied by satellite workshops. ETAPS 2023 is the twenty-sixth event in the series.
Early registration is until 28 February 2023. After 22 March, late registration rates apply.
More information is available on the conference's web page.
Dynamic Logic (DL), a generalization of the logic of Floyd-Hoare introduced in the 70s by Pratt, is a well-known and particularly powerful way of combining propositions, for capturing static properties of program states, and structured actions, responsible for transitions from a state to another (and typically combined through a Kleene algebra to express sequential, non-deterministic, iterative behavior of systems), into a formal framework to reason about, and verify, classic imperative programs. Over time DL grew to encompass a family of logics increasingly popular in the verification of computational systems, and able to evolve and adapt to new, and complex validation challenges. In particular, the dynamic logic community is interested in the study of operators that can modify the structure in which they are being evaluated. Examples include dynamic logics tailored to specific programming problems or paradigms (e.g., separation logics to model the evolution of a program heap); languages to reason and represent evolving information (e.g., dynamic epistemic logics); and formalism that aim to model new computing domains, including probabilistic, continuous and quantum computation.
This special issue is dedicated to new advances in Dynamic Logic. Its aim is to bring together papers on both pure and applied aspects of various branches of DL, and foster the exchange of ideas between researchers working in DL and other disciplines.
We invite submissions on both (a) theoretical topics from all branches of mathematical logic (e.g., proof-theory, model theory, game theory, computational complexity, etc.) in connection with DL, as well as (b) their applications in various areas (including computer science, linguistics, mathematics, philosophy, etc.).
Topics of Interest
We invite submissions on the general field of Dynamic Logic, its variants and applications, including, but not restricted to:
Relevant dates and deadlines
Submissions
Papers should be submitted via EasyChair.
The submissions should be formatted according to the Journal's guidelines.
All submissions will undergo the usual peer-review process by the standards of the Journal of Logical and Algebraic Methods in Programming.
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-29 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction.
Important Dates
More information is available on the conference's web page.
The use of graphs and graph-like structures as a formalism for specification and modelling is widespread in all areas of computer science as well as in many fields of computational research and engineering. Relevant examples include software architectures, pointer structures, state space and control/data flow graphs, UML and other domain-specific models, network layouts, topologies of cyber-physical environments, quantum computing and molecular structures. Often, these graphs undergo dynamic change, ranging from reconfiguration and evolution to various kinds of behaviour, all of which may be captured by rule-based graph manipulation. Thus, graphs and graph transformation form a fundamental universal modelling paradigm that serves as a means for formal reasoning and analysis, ranging from the verification of certain properties of interest to the discovery of fundamentally new insights.
The International Conference on Graph Transformation aims at fostering exchange and collaboration of researchers from different backgrounds working with graphs and graph transformation, either in contributing to their theoretical foundations or by applying established formalisms to classical or novel areas. The conference not only serves as a well-established scientific publication outlet, but also as a platform to boost inter- and intra-disciplinary research and to leeway for new ideas.
Topics
In order to foster a lively exchange of perspectives on the subject of
the conference, the programme committee of ICGT 2023 encourages all
kinds of contributions related to graphs and graph transformation,
either from a theoretical point of view or a practical one.
Topics of interest include, but are not limited to the following subjects:
Important Dates
More information is available on the conference's web page.
PACMPL issue ICFP 2023 seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, and from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects, concurrency, or parallelism. Topics of interest include (but are not limited to):
Important dates (All dates are in 2023 at 11.59pm anywhere on earth.)
More information is available on the conference's web page.
The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.
Research in verification has seen a steady convergence of heterogeneous techniques and a synergy between the traditionally distinct areas of testing (and dynamic analysis) and of proving (and static analysis). Formal techniques for counter-example generation based on, for example, symbolic execution, SAT/SMT-solving or model checking, furnish evidence for the potential of a combination of test and proof. The combination of predicate abstraction with testing-like techniques based on exhaustive enumeration opens the perspective for novel techniques of proving correctness. On the practical side, testing offers cost-effective debugging techniques of specifications or crucial parts of program proofs (such as invariants). Last but not least, testing is indispensable when it comes to the validation of the underlying assumptions of complex system models involving hardware and/or system environments. Over the years, there is growing acceptance in research communities that testing and proving are complementary rather than mutually exclusive techniques.
TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Its topics of interest center around the connection between proofs (and other static techniques) and testing (and other dynamic techniques). Papers are solicited on, but not limited to, the following topics:
Important Dates:
More information is available on the conference's web page.
Knowledge Representation and Reasoning (KR) is a well-established and lively field of research within Artificial Intelligence. KR builds on the fundamental thesis that knowledge can be represented in an explicit declarative form, suitable for processing by dedicated symbolic reasoning engines. This enables the exploitation of knowledge that would otherwise be implicit through semantically grounded inference mechanisms. Consequently, KR has contributed to the theory and practice of various areas in AI, including agents, automated planning and natural language processing, and to fields beyond AI, including data management, semantic web, verification, software engineering, robotics, computational biology, and cyber security.
The KR conference series is the leading forum for timely in-depth presentation of progress in the theory and principles underlying the representation and computational management of knowledge.
KR 2023 will consist of a number of tracks and events: the Main Track,
Topics of interest include, but are not limited to:
Important Dates
More information is available on the conference's web page.
The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized and computer assisted reasoning and computer programming.
The TYPES areas of interest include, but are not limited to:
Important Dates
More information is available on the conference's web page.
The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas. LPAR is an "A" ranked conference in the CORE ranking system; papers from previous proceedings are listed in DBLP.
List of Topics
New results in the fields of computational logic and applications are welcome.
Also welcome are more exploratory presentations, which may examine open
questions and raise fundamental concerns about existing theories and
practices. Topics of interest include, but are not limited to:
Important Dates
More information is available on the conference's web page.
Algebraic and coalgebraic methods and tools are a mainstay of computer science. From data types to development techniques and specification formalisms, both theoreticians and practitioners have benefited from the large body of research proposed and implemented since the pioneering works of the 1960s.
CALCO aims to bring together researchers with interests in both foundational and applicative uses of algebra and coalgebra in computer science, traditional as well as emerging ones.
Topics of Interests
All topics relating to algebraic and coalgebraic theory and applications
are of interest for CALCO, and among them
Important Dates
More information is available on the conference's web page.
SAT is the premier annual meeting for researchers focusing on the theory and applications of propositional satisfiability, broadly construed. That includes Boolean optimization, such as MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), model counting, and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning. Topics of interest include (but are not limited to): - Theoretical advances (including algorithms, proof complexity, parameterized complexity, and other complexity issues) - Practical search algorithms - Knowledge compilation - Implementation-level details of SAT solving tools and SAT-based systems - Problem encodings and reformulations - Applications (including both novel applications domains and improvements to existing approaches) - Case studies and reports on insightful findings based on rigorous experimentation
Important Dates
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. Areas of interest include, but are not limited to:
Important Dates
More information is available on the symposium's web page.
The International Conferences on Conceptual Structures (ICCS) focus on the formal analysis and representation of conceptual knowledge at the crossroads of artificial intelligence, human cognition, computational linguistics, and related areas of computer science and cognitive science. The ICCS conferences evolved from seven annual workshops on conceptual graphs, starting with an informal gathering hosted by John F. Sowa in 1986. Recently, graph-based knowledge representation and reasoning (KRR) paradigms have been getting more and more attention. With the rise of quasi-autonomous AI, graph-based representations provide a vehicle for making machine cognition explicit to human users. At ICCS 2023, scholars, students and industry participants from different disciplines will meet for several weeks of conferences, workshops, summer schools, and public events to engage with the broad topics, issues and challenges related to knowledge in the 21st century.
Submissions are invited on significant, original, and previously unpublished research on the formal analysis and representation of conceptual knowledge in artificial intelligence (AI). All papers will receive mindful and rigorous reviews that will provide authors with useful critical feedback. The aim of the ICCS 2023 conference is to build upon its long-standing expertise in graph-based KRR and focus on providing modelling, formal and application results of graph-based systems. In particular, the conference welcomes contributions that address graph-based representation and reasoning paradigms (e.g. Bayesian Networks (BNs), Semantic Networks (SNs), RDF(S), Conceptual Graphs (CGs), Formal Concept Analysis (FCA), CP-Nets, GAI-Nets, Graph Databases, Diagrams, Knowledge Graphs, Semantic Web, etc.) from a modelling, theoretical and application viewpoint.
Topics
Topics include but are not limited to:
Important Dates
More information is available on the conference's web page.
The ICLP conference series has a long standing tradition of hosting a rich set of co-located workshops. ICLP workshops provide a unique opportunity for the presentation and discussion of work that can be preliminary in nature, novel ideas, and new open problems to a wide and interested audience.
Co-located workshops also provide an opportunity for presenting specialized topics and opportunities for intensive discussions and project collaboration. The topics of the workshops co-located with ICLP 2023 can cover any areas related to logic programming (e.g., theory, implementation, environments, language issues, alternative paradigms, applications), including cross-disciplinary areas. However, any relevant workshop proposal will be considered.
The format of the workshop will be decided by the workshop organizers, but ample time should be allowed for general discussion. Workshops can vary in length, but the optimal duration will be half a day or a full day.
Important Dates:
More information is available on the conference's workshop page.
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 include, but are not limited to, the following:
Important Dates (anywhere on earth):
More information is available on the conference's web page.
Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information.
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.
topics
CICM 2023 invites submissions in all topics relating to intelligent
computer mathematics, in particular but not limited to
Important Dates
More information is available on the conference's web page.
KI is one of the major European AI conferences and traditionally brings together academic and industrial researchers from all areas of AI, providing an ideal place for exchanging news and research results on theory and applications.
Topics include all subareas of artificial intelligence with focus on foundations as well as applications.
Important Dates
More information is available on the conference's web page.
TABLEAUX is the main international conference at which research on all aspects -- theoretical foundations, implementation techniques, systems development and applications -- of tableaux-based reasoning and related methods is presented. The first TABLEAUX conference was held in Lautenbach near Karlsruhe, Germany, in 1992. Since then it has been organised on an annual basis (sometimes as a part of IJCAR).
Scope of Conference
Tableaux and related proof methods offer convenient and flexible tools for automated reasoning for both classical and non-classical logics. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis.
Topics of interest include but are not limited to:
Important Dates
More information is available on the conference's web page.
The Research and Innovation track at SEMANTiCS 2023 EU welcomes papers on novel scientific research and/or innovations relevant to the topics of the conference. Submissions must be original and must not have been submitted for publication elsewhere. Papers must follow the guidelines given in the author instructions, including references and optional appendices. Each submission will be reviewed by several PC members who will assess it based on its innovativeness, technical merits, and effectiveness at solving real problems.
SEMANTiCS 2023 especially invites contributions that target the following main topics, sub-topics in the context of semantic-based research and systems as well as applicative domains.
Topics of Interest Topics of interest include, but are not limited to:
Important Dates
More information is available on the conference's web page.
The program committee seeks high-quality submissions describing original work, written in English, not overlapping with published or simultaneously submitted work to a journal or conference, workshop, symposium, etc. with archival proceedings. Selection criteria include originality of ideas, rigour of evaluation, significance of results, and quality of presentation.
List of Topics
Topics of interest for FroCoS 2023 include (but are not restricted to):
Workshops and Tutorials
If you would like to organise a workshop or run a tutorial, please let Martin Suda and Uli Sattler know before July 14th, 2023.
Important Dates
More information is available on the conference's web page.
The aim of the FMICS conference series is to provide a forum for researchers and practitioners who are interested in the development and application of formal methods in the industry. FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
Topics of interest include (but are not limited to):
Important Dates
More information is available on the conference's web page.
The 7th International Joint Conference on Rules and Reasoning (RuleML+RR 2023) is the 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. We are looking for high-quality papers related to theoretical advances, novel technologies, and artificial intelligence applications that involve rule-based representation and reasoning.
Topics
RuleML+RR welcomes research from all areas of Rules and Reasoning.
The topics of the conference include, but are not limited to:
Important dates for the RuleML+RR conference
More information is available on the conference's web page.
The aim of JELIA 2023 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. Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in Artificial Intelligence, including, but not limited to:
Important Dates
More information is available on the conference's web page.
ADG is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction.
Scope: Relevant topics include (but are not limited to):
Special Focus: This edition of ADG will have additional special focus topic: Deduction in Education
Important Dates:
More information is available on the conference's web page.
The Pacific Rim International Conference on Artificial Intelligence (PRICAI) is an annual international event which concentrates on AI theories, technologies and their applications in the areas of scientific, social, and economic importance for countries in the Pacific Rim.
Areas of Interest
The conference areas of interest include, but are not limited to:
Important Dates
More information is available on the conference's web page.
The ICTAC conference series aims at bringing together researchers and practitioners from academia, industry, and government to present research and exchange ideas and experiences within theoretical aspects of computing through methods and tools for system development. ICTAC also aims to promote research cooperation between developing and industrial countries.
Topics
The conference concerns all aspects of theoretical computer science,
including, but not limited to:
Important Dates
More information is available on the conference's web page.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of a new software generation and to discuss existing systems.
Topics of interest include:
Important Dates
More information is available on the workshop's web page.
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
LFMTP 2023 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
Important Dates
More information is available on the workshop's web page.
UNIF 2023 is the 37th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of identifying terms, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.
The International Workshop on Unification (UNIF) is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory.
Topics
A non-exhaustive list of topics of interest includes:
Important Dates
More information is available on the workshop's web page.
The workshop addresses recent trends in implementing first-order theorem provers, and focus on new challenges and application areas. The workshop also discusses the development and use of the first-order theorem prover Vampire, and its potential use cases and interaction with other systems.
Workshop participants include both Vampire developers and users, with discussions between tool developers and users. Participants can learn more about the use of Vampire, its efficiency in various application areas and needs of the users.
The workshop sheds light on topics such as:
Important Dates
More information is available on the workshop's web page.
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts.
Aims and Scope The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:
Important Dates
More information is available on the workshop's web page.
The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
Topics of Interest
Important Dates
More information is available on the workshop's web page.
The Women in Logic workshop (WiL) provides an opportunity to increase awareness of the valuable contributions made by women in the area of logic in computer science. Its main purpose is to promote the excellent research done by women, with the ultimate goal of increasing their visibility and representation in the community. Our aim is to:
submission deadline April 23, 2023, anywhere on earth.
More information is available on the workshop's web page.
HOR is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress. The following is a non-exhaustive list of topics for the workshop:
Important Dates
More information is available on the workshop's web page.
The aim of this workshop is to bring together researchers who are currently developing new computation models or new features for traditional computation models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.
Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems. This includes (but is not limited to):
Important Dates:
More information is available on the workshop's web page.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and computational languages, supporting tool development and reasoning. The LSFA series' objective is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and the use of such techniques and results, from the practical side.
LSFA topics of interest include, but are not limited to:
Important dates
More information is available on the workshop's web page.
Machine Learning on Big Data has gained an enormous popularity during recent years. In the vast majority of cases, the machine learning software for a particular data set is constructed as a neural network. However, this approach is in need of methods for explainable artificial intelligence, as most of the applied models are opaque and operate as a black-box. Other possible issues are the reliability, robustness and fairness of the machine learning software. These issues could be addressed with formal methods from automated deduction.
The purpose of this workshop is to bring together researchers who work in machine learning and automated deduction. The targets of the workshop will be: to apply automated deduction methods to machine learning, to produce objects recognizable by automated deduction tools by machine learning methods, to enhance explainable artificial intelligence coupled with machine learning by automated deduction tools, and to consider further developments in the intersection of both research areas.
Non-exclusive list of topics:
Important Dates
TBA
More information is available on the workshop's web page.
RRRR provides a forum to present novel approaches to foster reproducibility of research results, and replication studies of existing work, in the broad area of formal methods research. Its goal is to spread the word on best practices, and reward the work invested in replicating results. RRRR invites abstracts and short papers for presentation at the workshop; authors will afterwards be invited to submit full papers to a special issue of STTT.
Timeline
More information is available on the workshop's web page.
NeSy 2023 invites submissions for presentation at the workshop of the latest and ongoing research work on neurosymbolic AI. Research papers in any of the following areas of neural-symbolic computing are welcome:
Important Dates
More information is available on the workshop's web page.
Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.
The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.
The topics of interest include but are not limited to:
Important Dates
More information is available on the workshop's web page.
Graphs are common mathematical structures which are visual and intuitive. They constitute a natural and seamless way for system modeling in science, engineering and beyond, including computer science, life sciences, business processes, etc. Graph computation models constitute a class of very high-level models where graphs are first-class citizens. They generalize classical computation models based on strings or trees, such as Chomsky grammars or term rewrite systems. Their mathematical foundation, in addition to their visual nature, facilitates specification, validation and analysis of complex systems. A variety of computation models have been developed using graphs and rule-based graph transformation. These models include features of programming languages and systems, paradigms for software development, concurrent calculi, local computations and distributed algorithms, and biological and chemical computations.
The International Workshop on Graph Computation Models aims at bringing together researchers interested in all aspects of computation models based on graphs and graph transformation. It promotes the cross-fertilizing exchange of ideas and experiences among young and senior researchers from different communities who are interested in the foundations, applications, and implementations of graph computation models and related areas.
Topics
GCM 2023 solicits papers on all aspects of graph computation models. This includes, but is not limited to the following topics:
Foundations
Applications
Important Dates
More information is available on the workshop's web page.
The 12th International Workshop on Confluence (IWC 2023), co-located with the Workshop on Termination (WST 2023), aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. In fact, confluence relates to many topics of rewriting and computation in general (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties.
Topics
IWC 2023 encourages submissions in the following areas:
The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2023 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.
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.
Workshop Scope We invite contributions on all aspects of description logic, including, but not limited to the following:
Important Dates
More information is available on the workshop's web page.
The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-29 will be held on the 3rd July 2023, during the 29th International Conference on Automated Deduction.
CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of:
The competition organizer is Geoff Sutcliffe, assisted by Martin Desharnais. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event.
Registration of systems for CASC-29 is now invited. System registration closes on 5th June. Please register early so that adequate resources can be allocated.
Further details and registration information are available on the competition's web page.
The TACAS 2023 TOOLympics is an event to celebrate the achievements of the various competitions and comparative evaluations broadly related to the field of formal methods and document the experiences, decisions, and best practices stemming from current and past competitions and evaluations in this area.
We invite all competitions and comparative evaluations related to formal methods to participate:
Important dates:
For more details, please see the 2023 TOOLympics website.
The Marktoberdorf Summer School is an 11-day event for young computer scientists and mathematicians, typically doctoral and post-doctoral researchers. It provides mini-courses on state-of-the-art topics in "Safety and Security through Formal Verification" and leaves ample room for interaction between participants and speakers.
Registration opens on February 9, 2023. Register online. Deadline: April 21, 2023
Speakers and Courses:
More information is available on the school's web page.
The Midlands Graduate School (MGS) provides an intensive course of lectures on the Mathematical Foundations of Computing. It has run annually since 1999, and is hosted by the Universities of Birmingham, Leicester, Nottingham, and Sheffield in rotation.
The lectures are aimed at PhD students, typically in their first or second year of study. However, the school is open to anyone who is interested in learning more about the mathematical foundations of computing, and in recent years has seen increased participation from industry. We also very much welcome students from abroad.
The following courses will be held this time:
Introductory Courses:
Important Dates:
More information is available on the school's web page.
We seek 4 PhD students to strengthen the group on Formal Techniques for Knowledge and Data Management at Umeå University (Sweden), funded by the WASP program (Wallenberg AI, Autonomous Systems and Software Program). The students will join a growing group that currently consists of WASP faculty members Diego Calvanese, Magdalena Ortiz, Mantas Šimkus, as well as PostDoc researchers and other doctoral students. The main theme of our research is the applications and further development of logic-based methods and techniques for smart data management. The students will also join the WASP Graduate School, gaining access to a vast professional network involving other top institutions in Sweden. We seek students with strong interest in the following research areas:
The positions are fully funded for 4 years. The deadline is 28/02/2023 Please see the official announcement for more details.
Wallenberg AI, Autonomous Systems and Software Program (WASP) is Sweden’s largest individual research program ever, a major national initiative for strategically motivated basic research, education and faculty recruitment. The program addresses research on artificial intelligence and autonomous systems acting in collaboration with humans, adapting to their environment through sensors, information and knowledge, and forming intelligent systems-of-systems. The vision of WASP is excellent research and competence in artificial intelligence, autonomous systems and software for the benefit of Swedish industry. Read more here.
The Faculty of Informatics at TU Wien invites applications for a full time Assistant Professor position with tenure track. The position is directed to Database Theory and is affiliated to the Institute of Logic and Computation, Research Unit Databases and Artificial Intelligence. The estimated starting date is December, 2023. The work contract is initially limited to six years. The candidate and TU Wien can agree upon a tenure evaluation, which when positive, opens the possibility to change the position to Associate Professor with an unlimited contract.
Detailed information can be found here.
Applications should be addressed here.
Application deadline is: April 13, 2023
The Individual and Collective Reasoning group - ICR (Department of Computer Science), led by Prof. Leon van der Torre, invites applications for 1 Post-Doc in knowledge representation and reasoning, automated theorem proving (especially for non-classical logics)
Your Role
What we expect from you
Our Offer
In Short
How to apply
Applications should include:
We ensure a full consideration for applications received by the 15th of March. Please apply online formally through the HR system. Applications by email will not be considered.
The University of Luxembourg embraces inclusion and diversity as key values. We are fully committed to removing any discriminatory barrier related to gender, and not only, in the recruitment and career progression of our staff.
In return, you will get
For further information concerning this position, please contact Prof. Leon van der Torre or Dr. Réka Markovich.
The Computing Foundations cluster at the School of Computing, The Australian National University, have multiple PhD scholarships available in areas relevant to the types community, including logic, programming languages, systems, formal methods, theory and software engineering.
If you want to do cutting edge research in any of these fields, or a mix thereof, visit our page and get in touch with any of the staff listed.
In particular, Nisansala Yatapanage's areas of interest include formal methods, concurrency verification, safety-critical systems and security verification.
We are looking for a PhD student (4 years) or postdoctoral researcher (3 years) to work on the Isabelle formalization of modal model theory. The work will take place within the Chair of Theoretical Computer Science at LMU Munich under Jasmin Blanchette's supervision with the participation of two external experts: Cláudia Nalon (University of Brasília) and Sophie Tourret (Inria Nancy).
Modal logics are extensions of classical logics with operators that allow for the qualification of truth. Model theory for modal logics is concerned with the interplay between the language (syntax, i.e., the set of its formulas) and its meaning (semantics, i.e., the structures over which the language is interpreted). There are, however, different ways of characterizing meaning for modal sentences and also several (well-established) results that allow for restriction on the sets of structures being considered. This project concerns the formalization in Isabelle of those results for general Kripke structures for generalized modal operators (i.e., of any arity). The goal is to produce a library that could then be used (and possibly extended) for particular applications, in particular those related to proof theory.
The position is categorized as TV-L E13 according to the German salary scale. It includes some teaching obligations. The starting date is flexible. Please contact Jasmin Blanchette for more information or if you want to apply. The application deadline is 15 April 2023.
The Computer Science Group at the GSSI (top ranked computer science department in Italy in 2022 and national department of excellence) invites expressions of interest for open-rank positions in computer science (Open Rank: Tenured Full Professorship, Associate Professorship or Assistant Professorship with Tenure Track). Moreover, it invites expressions of interest for direct calls of researchers. This is a form of direct recruitment that does not include calls from individual universities, but it is a nominative proposal that the university sends directly to the Ministry (Law 230/2005, Art. 1, paragraph 9). A researcher is eligible for a direct call if she/he meets either of the following two criteria: They have been permanently engaged in research or teaching activities outside Italy for at least three years, holding an equivalent academic position in a university or a research institution abroad. The call requires the approval of the National Scientific Qualification Commission (ASN). They have been qualified for specific high-qualification research projects, funded by the European Union or by the Italian Ministry of Education, University and Research (MIUR) and identified with a specific decree, after a positive opinion from ANVUR and CUN. For calls made within three years of winning the research project, approval of the National Scientific Qualification Commission (ASN) is not required.
The main research areas of the Computer Science area are Algorithms, Formal Methods, and Software Engineering. Research in Algorithms at GSSI focuses on computational problems arising in networks and multi-agent systems. The research of the Formal Methods group focuses on complex reactive systems and spans a broad range of topics from languages, to semantic models, and to software verification. The research of the Software Engineering group focuses on the systematic application of engineering approaches to the development of software for autonomous and smart systems. More details are available on the website.
Gran Sasso Science Institute (GSSI)
Gran Sasso Science Institute (GSSI) is an
International centre of excellence for advanced studies and PhD school
established in L'Aquila (Italy).
Despite being founded only in 2012 and stabilized in 2016, after a
three-year successful experimental period, the institute has already
obtained wide recognition at both national and international levels.
The PhD program at GSSI is organized in the scientific areas of
Astroparticle Physics, Computer Science, Mathematics, Regional
Sciences and Economic Geography. Every year, the institute offers PhD
scholarships and postdoctoral grants as well as research internship
opportunities, thus facilitating the attraction of prestigious
scientists in the field of Computer Science.
In 2022, GSSI participated for the first time in the Ministry of University and Research call of ANVUR (Italian National Agency for the Evaluation of Universities and Research Institutes) to evaluate universities in Italy.
In this first participation, the computer science area has been evaluated as the first computer science department in Italy. This recognition gave the computer science area the opportunity to participate in a further call for funding, and together with the mathematics area, was recognized as one of the "Departments of Excellence", obtaining more than 7 million Euros in additional funding. Besides its prestige, this recognition will bring additional permanent positions and significant funds (over one million Euros) for building autonomous systems, IoT, and algorithm-engineering laboratories. Moreover, the GSSI project was ranked first in the specific disciplinary sector among the 11 departments of excellence in computer science and mathematics, with only three of them (including GSSI) concerning Computer Science. The first place is shared with the Scuola Normale Superiore of Pisa and the University of Pisa, two other prestigious Italian institutions.
Working at GSSI
GSSI is the perfect place for young researchers that aim to establish
and consolidate their group and become principal investigators (PIs).
Indeed, these are the main strengths of GSSI as a working environment:
Freedom in selecting research topics and activities.
Entry package aiming at helping newcomers to develop their own
research; ideal conditions to perform excellent research;
availability of open PhD positions and of funding to buy research
resources; access to the three laboratories mentioned above; a
collegial environment welcoming newcomers to joint ongoing research
projects; space to host a research group; funding for travelling and
inviting researchers.
Low teaching duties: teaching only to our PhD students and supervising
PhD students.
Laboratories: Autonomous Systems (service robots and vehicles), IoT,
Algorithm Engineering, High-Performance Computing (HPC).
Young, friendly, non-hierarchical, vibrant, and International environment.
Excellent place to perform interdisciplinary research, e.g., with the
other areas of GSSI, in the context of existing or new projects.
Located in a cosy and medium-size city in the centre of Italy, a city
of science hosting also the University of L’Aquila
and the INFN, Gran Sasso Tech (a joint venture between GSSI and Thales Alenia Space),
companies (like Thales Alenia Space, Leonardo, Sanofi, IZS), good
food, great nature, mountains, lakes, seaside at around 80 km, Rome at
less than 100 Km, etc. The quality of life in L’Aquila is pretty high
and there is also an international Lyceum.
Call for Expression of Interest
We are looking for candidates with an excellent publication record, an
internationally visible research profile, a clear potential to promote
and lead research activities, and a specific interest in teaching
skilled and internationally recruited students at the postgraduate
level.
Applications Applicants should submit their expression of interest by sending:
Applications (and questions regarding the application process) must be submitted in electronic form, preferably by 28 February 2023.
GSSI is committed to gender balance, inclusion and diversity. All expressions of interest will be given proper consideration, independent of ethnicity, religion, age, gender, sexual orientation, or disability.
Disclaimer: Please note that this is not a job advertisement. Based on the received expressions of interest, the Gran Sasso Science Institute will decide whether to open an official call and which selection procedure to follow.
Additional information
The department of computer science of Université Paris Cité has five openings for tenured positions in theoretical computer science, broadly construed, which could be of interest to the readers on this mailing-list:
See the announcements in French here and here.
General description
The positions are tenured (more precisely civil servant positions)
with research, teaching, and administrative duties. Here is the
official description of these types of positions in French academia:
The research profile is quite wide for all these positions: pretty much all of theoretical computer science, in both its `track A' and `track B' flavours, is represented within IRIF.
The teaching profile encompasses all of computer science (i.e., not just theory), with a wide choice of courses at both undergraduate and graduate levels. The teaching language in our computer science department is French—as in most French universities. Accordingly, the interviews for these positions will be carried in French.
IRIF has taken up gender equality issues and published recommendations for hiring committees to help alleviate bias. More information can be found on the page of our commission for gender equality.
Contact information
Contacting people locally is strongly encouraged and allows to provide
assistance navigating the French academic system and tailoring
applications for this type of positions.
Regarding research: - presentation of IRIF - who to contact: the heads of poles and research teams relevant to your research area - IRIF heads: Giuseppe Castagna and Thomas Colcombet
Regarding teaching: - presentation of the computer science department - heads of the department: Carole Delporte, Hugues Fauconnier, and Ralf Treinen
3 year PhD research fellowship available in formal methods at the University of Oslo: Rewrite-based methods for real-time systems.
This PhD project is part of a broader project which aims at developing formal modeling languages and analysis methods that can be successfully applied to complex modern cyber-physical systems.
In particular, the goal of this PhD project is to integrate symbolic analysis methods, such as narrowing analysis and SMT solving, into rewriting-based analysis techniques for real-time and hybrid/cyber-physical systems, and into tools such as Real-Time Maude and Synchronous AADL.
The project also involves researchers at the University Sorbonne Paris Nord, POSTECH Korea, University of Illinois at Urbana-Champaign, and others.
The Department of Philosophy, Linguistics, and Theory of Science at the University of Gothenburg invites applications for one PhD position and several postdocs in Logic. The PhD position is open to all topics in mathematical, philosophical and computational logic within the expertise of the Logic Group. The two postdocs are available on the research project "Taming Jörmungandr: The Logical Foundations of Circularity" lead by Graham E. Leigh and funded by the Knut and Alice Wallenberg Foundation.
Doctoral position in Logic
Postdoctoral researcher in Logic, one or more
Peter Lammich and his group have an opening for a 4 year PhD position in the VESPA project (Verification of Efficient and Secure Parallel Algorithms) at the University of Twente.
We want to apply stepwise refinement techniques in Isabelle/HOL (or another ITP) to develop scalable verification techniques for parallel algorithms, down to their efficient implementations on Multicore CPUs / GPUs.
You will be supervised by Peter Lammich, and work in the Formal Methods and Tools group at the University of Twente, which has a strong expertise in verification of concurrent software.
The PhD position is fully funded, and your salary will be increasing from € 2,541 in the first year to € 3,247 in the last year.
Starting date is (ideally) before June 2023, but later starting dates can be negotiated.
For applications and other details: please follow this link. Application Deadline: 28th February
For more information, feel free to contact Peter Lammich.
This is an announcement for a post-doc position at Université de Montpellier (France). We are seeking candidates holding a PhD in computer science, and with expertise in program verification, algorithms, automated deduction or programming languages.
The aim of the project is to formally verify term indexing algorithms (as used for the implementation of automated theorem provers, logic and functional programming languages, and other symbolic computing applications), in order to produce verified and efficient implementations.
The successful candidate will be employed by Université de Montpellier, and will join the LIRMM research department. The position is for 18 months, starting on March 1st or later. The monthly salary before taxes is between 2674€ and 2762€. The working language can be either French or English.
Interested people can contact Simon Robillard for further information about the position and the application process.
Within the AUTOSARD project, led by Georg Moser (University of Innsbruck) and Florian Zuleger (Vienna University of Technology), both in Austria, there are two openings for 4 year PhD student positions. In AUTOSARD, we target an automated complexity analysis of the most common data structures with good, ie. sublinear, complexity, as they are typically used in standard libraries of programming languages. Our goals are the verification of textbook data structures, the confirmation and improvement (on coefficients) of previously reported complexity bounds, as well as the automated analysis of realistic data structure implementations. For more details, kindly see here.
The PhD positions will be be jointly supervised by Georg and Florian and are either located at Innsbruck or Vienna.
Applications (including CV, short letter of motivation, three references, preferred location) should be submitted to either
no later than March 12, 2023. Informal inquiries may be sent to either Florian or Georg.The city of Innsbruck is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of urban life in this historic town and the Alpine environment provides a high quality of living. On the other hand, Vienna has just last year reclaimed the title of the world’s most liveable city; a title it frequently held in the last years.
Further information on the hosting groups and institutions is available from the following links: - Theoretical Computer Science Group - University of Innsbruck - Formal Methods in Systems Engineering - Vienna University of Technology
Temporary engineer positions at Inria are available for the ``ProofInUse'' consortium.
ProofInUse in short
The ProofInUse consortium is a laboratory for research and development
in the domain of high-assurance software. It is joint between several
academic and industrial partners. The general objective of ProofInUse
is to provide software verification tools, based on mathematical
proof, to industry users.
The objective of ProofInUse is to significantly increase the capabilities and performances of verification environments proposed or internally used by the partners. Beyond a common interest in formal verification techniques, the members of ProofInUse share a common interest in the generic environment Why3 for deductive program verification, developed in the Toccata research group. In particular, ProofInUse aims at integration of verification techniques at the state-of-the-art of academic research, via the Why3 environment.
See also here
Expectations from the candidates
We seek for candidates with as much experience and skills as possible
in several domains among : development using the OCaml language ;
techniques for evaluation, compilation and/or transformation of
programs ; formal methods for software engineering ; formal logics ;
static analysis of programs ; computer-assisted theorem proving ; use
of formal proof environments; knowledge of programming languages Ada,
C, C++ and Rust.
We expect some experience in the field of formal methods of software engineering in a general sense. The typical candidate would be someone who recently defended a master's thesis or a PhD in a related domain.
The research part of the job is significant, the work being expected to lead to academic publications, as exemplified by the publications of the former engineers of ProofInUse (see here). The development activities include a participation to the development of Why3, for which we are interested in candidates with experience in OCaml programming, or similar functional programming languages, and in the practice of shared development using git.
Some skills in the use of a formal proof environment will be a plus.
How to apply
The engineer positions should be filled as soon as possible.
The primary site for the positions is here where you can apply with a CV and a motivation letter.
Do not hesitate to contact Claude Marché directly for more information on the positions.
Cryspen is a small research-oriented company that seeks to apply formal verification tools to build high-assurance production-ready cryptographic software. We have a few open roles at Cryspen right now in Germany and in France.
In particular, we are looking to hire a Software Verification Engineer who will focus on implementing and verifying high-assurance software, which includes writing and maintaining proofs for the code. This position requires expertise in verification frameworks like Coq, Lean, Isabelle, F*, etc. and the willingness to apply them to production software.
To apply go here. For more information or any questions, feel free to send an email.
A postdoctoral position in program semantics and verification is open at the Singapore Institute of Technology (SIT) under the supervision of Prof. David Sanan.
The project aims to minimize the gap between formal verification and efficient industrial applications. Specifically, we focus on constructing a verification framework for software using deductive reasoning, and on the formalization of smart contract semantics, with special attention to the Solidity language.
The candidate will work on formalizing programming language semantics, constructing a framework for scalable verification, and building mechanisms for automatic reasoning on Isabelle/HOL.
Qualifications:
SIT offers highly competitive salaries and is situated in Singapore, a multicultural English-speaking city. Singapore offers high-quality education and healthcare at all levels and very low tax rates.
The position is available full-time for one and a half years in the first instance, with the possibility of renewal(s).
Starting date: as soon as possible.
To apply, send an email with the CV to David Miguel Sanan Baena
The group of André Platzer, the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems, in the Department of Informatics at KIT, Karlsruhe, is recruiting a PhD Student or Doctoral Researcher (full-time, about €4200-4800 gross by TVL E13 depending on experience). Exceptionally qualified applicants for postdoc positions may be considered as well. Our research develops the logical foundations for cyber-physical systems and practical theorem proving tools for analyzing and correctly building such systems, including the theorem prover KeYmaera X, verified runtime monitoring ModelPlex, verified compilation, and provably safe AI techniques. Our techniques are used to analyze the safety of autonomous cars, airplanes and collision avoidance protocols in aerospace applications, robotics, and train control.
Key requirements for successful applications:
The successful candidate is able to quickly get into new research areas and will be responsible for actively engaging in novel research questions, publishing and communicating research results, advising junior students, assisting in research grants, implementation of research results in formal methods or theorem proving tools, and demonstrating their applicability in cyber-physical systems applications.
Faculty / Division: Alexander von Humboldt Professor group on Logic of Autonomous Dynamical Systems, KIT Department of Informatics
Group: The Alexander von Humboldt Professorship, Germany's most highly endowed international research award, is endowed with up to five million euros. With this award, the Alexander von Humboldt Foundation honors internationally leading researchers of all disciplines.
Institute: Institute of Information Security and Dependability (KASTEL) Institute for Reliability of Autonomous Dynamical Systems (VADS) of the Karlsruhe Institute of Technology (KIT)
Starting Date: Immediately
Application Material: Usual material as PDF, including letter, curriculum vitae with references, statement of purpose (a concise two-page essay describing your primary research interests and experience), publications, academic transcripts, etc.
Contact Person: André Platzer
The LaBRI research lab based at the University of Bordeaux is currently seeking highly motivated candidates with excellent academic records and experience in knowledge representation and reasoning (esp. ontologies, description logics, inconsistency and uncertainty handling), database theory, data quality and/or logic in CS to join the Ratio team and take part in the INTENDED AI Chair.
We currently have openings for a two-year postdoc position and a three-year PhD position (which may be preceded by a paid 4-6-month research internship).
The recruited persons will collaborate with myself and other project members on foundational research related to the project's overall theme of developing principled methods for handling imperfect (inconsistent, inconsistent, and/or uncertain) data, by exploiting declarative knowledge and reasoning. Generally speaking, this will involve the definition of formal frameworks for repairing and querying imperfect data, the study of the computational complexity of the associated reasoning tasks, and the development of reasoning algorithms (note that implementation of the developed algorithms is not required, but could be undertaken if so desired).
The precise research topics can be adapted to some degree to take into account the specific background and interests of the hired researchers, so brilliant candidates with an interest for the overall project topic should not hesitate to apply!
A more detailed description of the positions, research environment, desired profiles, and application procedure can be found here.
Applications will be reviewed on regular basis until a suitable candidate is found. The desired starting date is February-April 2023, and should be no later than September 2023.
If you're interested in applying, or simply want more information, please get in touch!