Editor's note As I was preparing the issue #131 of the AAR newsletter, I contacted Larry Wos to ask him for his column and he sent me, as prompt as usual, not one but two columns, asking which was the most appropriate. I told him that both were fine, and that I would gladly include the second one in the following issue, that is #132, the one you are currently reading. Lawrence passed away in the night between the 20th and the 21st of August 2020. What follows is the last column he sent me.
Column after column, my readers have been asked to meet challenges in mathematics or in logic. In this column, I again turn, as I did in a 2016 column, to the world of puzzles. In the 2016 column, I offered puzzles to solve for a person and, far more important, for an automated reasoning program to solve. In that column, I offered a puzzle about five couples, and I also offered a puzzle taken directly from Lewis Carroll. The Lewis Carroll logic puzzle was brought to me by my long-time friend, Ross Overbeek. Overbeek wrote many automated reasoning programs, programs that provided the base for OTTER, William (Bill) McCune's marvelous and powerful automated reasoning program.
In this column, I offer four puzzles, three of which are posed for an automated reasoning program to solve or for you, as a reader, to solve. The fourth puzzle I offer is a puzzle given to me many, many decades ago by the great mathematician I. J. Kaplansky. I shall call that puzzle the coconuts-and-monkey puzzle. I offer this puzzle near the end of this column. the coconuts-and-monkey puzzle is not suggested as a puzzle for an automated reasoning program to solve. The coconuts-and-monkey puzzle is, in fact, difficult to solve for the unaided person. If you are able to have an automated reasoning program solve this fourth puzzle, I will be fascinated to see how that was done. If you solve the puzzle yourself, I would also be interested although, admittedly, not as interested as I would be if a program using automated reasoning solved the puzzle.
My goal in offering puzzles is to interest newer people in automated reasoning, to increase the interest in those already in the field, and, just perhaps, to add to my own knowledge of what can be accomplished with an automated reasoning program. I now pose the puzzles that I promised.
Challenges, in the form of puzzles, for you and your automated reasoning program
The first puzzle I offer is sometimes known as the jobs puzzle.
There are four people: Roberta, Thelma, Steve, and Pete.
Among them, they hold eight different jobs.
Each holds exactly two jobs.
The jobs are chef, guard, nurse, clerk, police officer (gender not implied),
teacher, actor, and boxer.
The job of nurse is held by a male.
The husband of the chef is the clerk.
Roberta is not a boxer.
Pete has no education past the ninth grade.
Roberta, the chef, and the police officer went golfing together.
Question: Who holds which jobs?
Your are challenged to find a means to present this puzzle to an automated reasoning program, to choose which inference rule(s) to use, and, if you intend to use strategy, which strategies to employ. The following clause may provide a guide to representation. the clause informs your program that Roberta and Thelma are two different people.
-EQUALP(Roberta,Thelma).
The following strategy may aid you in solving the first three puzzles I offer. the strategy I have in mind is the set of support strategy. This strategy will prove almost crucial in areas other than puzzle solving. In a 2018 column, the set of support strategy was featured. The set of support strategy restricts a program's reasoning. In OTTER, to use the set of support strategy, you include the list list(sos).
William McCune's program OTTER relies mainly on three of the seven lists. The three lists that are the most significant to use are list(usable), list(sos), and list(passive). the first of the three lists, list(usable), is the list on which you place the axioms for the area you are studying. the clause for reflexivity, x = x, should always be included and placed on list(usable). The reason rests with the definition of the inference rule paramodulation. If the program deduces t != t for some term t, the lack of the clause for reflexivity, x = x, prevents the program from recognizing that a proof has been completed. Your program will not yield UNIT CONfLICT.
The third list, list(passive). is the list on which you place the denial of the conclusion of the theorem to be prove. the discussion of the three lists OTTER mainly relies on is at an end.
Having read and, perhaps, enjoyed the jobs puzzle, I offer a second puzzle, one that I shall call the checkerboard puzzle.
There is a checkerboard whose upper right and lower left squares have been removed. There is a box of dominos that are one square by two squares in size. Can you exactly cover the checkerboard with the dominos?
Your challenge is to find appropriate representation, well-chosen inference rule(s), and, if you choose to use strategy, you are asked to choose the strategy you prefer using. You might decide to avoid the use of strategy.
I now present the third puzzle, a puzzle that I call the billiardball puzzle. This puzzle is clearly very, very difficult for a person to solve. Decades ago, Steve Winker enabled an automated reasoning program to solve the puzzle.
There are twelve billiard balls, eleven of which are identical in weight. The remaining ball--the odd one--has a different weight. You're not told whether it is heavier or lighter. You have a balance scale for weighing the balls. Can you find which ball is the odd ball in three weighings, and also find out whether it is lighter or heavier than the others?
As in the two puzzles that precede the billiardball puzzle, you are asked for appropriate clauses, a good choice from among the inference rules that may be offered by your program, and asked to choose whichever strategy you prefer using. Again, you might choose to avoid the use of strategy.
I now come to the Kaplansky puzzle, the coconuts-and-monkey puzzle. I know of no approach for asking an automated reasoning program to attempt to solve this puzzle.
Three men were shipwrecked on an island whose only other inhabitant was a monkey.
Although fresh water was in abundance, food appeared to be a problem.
Therefore, when trees bearing coconuts were found, the three men harvested all they could find.
Because it was getting late, they buried the coconuts, planning to divide them equally in the morning.
At midnight, the tallest of the three men awoke and decided to confiscate some of the buried coconuts for himself.
Unaware of what occurred at midnight, the shortest man dug up the buried coconuts, took one third of them for himself,
found that one coconut remained, and he have that to the monkey.
The third man, unaware of what occurred earlier in the night, dug up the buried coconuts, took one third of them,
buried two thirds of them, and gave the monkey the extra coconut he realized had remained.
In the morning, all three men pretended that they had each slept through the night.
They retrieved the buried coconuts, divided them equally and found that one coconut remained.
They gave that coconut to the monkey.
How many coconuts did they harvest?
I hope that you have enjoyed trying to solve the puzzles, and, even more, enjoyed attempting to have an automated reasoning program solve one or more of the puzzles.
I would enjoy hearing from you by e-mail and learning of your successes, especially those in which automated reasoning played a key role.
I can be reached by e-mail at wos@cs.anl.gov.
Editor's note: I left the end of the column as is although the email address is no longer active. In my opinion, this last paragraph illustrates Larry Wos's insatiable enthusiasm for automated reasoning best.
Former and current presidents of CADE Inc. join to mourn the loss of Larry Wos, automated theorem proving pioneer, founder of CADE (the international Conference on Automated Deduction), AAR (the Association for Automated Reasoning), and JAR (the Journal of Automated Reasoning), and AAR President from 1986 to 2020.
Born in Chicago to Polish immigrant parents, a background that he was fond to remember with pride, Larry Wos was an accomplished mathematician and computer scientist with an exceptional vision for theorem proving, an inexhaustible enthusiasm for its application to mathematics, especially logic and algebra, and a vivid curiosity for computer experiments. He achieved so much while being blind, and there was a certain playfulness about him, as if research was a bit like a game or a puzzle, where he found joy in the discovery of patterns.
After studying at the University of Chicago (BS and MS) and at the University of Illinois at Urbana-Champaign (PhD), Larry Wos spent his entire career at the Mathematics and Computer Science (MCS) Division of the Argonne National Laboratory, at Argonne, near Chicago. Argonne was the birth place of resolution: (John) Alan Robinson alternated summer jobs at Argonne and at Stanford University in the years 1961-1966, with an implementation of the Davis-Putnam procedure as initial task for the summers at Argonne. It was at Argonne that Robinson worked on resolution and unification in 1962-1964, writing his milestone paper on "A machine-oriented logic based on the resolution principle" in 1963. Larry Wos, at Argonne since 1957, seized the moment and developed Argonne into the cradle of automated theorem proving.
Larry Wos understood right away the power of resolution, as well as the need to control it by appropriate strategies. Thus, he devised the set-of-support strategy, and the year 1965 saw the publication in JACM of both Robinson's "A machine-oriented logic" and Wos' paper "Efficiency and completeness of the set of support strategy in theorem proving" with Daniel F. Carson and George A. Robinson as second and third authors, respectively. Control strategies, or search plans, remained central in Larry's research and in his relentless experimentation with theorem provers. This was the reason why he preferred the name automated reasoning over automated deduction, feeling that reasoning better captures the mix of inference and search that constitutes theorem proving by machine. This was also a motivation for the name of the Association for Automated Reasoning. When the IJCAR conference series was being planned around 2000, Larry was delighted that the new event would be called International Joint Conference on Automated Reasoning.
Larry Wos also was a pioneer in recognizing how crucial it was to start building equality into resolution. To this end, he initiated the concept of demodulation, a first attempt at mechanizing the replacement of equals by equals, later systematized by others as rewriting or simplification by equations controlled by a well-founded ordering. His paper on "The concept of demodulation in theorem proving" with George A. Robinson, Daniel F. Carson, and Leon Shalla, as second, third, and fourth authors, respectively, appeared in JACM already in 1967. Even more importantly, George A. Robinson and Larry Wos were the first to propose a paramodulation inference rule in their paper "Paramodulation and theorem-proving in first-order theories with equality," which appeared in 1969 in a volume of the historic Machine Intelligence series, edited by Donald Michie and Bernard Meltzer, for Edinburgh University Press. Both papers were reprinted in the volume "Automation of Reasoning II: Classical Papers on Computational Logic 1967-1970" edited by Joerg Siekmann and Graham Wrightson in 1983 for Springer-Verlag.
Not only was Larry a discoverer of strategies and inference rules, he was also exceptional in leading the theorem proving group at Argonne, including Larry J. Henschen of Northwestern University, Ewing (Rusty) Lusk, the late William W. (Bill) McCune, Ross Overbeek, Robert (Bob) Veroff, later at the University of New Mexico, Steven K. Winker, and in connecting with other scientists invited to Argonne, including Deepak Kapur, Hantao Zhang, and one of us (Maria Paola, right after her PhD at SUNY Stony Brook, and later while at the University of Iowa). Larry Wos also collaborated with numerous mathematicians, especially from the University of Chicago: indeed, Larry was fond of applying the Argonne provers, mainly Bill McCune's Otter, to search for proofs of mathematical theorems, constantly seeking shorter or more elegant proofs, as if he wanted to show that automated theorem proving can display not only brute force, but also insightfulness and beauty.
Many of his quests were reported in his books, including "Automated Reasoning: 33 Basic Research Problems" (1988), "The Automation of Reasoning: an Experimenter's Notebook" (1996), "A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning" (1999), and "Automated Reasoning and the Discovery of Missing and Elegant Proofs" (2003), the latter two written with Gail W. Pieper, coordinator of writing and editing at MCS. These books show how keen Larry was on scientific writing, directed also to the non-specialists. Larry maintained an online page to report on his theorem proving experiments.
Under Larry's leadership, the Argonne group played a key role in the establishment of CADE, JAR, and AAR. CADE is the oldest conference in automated reasoning: prior to its inception, papers in theorem proving and related topics could only appear at theory conferences or artificial intelligence conferences, while CADE provided for the first time a dedicated venue. After a Symposium on Automatic Demonstration, held at Rocquencourt, France, in 1968, an IEEE Workshop on Automated Theorem Proving was organized by Larry Wos and Larry Henschen at Argonne in 1975. According to Gérard Huet, CADE was probably created in 1977, and the 1975 workshop at Argonne was named CADE-1 when the history of the conference was reconstructed. CADE returned triumphantly to Argonne for its ninth edition in 1988, organized by Rusty Lusk and Ross Overbeek. It was at CADE-9 that Bill McCune released the first publicly available version of Otter. It was at CADE-9 that Larry Wos gave a memorable banquet speech at the Natural History Museum in Chicago, delving on a comparison of theorem proving with gambling that he was fond of.
The Journal of Automated Reasoning, founded in 1985 with Larry Wos as Editor-in- Chief and Gail Pieper as Managing Editor, played the same role at the journal level: prior to its creation, journal papers in automated reasoning could only be submitted to theory, artificial intelligence, or symbolic computation journals, while the foundation of a dedicated journal witnessed and furthered the growth of the field. The first issue of JAR in March 1985 included a foreword by Larry Wos, and an overview paper co-authored by Larry with Fernando Pereira, Robert Hong, Robert S. Boyer, J Strother Moore, Woodrow Wilson (Woody) Bledsoe, Larry J. Henschen, Bruce G. Buchanan, Graham Wrightson, and Cordell Green.
The Association for Automated Reasoning was established in 1983, with Larry Wos as President, Bill McCune as Secretary, and Larry Henschen as Treasurer. The first issue of the Newsletter appeared in March 1983, with Gail Pieper as Technical Editor. Larry was a warm supporter of the AAR as a way to connect people beyond conference attendance. He collaborated enthusiastically with all AAR Secretaries (after Bill: Bob Veroff, Maria Paola Bonacina, Amy Felty, Wolfgang Ahrendt, Martin Giese, and current Secretary Philipp Ruemmer), and AAR Newsletter Editors (after Gail: Jasmin Blanchette, and current Editor Sophie Tourret), relentlessly contributing to the newsletter reports of theorem proving experiments and theorem proving challenges. Once he told Maria Paola: "Don't you ever leave CADE and the AAR: we can't do it without you." To Amy Felty he wrote: "Amy, you're a gem." Larry was eager to debate with people over the phone and by email, with many long-term correspondents, including Michael Beeson, Deepak Kapur, and Geoff Sutcliffe.
Larry Wos was honored with the first Automated Theorem Proving Prize of the American Mathematical Society (with Steve Winker) in 1982 and with a liber amicorum, entitled "Automated Reasoning and its Applications: Essays in Honor of Larry Wos", edited by Bob Veroff for the MIT Press (1997). Larry Wos won the first Herbrand Award in 1992, in recognition of his research and his role as a founder of automated reasoning. His acceptance speech in the CADE-11 proceedings is still inspiring today. The Herbrand Award to Bill McCune in 2000 sealed the pioneering season when Argonne was a beacon for theorem proving during almost forty years, a season that would not have been possible without Larry's leadership. He will be remembered by many in automated reasoning and beyond.
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 Award selection committee, instituting new awards, etc.
The members of the board of trustees in the period summer 2019 until summer 2020 were:
The terms of Jürgen Giesl, Marijn Heule, and Andrew Reynolds end, and three new trustees need to be elected. In addition, the term of office of Nicolas Peltier as IJCAR 2020 programme chair ended after the IJCAR conference, and he is replaced by the CADE-28 program co-chair André Platzer.
The following candidates were nominated and their statements, in alphabetic order, are below:
In this year the number of nominees matches the number of places to be filled, which means that no election is required to determine the new board of trustees.
The new board of trustee is:
On behalf of the AAR and CADE Inc., I would like to thank Jürgen Giesl for his service on the board of trustees since 2014. I would like to congratulate Marijn Heule and Andrew Reynolds for being reelected, and Renate Schmidt who will join the board as a new trustee!
CADE and IJCAR are, together with SAT, my favorite conferences. They stimulate exciting and important research. It has been a pleasure to take part in most CADE and IJCAR conferences since 2012 and several of its program committees. I am honored to serve as a trustee since 2017.
The focus of my research in recent years has been on two important challenges in automated deduction: 1) how to validate that the complex techniques developed by the community produce correct results; and 2) how to exploit the power of big computer clusters. Although my work has targeted mainly SAT and QBF solving, these challenges are also important for first-order logic and beyond. I am interested in and would like to promote lifting successes from propositional logic to richer logics.
Researchers in the community have created very powerful tools from CaDiCaL to Vampire to Z3. These tools are successful in industry as well. I am supportive of attracting paper submissions that describe how these tools can make a difference in solving relevant problems. Such papers can have a broad impact. I am also supportive of the requirement that experimental evaluations must be reproducible by the reviewers and the community at large.
I prefer that all publications in automated reasoning become Open Access, including the proceedings of CADE/IJCAR and articles in JAR. This would make the research more accessible, which in turn can enlarge the community. A frequent argument against Open Access is the perceived financial impact on the authors/participants. I believe that we can deal with this issue via sponsoring and agreements with funding agencies.
The current structure of alternating yearly between CADE and IJCAR and joining FLOC every four years is the right balance between focusing on the own community and ensuring visibility to related communities. I am in favor of coordinating the CADE/IJCAR/FLOC conference locations to improve the geographic distribution. Although most CADE attendees come from Europe, I would like to stimulate participation from researchers in North America. Organizing CADE/IJCAR regularly in the US or Canada should therefore be continued. I am therefore thrilled that CADE will come back to Pittsburgh in 2021 and I am dedicated to make it a success as local organization co-chair.
CADE was the first conference I attended as a PhD student and is my favorite conference to attend. I have always found the CADE community to be great at stimulating collaboration and new ideas among a range of researchers within automated deduction. I have sub-reviewed numerous papers, and had the pleasure to serve on the program committee for CADE 2015, CADE 2019, and IJCAR 2020. I also served as the co-organizer of workshops and competitions for CADE 2015 in Berlin, and again as the chair of workshops and competitions for IJCAR 2020.
My research has focused on developing techniques in Satisfiability Modulo Theories (SMT) solvers. I am one of the main developers of the SMT solver CVC4, which is a frequent participant in the CASC competition. While most of the SMT community focuses on quantifier-free reasoning, my research has focused on new approaches that combine background theories and quantified formulas, and hence often aligns closely with the research at CADE. In the coming years, more tools within the automated theorem proving community will benefit from SMT solver back ends, and conversely SMT solvers will learn from techniques that target other logics.
As a member of the steering committee, I will further emphasize putting foundational research into practice. I believe that the many great ideas that come out of the CADE community should be applied more actively in academia and industry. I believe that competitions like CASC and SMT COMP are a great driving force in encouraging researchers to develop tools that are efficient, robust and trustworthy. I believe that the incorporation of a reproducibility section in the review process at CADE has been a positive development, especially for tool papers.
I believe the CADE community should actively seek cross-fertilization with related fields like software verification and automated synthesis. Automated theorem provers already can play a more active role in these areas. For instance, constrained Horn clause solving and syntax-guided synthesis are two application-inspired disciplines that are converging with techniques for automated theorem proving. CADE is potentially a great place to bring these communities together. In particular, I believe it is important to encourage a broad range of workshops at CADE, as this is a great way to encourage researchers from neighboring fields to attend CADE.
I am honoured to have been nominated again for the CADE Board of Trustees. My first CADE was in 1999. What I always loved about CADE is the exciting progress made every year and the enthusiasm of young researchers stepping up. The high-quality mix of theoretical and practical research was very much evident again at this year's IJCAR. As was said in one of the invited talks, Automated Reasoning has seen the fastest development in any research area. Progress is indeed impressive; we see hard problems are being tackled and solved that were outside reach just a few years ago.
What do I want to see happen in the CADE community? I think the AR Summer School is such an important educational activity for young scientists that it should become a regular event.
There is an uncomfortable matter concerning the Herbrand Award process that needs to be urgently reviewed and rectified by the Board of Trustees. Two years ago the Herbrand Award selection process was changed. This did not involve a wide consultation and no discussion took place in the community. Many may therefore not have noticed the change. I think representativeness and sequencing needs to be looked at.
In conjunction with the 2019 CADE trustee elections, a vote on a motion brought forward by the CADE trustees was held, and as a result the CADE bylaws defining the election of trustees were updated to:
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected electronically by the entire CADE membership. The CADE trustees decide on a voting procedure for the trustee election. The procedure will be published on the CADE homepage. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
The voting procedure is therefore no longer hard-coded in the bylaws, but can be chosen by the board of trustees. The choice of procedure was discussed by the CADE trustees via email during spring 2020, and in the light of the issues earlier indentified in the CADE version of the Single Transferrable Vote (STV) procedure it was decided to replace STV with a Condorcet method in future trustee elections. More specifically, the selected voting procedure for trustee elections is the Condorcet completion Minimax-PM. It is the current default voting system at the Condorcet Internet Voting Service (CIVS) supported by Andrew Myers, see here. The implementation at Cornell has been used for some time in similar elections, for instance for the TABLEAUX Steering Committee elections. CIVS completely automates the counting of votes, and does not disclose the votes by individual people, not even to the person arranging the election. In rare cases in which Minimax-PM is not able to resolve ties, a second election round will be organised.
In 2020, since the number of trustee nominations matched the number of places to be filled, no election had to be held; we will have wait until 2021 to see the new voting procedure in action and collect experiences with CIVS.
CADE will carefully monitor the development of the COVID-19 pandemic, and take guidance from from the health authorities, to determine whether CADE-28 will be physical or online.
Call for Papers
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 STEM, implementations, and the use/contribution of automated
deduction in AI, are solicited. CADE-28 aims to present research that reflects
the broad range of interesting and relevant topics in automated deduction.
Important Dates (Conference)
Call for Workshops
Workshop proposals for CADE-28 are solicited. The workshops will take place
before the conference. Both well-established workshops and newer ones are
encouraged. Similarly, proposals for workshops with a tight focus on a core
automated reasoning specialization, as well as those with a broader, more
applied focus, are welcome. Please provide the following information in your
application document:
Call for Tutorials
Tutorial proposals for CADE-28 are solicited. The tutorials will take place
before the conference. Tutorials are expected to be either half-day or full-day
events, with a theoretical or applied focus, on a topic of interest to CADE-28.
Proposals should provide the following information:
Call for Competitions
The CADE ATP System Competition (CASC), which evaluates automated theorem
proving systems for classical logics, has become an integral part of the CADE
conferences. Further competition proposals are solicited. The goal is to foster
the development of automated reasoning systems and applications, in all areas
relevant to automated deduction in a broad sense. Proposals should include the
following information:
Important Dates (Workshop/Tutorials/Competitions)
Submission Instructions
Proposals for workshops, tutorials, and competitions must be submitted to the
CADE-28-WTC track via easychair.
More information is available on the conference's web page, and on the online CfP.
The ACM Symposium on Applied Computing (SAC) has gathered scientists from different areas of computing over the last thirty years. The forum represents an opportunity to interact with different communities sharing an interest in applied computing.
Software Verification and Testing Track (SVT)
The Software Verification and Testing track aims at contributing to the
challenge of improving the usability of formal methods in software
engineering. The track covers areas such as formal methods for
verification and testing, based on theorem proving, model checking,
static analysis, and run-time verification. We invite authors to submit
new results in formal verification and testing, as well as development
of technologies to improve the usability of formal methods in software
engineering. Also are welcome detailed descriptions of applications of
mechanical verification to large scale software.
Topics
Possible topics include, but are not limited to:
Important dates
More information is available on the symposium's web page.
The topic of the track covers an important field of research in Artificial Intelligence: Knowledge Representation and Reasoning (KRR) is dedicated to representing information about the world in a form that a computer system can utilise to solve complex tasks. Examples of knowledge representation formalisms include semantic nets, systems architecture, frames, rules, and ontologies. Some examples of automated reasoning engines include inference engines, theorem provers, and classifiers. KRR track will be a venue for all the researchers and practitioners working on the fundaments and applications of reasoning, and cross-fertilisation among different areas (e.g., Argumentation and Belief Revision). ACM SAC is ranked CORE:B, MAS:A-, SHINE:A. The average acceptance rate per track is under 25%. KRR track is organised for the fifth consecutive year at SAC.
Topics
Knowledge-representation is the field of artificial intelligence that focuses on designing computer representations that capture information about the world that can be used to solve complex problems. Its goal is to understand and build intelligent behaviour from the top-down, focusing on what an agent needs to know with the purpose to behave intelligently, how this knowledge can be represented symbolically, and how automated reasoning procedures can make this knowledge available as needed. In KRR a fundamental assumption is that an agent's knowledge is explicitly represented in a declarative form, suitable for processing by dedicated reasoning engines. Topics of interest include:
Deadlines and Important Dates:
More information is available on the conference's web page.
VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas.
Scope
The program of VMCAI 2021 will consist of refereed research papers as well as invited lectures and tutorials. Research contributions can report new results as well as experimental evaluations and comparisons of existing techniques.
Topics include, but are not limited to:
Important Dates AoE (UTC-12)
More information is available on the conference's web page.
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 2021 is the twenty-fourth event in the series.
Main Conferences (29 March-1 April)
Important Dates
More information is available on the joint conferences' web page.
The FSEN Steering and Organizing Committees are monitoring the situation surrounding COVID-19, and are aware of the restrictions and uncertainty that people are facing this period, complying with local and international rules on travel restrictions. Therefore FSEN 2021 will be held as a mixed event, offering virtual presentation as option to participants. All accepted papers will be published in the conference proceedings, regardless of whether a physical or virtual presentation is given. More details will follow in the course of time via the FSEN 2021 website.
Fundamentals of Software Engineering (FSEN) is an international conference that aims to bring together researchers, engineers, developers, and practitioners from academia and industry to present and discuss their research work in the area of formal methods for software engineering. Additionally, this conference seeks to facilitate the transfer of experience, adaptation of methods, and where possible, foster collaboration among different groups. The topics of interest cover all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry and promoting their integration with practical engineering techniques.
Topics of Interest
The topics of this conference include, but are not restricted to, the following:
Important Dates
More information is available on the conference's web page.
LATA is a conference series on theoretical computer science and its applications. LATA 2020 & 2021 will reserve significant room for young scholars at the beginning of their career. It will aim at attracting contributions from classical theory fields as well as application areas.
LATA 2020 & 2021 will merge the scheduled program for LATA 2020, which could not take place because of the Covid-19 crisis, with a new series of papers submitted on this occasion.
Scope:
Topics of either theoretical or applied interest include, but are not limited to:
Deadlines (all at 23:59 CET):
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 2020 wasn’t held in Turin as planned because of the COVID-19 outbreak. Nonetheless the significant number of submissions and registrations testified the interest for TYPES in our community, motivating us to plan publishing post-proceedings. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings.
Submission to this post-proceedings volume is open to everyone, also to those who did not submit a contribution to the conference.
We would like to invite all researchers that study and apply type systems to share their results. In particular, we welcome submissions on the following topics:
Important dates:
Details:
Papers have to be formatted with lipics.cls and adhere to the style requirements of LIPIcs.
The recommended length of a paper is 12-15 pages, excluding front-page(s) (authors, affiliation, keywords, abstract, ...), bibliography and an appendix of max 5 pages. Longer submissions will not be considered.
In case of questions, please contact one of the editors.
Editors:
FM 2021 is the 24th international symposium in a series organised by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The symposia have been notably successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral work. FM 2021 will be both an occasion to celebrate and a platform for enthusiastic researchers and practitioners from a diversity of backgrounds to exchange their ideas and share their experience.
FM 2021 will highlight the development and application of formal methods in a wide range of domains including software, cyber-physical systems and integrated computer-based systems. We are in particular interested in the application of formal methods in the areas of systems-of-systems, security, artificial intelligence, human-computer interaction, manufacturing, sustainability, power, transport, smart cities, healthcare, biology. We also welcome papers on experiences from application of formal methods in industry, and on the design and validation of formal methods tools.
Topics of Interest
FM 2021 encourages submissions on formal methods in a wide range of
domains including software, computer-based systems,
systems-of-systems, cyber-physical systems, security, human-computer
interaction, manufacturing, sustainability, energy, transport, smart
cities, and healthcare. We particularly welcome papers on techniques,
tools and experiences in interdisciplinary settings. We also welcome
papers on experiences of formal methods in industry, and on the design
and validation of formal methods tools. The broad topics of interest
for FM 2021 include, but are not limited to:
Important Dates
More information is available on the conference's web page.
The aim of GandALF 2020 is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization.
Due to the outbreak of COVID-19 and the current difficulties for traveling, it has been decided to organize the symposium online. The organization will be as follows:
To maximize the online attendance to the conference, the registration is free of charge but mandatory.
Registration can be done on the website of the conference, where more information is available.
FMCAD'20 is the twentieth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing ground-breaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
The program comprises presentations of 28 papers, 3 tutorials and 2 keynotes, a student forum, and the Hardware Model Checking Competition.
Short presentations will be given on Zoom and longer versions of the talks will be made available for download.
Registration is now open and free.
More information is available on the conference's web page.
The symposium will be held in an in-person/virtual hybrid format in Norfolk, VA, USA, possibly transitioning to fully virtual depending on the COVID-19 situation.
Theme of the Symposium:
The widespread use and increasing complexity of mission-critical and
safety-critical systems at NASA and in the aerospace industry require
advanced techniques that address these systems' specification, design,
verification, validation, and certification requirements. The NASA
Formal Methods Symposium (NFM) is a forum to foster collaboration
between theoreticians and practitioners from NASA, academia, and
industry. NFM's goals are to identify challenges and to provide
solutions for achieving assurance for such critical systems. New
developments and emerging applications like autonomous software for
Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced
separation assurance algorithms for aircraft, and the need for
system-wide fault detection, diagnosis, and prognostics provide new
challenges for system specification, development, and verification
approaches. Similar challenges need to be addressed during development
and deployment of on-board software for both spacecraft and ground
systems. The focus of the symposium will be on formal techniques and
other approaches for software assurance, including their theory,
current capabilities and limitations, as well as their potential
application to aerospace, robotics, and other NASA-relevant
safety-critical systems during all stages of the software life-cycle.
The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Research Group, comprised of researchers spanning six NASA centers. NFM2021 is being organized by the NASA Langley Formal Methods Team.
Topics of Interest:
We encourage submissions on cross-cutting approaches that bring
together formal methods and techniques from other domains such as
probabilistic reasoning, machine learning, control theory, robotics,
and quantum computing among others. Topics of interest include, but
are not limited to, the following aspects of formal methods:
Important Dates:
More information is available on the symposium'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.
The LFMTP 2020 workshop adopts a post-proceedings publication model. The workshop itself took place on 29-30 June 2020 online, jointly with IJCAR and FSCD. Now that the workshop has concluded, we solicit submissions of full papers for the post-proceedings of LFMTP 2020, which will go through the normal peer-review process. Submission is open to all; attendance at the workshop is not prerequisite.
Submissions related to the following topics are welcome:
Important Dates
All deadlines are established as the end of day (23:59) AoE.
More information is available on the workshop's web page.
Research, work in progress, position and student papers were welcome. List of topics of interest includes (but is not limited to):
Important Dates
More information is available on the workshop's web page.
CMCS 2020 will be held virtually, as a series of approximately three hour sessions spread across five weeks, according to the following tentative schedule:
The exact schedule will be determined and announced in August. Registration will be free (details will follow), but please subscribe to the coalgebra mailing list for updates.
Objectives and scope
Established in 1998, the CMCS workshops aim to bring together
researchers with a common interest in the theory of coalgebras, their
logics, and their applications. As the workshop series strives to
maintain breadth in its scope, areas of interest include neighbouring
fields as well.
Topics of interest include, but are not limited to, the following:
More information is available on the workshop's web page.
This Special Issue on Confluence aims to publish recent advances presented at, but not restricted to leading conferences and workshops such as IWC (collocated with FSCD in recent editions: FLoC 2018, FSCD 2019, Paris Nord Summer of LoVe 2020). Submissions of papers related to aspects of confluence such as commutation, ground confluence, nominal confluence, completion, CP criteria, decidability, complexity, system and tool descriptions, certification, and applications of confluence, are welcome. All submissions will pass a thorough and rigorous reviewing process, according to the standards of MSCS. The reviewing process of each paper will start as soon as it is submitted, and accepted papers will undergo production before being published online in MSCS.
Submissions should be submitted to the ScholarOne system.
When submitting your paper please select the Special Issue on "Confluence" from the drop-down list on the ScholarOne system, as this is the only way the papers can be correctly tagged for this special issue.
Guest Editors:
Deadline: 31 January 2021
The organization of the autumn school on logic and constraint programming invites you to participate in this year’s school (September, 18-19, virtually in Calabria), co-located with ICLP. It promises to be an interesting session -- for students, as well as for more senior researchers -- in which Marc Denecker discusses the informal semantics of logic programs (is negation-as-failure actually classical?), Peter Stuckey takes on the role of Trojan horse, convincing us to use Minizinc instead of logic programming, Martin Gebser provides unique insights in the magic he uses for tackling industrial applications with answer set programming, and Elena Bellodi will probably talk about probabilistic logic programming.
The courses will be run as a hybrid model in which the first two hours are thought live, and for the last two hours, a recording will be made available.
The abstracts of these talks are included on the website.
Registration is included in the ICLP registration and can be done via this link.
The talks will be a mixture of live sessions and pre-recorded videos.
More information is available on the school's web page.
Applications are invited for a one-year postdoctoral position at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and reviews of applications will be conducted as they are received.
The project within which the appointment is to be made concerns the development of a framework that supports the encoding of rule-based relational specifications and the process of reasoning about such specifications through the encoding. A defining characteristic of the project is its focus on the so-called higher-order abstract syntax approach to representing objects that embody a binding structure. Ongoing work is aimed at developing systems for reasoning about specifications encoded in linear logic as well as in the dependently typed lambda calculus LF. The group is also interested in furthering its earlier work that has demonstrated the benefits of higher-order representations of syntax in the verification of compilers and transformers for functional programming languages. Another direction of investigation is that of enhancing the logic underlying the Abella proof assistant (see http://abella-prover.org) with the capability of predicate quantification and on exhibiting the usefulness of such an enhancement through a collection of targeted reasoning applications. The successful candidate will be expected to participate in and help lead the work in some of these directions.
To be suitable for the position, the candidate should be broadly conversant with the areas of computational logic and programming languages and should have the mathematical and programming skills necessary for conducting research in them. Some particular facets that would be help in engaging immediately with the research problems are a prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and similar logical systems.
Please feel free to contact Gopalan Nadathur for more details about the topics of research within the project, the necessary background and other relevant details about the position. To view the official announcement, please visit this URL.
This site also provides details about how to apply and serves as the portal for applications. The application process will require you to submit a letter indicating your interest, a current CV, one or two of your papers broadly related to the topics of research and the names and contact details for two references who might be contacted as part of the application review process. Note that a prerequisite for employment is a doctoral degree in Computer Science or closely related field.
The International Max Planck Research School on Trustworthy Computing (IMPRS-TRUST) is a new graduate program jointly run by the Max Planck Institute for Informatics, the Max Planck Institute for Software Systems, Saarland University, and TU Kaiserslautern.
The IMPRS-TRUST offers a PhD program upon successful completion of which students receive a Doctoral Degree in Computer Science from Saarland University or TU Kaiserslautern. The program is open to students with a bachelor’s or master’s degree in computer science (or an equivalent degree). Successful candidates will typically have ranked at or near the top of their classes, have already engaged in research and published their results, and be highly proficient in written and spoken English.
Admitted students receive full funding to cover their living expenses and tuition fees. They enjoy a research-oriented education with close supervision by world-renowned scientists in a competitive, yet collaborative, environment rich in interaction with other students, post-docs, and scientists.
Students admitted to IMPRS-TRUST can enroll at either Saarland University or at TU Kaiserslautern. PhD projects are jointly supervised by scientists of the two Max Planck Institutes and their colleagues at the computer science departments at Saarland University and TU Kaiserslautern.
Applications are accepted all year round; the current round closes on December 31st, 2020.
Further information, including instructions on how to apply, can be found here.
Applications are invited for a postdoctoral or research faculty position with the Systems Software Research Group at Virginia Tech on DARPA-funded projects at the intersection of program analysis, verification, and security. A particular focus of the position is static and dynamic program analysis, especially at the binary level, for automatic exploit generation with an underlying basis in semantics and logic. Additional thrusts include logic frameworks for formal reasoning of non-exploitability.
Computer science PhD graduates with a background and publication record in program/binary analysis, verification, or security is sought. The position has no teaching obligations.
Interested candidates are requested to contact Prof. Binoy Ravindran with a CV or for any questions.
In the near future, the University of Strathclyde will announce a call for five-year research positions leading to permanent appointments. Indeed, it is reassuring to see the university continue recruitment despite the Covid situation. The Mathematically Structured Programming group in the Department of Computer and Information Sciences welcomes applications from type theorists and semanticists, and would be happy to help you develop an application. Please contact Neil Ghani if you are interested, or anyone else from the group if you have questions.
The MSP group
The MSP group's vision is to use mathematics to understand the nature of computation, and to then turn that understanding into into the next generation of programming languages. We use ideas from category theory, type theory, and logic to do so. The group consists of Dr Robert Atkey, Dr Ross Duncan, Professor Neil Ghani, Dr Jules Hedges, Dr Clemens Kupke, Dr Jérémy Ledent, Professor Radu Mardare, Dr Conor McBride, Dr Fredrik Nordvall Forsberg, Professor Glynn Winskel, and our PhD students.
For more information, please see our group website, and our individual websites linked from there.
Glasgow and Scotland
The University of Strathclyde is located in the heart of Glasgow, which Lonely Planet Travel Guides hail as "one of Britain's most intriguing metropolises". It is less than an hour away by car or public transport from the Scottish Highlands. Southern Scotland provides a particularly stimulating environment for researchers in theoretical computer science, with active groups in this area at Heriot-Watt University, the University of Edinburgh, the University of Glasgow, the University of St. Andrews, and the University of Strathclyde.
Applications are welcome in research areas that complement the existing strengths of the Formal Analysis, Theory and Algorithms section (FATA) and the Glasgow Systems Section (GLASS). Relevant topics include programming language foundations (including session types for concurrent and distributed systems) and formal methods (including process algebras, modelling and analysis of complex and reactive systems, model checking and bigraphs).
The post-holder will develop, lead and sustain research of international standard in Computing Science; contribute to teaching, assessment, project supervision and curriculum design at undergraduate and postgraduate levels; and participate in School management and organisation.
For appointment at Reader you will have an outstanding track record of national and international distinction and leadership in research, including publications, income, and awards, bringing external recognition and distinction to yourself and the University.
Since 1957, when Glasgow became the first university in Scotland to have an electronic computer, we have built a reputation for the excellence of our Computing Science research and our graduates. Today, our School is one of the foremost in the UK, setting itself the highest standards in research, and research-led learning and teaching.
In the UK's 2014 independent research exercise, we are rated top in Scotland for research impact with 68% of our impact judged world-leading and 32% internationally excellent. In the overall research ranking, our School was judged equal 16th amongst UK computer science departments, rising to 10th position on research volume with 84% of all research judged world-leading or internationally excellent. We are 6th in the UK on research intensity-weighted GPA rank order (GPA * % returned).
Our School is ranked 7th in the UK in The Complete University Guide 2020. Glasgow Computing is renowned for research and teaching at the intersection of theoretical and applied Computing, and our undergraduate degree programmes are underpinned by a deep theoretical understanding. 93% of our undergraduates are in positive employment (91% in professional destinations) and have a 20% higher salary than the average (Destinations of Leavers from Higher Education 2016-17, DiscoverUni).
For more information, including the job description, see here (reference number 040665), here and here.
For informal inquiries please contact Professor David Manlove
Please note that the above positions require a Scottish Credit and Qualification Framework level 12 (PhD) or equivalent in Computing Science or closely related discipline, or equivalent as evidenced by relevant teaching experience.
It is the University of Glasgow’s mission to foster an inclusive climate, which ensures equality in our working, learning, research and teaching environment.
We strongly endorse the principles of Athena SWAN, including a supportive and flexible working environment, with commitment from all levels of the organisation in promoting gender equity.
Job description
You will be working on the project POSTMAN (Powering SMT Solvers by Machine Learning).
The project POSTMAN aims at a breakthrough in the field of
Satisfiability Modulo Theories (SMT) by developing Machine
Learning (ML) methods targeted at critical parts of SMT procedures.
To solve real-world problems, many tools rely on SMT by translating the problems into a logic formulation and delegating their solution to a solver. SMT is thus at the heart of today's large verification toolchains, run continuously on thousands of CPUs by major software and hardware companies around the world.
The project will advance SMT solving by developing ML methods that prune the search space of the solvers. Unlike the current search methods, ML allows taking into account a large number of observations made during the search.
Guiding methods will be developed at various levels of abstraction, focusing on two critical problems in SMT: solving of quantified formulas and solving of sets of related formulas. The grand challenges for ML are to learn and represent abstract objects under semantic constraints and to employ interpretable learning in combination with reasoning.
The expected outcome of the project is a range of new powerful methods combining ML techniques with current logic-based SMT approaches, providing a significant improvement over the state-of-the-art. The methods will be integrated in a number of systems and deployed in major SMT applications, benefiting large parts of today's formal methods.
Topics of interest include:
The work will include close collaboration with several international partners: Xerox PARC, University of Innsbruck, University of Miami, Radboud University Nijmegen, University of Lisbon, and others.
Requirements
You should meet the following requirements:
Research Environment
The research will take place at the recently established Czech
Institute of Informatics, Robotics, and Cybernetics (CIIRC) of the
Czech Technical University (CTU) in Prague, which is with over 1700
members of academic staff one of the largest research institutions in
the Czech Republic. CIIRC has been founded by CTU in July 2013 as a
research and teaching institute and a center of excellence in the
Czech Republic.
CIIRC is the home of the Prague Automated Reasoning Group - an international research group working on various aspects of Automated Reasoning, AI and Machine Learning, Formalization of Mathematics, and related fields. The group has a large and active network of collaborations around the world. The project POSTMAN, led by Mikolas Janota, is funded by the Czech ministry of education within the prestigious ERC CZ scheme.
Prague is the capital of the Czech Republic, considered one of the most beautiful cities in the world and attracting millions of tourists every year. It has the highest Quality of Living Worldwide ranking among the eastern European cities and over 160,000 foreign residents. It boasts a rich history and culture, long tradition of university education and scientific research, and a dynamic economy. The cost of living in Prague is about one half of the living costs in Amsterdam, Paris or Munich.
ApplicationInquiries and applications should be sent via email to Mikolas Janota with "POSTMAN PhD" in the subject. When sending an application please include your CV together with a brief description of your research accomplishments and interests, including the names of two references.
Deadlines: Until the positions are filled. Earlier applications are welcome and early start date is an advantage.
You may be interested to know that there are open full-time proof engineering positions at Siemens Mobility in Chatillon, close to Paris.
They are looking for people more or less experienced with formal methods development, from recent graduates to post-doc researchers. Remuneration depends on previous experience. The knowledge of French is however imperative.
Do not hesitate to contact Danko Ilik if interested.
More details: https://jobs.siemens.com/jobs/214774?lang=fr-fr&utm_source=hellowork&utm_medium=jobboard&utm_campaign=hellowork
Do you have a PhD (or will you soon have) in runtime verification, symbolic execution, fuzzing, automated reasoning, interactive theorem proving, or other methods for statically or dynamically reasoning about software systems?
We are looking for two outstanding and ambitious postdoctoral research associates to work on our “SCorCH: Secure Code for Capability Hardware” project. SCorCH is a collaboration between The University of Manchester, The University of Oxford, ARM Ltd, and Amazon Web Services that will leverage new advances in formal analysis tools to find security issues in code running on a new generation of security-aware hardware chips i.e. Capability Hardware. Our website provides an overview of our vision.
The two positions are available at the University of Manchester, UK and are available to start ‘as soon as possible’. These are fixed-term positions for 3 years with a salary from £32,816.
The University of Manchester (UK) is the largest single-site university in the UK, with the biggest student community, ranked 36th in the world, and fifth in the UK in the Shanghai Jiao Tong World Ranking. The research strength of the Department of Computer Science is reflected in consistently strong returns in UK research assessment exercises (5* in RAE 2000, 2nd in Research Power in RAE 2008, 4th in overall GPA in REF 2014 and ranked equal 1st for research environment). In particular, we have a strong Formal Methods group with expertise in model checking, runtime verification, and automated reasoning.
For more information (see Further Particulars at bottom of page) and to apply see here. We welcome informal enquiries to Dr Giles Reger.
Bernhard Aichernig is looking for a University Assistant (postdoc) to join his research group at Graz University of Technology, Austria. They do research in the areas of formal methods, testing and automata learning. The group combines verification, falsification, modelling, and learning.
The postdoc will do fundamental research in the new TU Graz-SAL Dependable Embedded Systems Lab (DES Lab) where they research new methods for zero-bug software and dependable AI. In the DES Lab she/he will collaborate with SAL and a team around six well-known researchers of TU Graz: Marcel Baunach (embedded systems), Roderick Bloem (verification, synthesis), Robert Legenstein (computational neuroscience, machine learning), Stefan Mangard (security), Thomas Pock (optimisation, machine learning), and Berfhard Aichernig.
Needed qualification: completed doctoral studies in computer science, software engineering or a comparable subject.
Wanted qualifications:
Application deadline: 30 Sep 2020.
For further details and information how to apply, see here.
A brief description of the DES Lab can be found on Bernhard Aichernig's homepage.
In case of questions, feel free to contact Bernhard Aichernig via email.
The Theoretical Computer Science Group (Prof. Barbara Koenig) at the University of Duisburg-Essen, Campus Duisburg (Germany) has two open PhD positions paid according to TV-L 13 (full-time).
The first position (no. 604-20) is in the DFG project SpeQt ("Spectra of Behavioural Distances and Quantitative Logics"), which has recently been granted by the German Research Foundation. This is a joint project with Prof. Lutz Schröder at the University of Erlangen-Nürnberg. A project description is attached below.
The second position (no. 605-20) is not associated with a specific project. The PhD thesis topic will be in the area of modelling and verification of concurrent systems.
You can apply for one or both positions. For both positions, candidates at post-doc level can also be considered.
Due to the Covid-19 pandemic universities in Germany are partially closed. However, there is the possibility to meet and work at the university, observing the current Corona regulations. There is of course the possibility to do the job interview virtually.
Requirements
You should have or should be in the process of obtaining an MSc or
equivalent degree (in Computer Science or Mathematics). Prior
knowledge about the topics of the projects is considered an
advantage. Good English speaking and writing skills are demanded, as
well as the willingness to learn German.
For a post-doc position you should have or should be in the process of obtaining a PhD.
The application deadline is 8th October 2020.
Your Application You can obtain further information by adressing your enquiries to Barbara Koenig.
If you are interested in the position, please send your application. Your application should include:
DFG Project SpeQt - Spectra of Behavioural Distances and Quantitative Logics
One of the central topics in the study of concurrent systems are
notions of system equivalence, which define when two given system
states have the same behaviour in a given sense. Classically,
i.e. over relational transition systems, such system semantics range
on a spectrum between branching-time and linear-time equivalences,
with each equivalence reflecting a notion of possible interaction with
systems, and characterized by a dedicated modal logic. In this
setting, equivalences and logics are two-valued, i.e. two states are
either equivalent or inequivalent, and a formula is either satisfied
or not satisfied in a given state. For systems involving quantitative
data, such as probabilities, weights, or more generally values in some
metric space, it has been recognized that quantitative notions of
equivalence, i.e. behavioural distances, and quantitative logics are
more suitable for some purposes, and enable a more fine-grained
analysis. For instance, while two states in Markov chains with small
differences in their transition probabilities are just inequivalent
under two-valued probabilistic bisimilarity, a suitable behavioural
distance will retain the information that the two states are not
exactly equivalent but still quite similar.
As indicated above, behavioural distances by their very nature apply to settings that deviate from the classical relational model; these settings are generally less standardized and vary quite widely. This creates a need for uniform methods that apply to many system types at once. For branching-time behavioural metrics, we have developed such methods in earlier work within the framework of universal coalgebra, which encapsulates system types as functors and systems as coalgebras for the given type functor. The objective of SpeQt is to additionally parametrize these methods over the system semantics, thus providing support for spectra of behavioural distances in coalgebraic generality.
The key tool we foresee for such a parametrization are graded monads, which we have successfully used in earlier work to parametrize two-valued equivalences. Central research goals include game-theoretic and logical characterization and efficient calculation of distances. Our results will enable us to derive such logics, games and algorithms in a principled way for a whole range of different types of transition systems and for the full spectrum between branching-time and linear-time semantics. We plan to test and evaluate the resulting algorithms in case studies centered around conformance testing of hybrid systems and differential privacy.