June 2021 - Termtools - lists.rwth-aachen.de

Termination and Complexity Competition 2021: Call for Participation (Deadline June 30)
by Juergen Giesl 02 Jul '21

02 Jul '21

*Termination and Complexity Competition 2021* http://www.termination-portal.org/wiki/Termination_Competition_2021 *Call for Participation* Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated to CADE 2021 (http://www.cade-28.info/). The competition will be run on the StarExec platform ( https://www.starexec.org/) shortly before CADE. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: http://www.termination-portal.org/wiki/Termination_Competition_2021 *Important dates* - Tool and Problem Submission: June 30, 2021 - First Run: July 1, 2021 - Bug/Conflict Report Deadline: July 5, 2021 - Bugfix Deadline: July 10, 2021 - Final Run: July 13, 2021 - Presentation of Results: July 15, 2021

6 14

Last Call for Participation: 12th International School on Rewriting (ISR 2021), online and free
by Carsten Fuhs 30 Jun '21

30 Jun '21

================== LAST CALL FOR PARTICIPATION ================== 12th International School on Rewriting (ISR 2021) 5-16 July 2021 Virtual event hosted via ZOOM by Universidad Complutense de Madrid https://dalila.sip.ucm.es/isr2021/ Registration (FREE but required) is open at: https://eventos.ucm.es/66824/detail/12th-international-school-on-rewriting-… ================== Rewriting is a powerful model of computation that underlies much of declarative programming and is ubiquitous in mathematics, logic, theorem proving, verification, model-checking, compilation, biology, chemistry, physics, etc. In 2021, the 12th International School on Rewriting (ISR 2021) will take place online as a virtual event hosted via ZOOM by the Computer Science School at Universidad Complutense de Madrid, Spain. The school is aimed at Master and PhD students, researchers and practitioners interested in the use or the study of rewriting and its applications. >From July 5 to July 16 a course will be taught every day, according to the schedule published in the web page. ================== COURSES ================== Christiano Braga: Compiler construction in Maude Paola Bruscoli: An introduction to deep inference methodology in proof theory Santiago Escobar: Unification and Narrowing in Maude 3.0 Maribel Fernandez: Nominal rewriting Carsten Fuhs: Automated complexity analysis for term rewriting Maja H. Kirkeby & Robert Glück: Inversion and term rewriting systems Jean-Jacques Levy: Lambda calculus, the generalized finite development theorem Luigi Liquori & Vincent van Oostrom: Lambda calculi with patterns Dorel Lucanu, Xiaohong Chen & Grigore Rosu: From rewriting to matching logic Jorge A. Perez: Session types for message-passing concurrency Carolyn Talcott: Pathway Logic, using rewriting logic to understand how cells work ================== REGISTRATION ================== Registration is FREE but required. https://eventos.ucm.es/66824/detail/12th-international-school-on-rewriting-… ================== ORGANIZERS ================== David de Frutos Escrig Narciso Marti-Oliet Albert Rubio Manuel Montenegro Adrian Riesco Contact: narciso(a)ucm.es ISR 2021 is promoted by the IFIP WG1.6 and supported by Universidad Complutense de Madrid. ==================

1 0

crashes on StarExec that cannot be reproduced elsewhere
by Florian Frohn 23 Jun '21

23 Jun '21

Dear all, I'm struggling with StarExec and running out of ideas, so if anybody experienced similar issues, please let me know: On StarExec, my tool LoAT reliably crashes on some problems with error messages like: /export/starexec/sandbox/solver /bin/starexec_run_loat_nonterm_debug: line 4: 62638 Illegal instruction (core dumped) ./loat-static --plain --timeout $TO --nonterm $1 The crash happens after a few milliseconds. The same binary works perfectly fine on my PC and in the VM (https://www.starexec.org/vmimage/). My tool is written in C++. I build the binary and its dependencies (Z3, Yices, ginac, ntl, purrs) with gcc in a voidlinux docker container. It's statically linked with musl (http://musl.libc.org/). I tried to compile it in the VM instead, but one more dependency (giac) is missing in the CentOS repositories. Since building giac from scratch seems rather complex, I gave up at that point. I disabled optimizations as far as possible (by compiling LoAT as well as its dependencies with -O0), but that didn't change anything. Running the same binary with valgrind or the clang/gcc sanitizer for undefined behavior does not reveal any problems either. If you have any ideas what else to try or how to debug such issues on StarExec, please let me know! Thanks, Florian

2 2

crashes on StarExec that cannot be reproduced elsewhere
by Florian Frohn 19 Jun '21

19 Jun '21

Dear all, I'm struggling with StarExec and running out of ideas, so if anybody experienced similar issues, please let me know: On StarExec, my tool LoAT reliably crashes on some problems with error messages like: /export/starexec/sandbox/solver/bin/starexec_run_loat_nonterm_debug: line 4: 62638 Illegal instruction (core dumped) ./loat-static --plain --timeout $TO --nonterm $1 The crash happens after a few milliseconds. The same binary works perfectly fine on my PC and in the VM (https://www.starexec.org/vmimage/). My tool is written in C++. I build the binary and its dependencies (Z3, Yices, ginac, ntl, purrs) with gcc in a voidlinux docker container. It's statically linked with musl (http://musl.libc.org/). I tried to compile it in the VM instead, but one more dependency (giac) is missing in the CentOS repositories. Since building giac from scratch seems rather complex, I gave up at that point. I disabled optimizations as far as possible (by compiling LoAT as well as its dependencies with -O0), but that didn't change anything. Running the same binary with valgrind or the clang/gcc sanitizer for undefined behavior does not reveal any problems either. If you have any ideas what else to try or how to debug such issues on StarExec, please let me know! Thanks, Florian

1 0

Termination and Complexity Competition 2021: Second Call for Participation (Deadline June 30)
by Juergen Giesl 16 Jun '21

16 Jun '21

*Termination and Complexity Competition 2021* http://www.termination-portal.org/wiki/Termination_Competition_2021 *Call for Participation* Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated to CADE 2021 (http://www.cade-28.info/). The competition will be run on the StarExec platform ( https://www.starexec.org/) shortly before CADE. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: http://www.termination-portal.org/wiki/Termination_Competition_2021 *Important dates* - Tool and Problem Submission: June 30, 2021 - First Run: July 1, 2021 - Bug/Conflict Report Deadline: July 5, 2021 - Bugfix Deadline: July 10, 2021 - Final Run: July 13, 2021 - Presentation of Results: July 15, 2021

1 0

Certified Programs and Proofs (CPP) 2022: Call for Papers
by Thiemann, René 16 Jun '21

16 Jun '21

Dear all, I’m forwarding this CFP on behalf of the organisers. In particular, they mention certified termination proving in their topics of interest. With best regards, René Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education. CPP 2022 (https://popl22.sigplan.org/home/CPP-2022) will be held on 16-18 January 2022 and will be co-located with POPL 2022 in Philadelphia, Pennsylvania, United States. CPP 2022 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2022 will welcome contributions from all members of the community. The CPP 2022 organizers will strive to enable both in-person and remote participation, in cooperation with the POPL 2022 organizers. IMPORTANT DATES * Abstract Submission Deadline: 16 September 2021 at 23:59 AoE (UTC-12h) * Paper Submission Deadline: 22 September 2021 at 23:59 AoE (UTC-12h) * Notification (tentative): 22 November 2021 * Camera Ready Deadline (tentative): 12 December 2021 * Conference: 16-18 January 2022 Deadlines expire at the end of the day, anywhere on earth. Abstract and submission deadlines are strict and there will be no extensions. DISTINGUISHED PAPER AWARDS Around 10% of the accepted papers at CPP 2022 will be designated as Distinguished Papers. This award highlights papers that the CPP program committee thinks should be read by a broad audience due to their relevance, originality, significance and clarity. TOPICS OF INTEREST We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP: * certified or certifying programming, compilation, linking, OS kernels, runtime systems, security monitors, and hardware; * certified mathematical libraries and mathematical theorems; * proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc); * new languages and tools for certified programming; * program analysis, program verification, and program synthesis; * program logics, type systems, and semantics for certified code; * logics for certifying concurrent and distributed systems; * mechanized metatheory, formalized programming language semantics, and logical frameworks; * higher-order logics, dependent type theory, proof theory, logical systems, separation logics, and logics for security; * verification of correctness and security properties; * formally verified blockchains and smart contracts; * certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; * certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; * certificates for program termination; * formal models of computation; * mechanized (un)decidability and computational complexity proofs; * formally certified methods for induction and coinduction; * integration of interactive and automated provers; * logical foundations of proof assistants; * applications of AI and machine learning to formal certification; * user interfaces for proof assistants and theorem provers; * teaching mathematics and computer science with proof assistants. SUBMISSION GUIDELINES Prior to the paper submission deadline, the authors should upload their anonymized paper in PDF format through the HotCRP system at https://cpp2022.hotcrp.com The submissions must be written in English and provide sufficient detail to allow the program committee to assess the merits of the contribution. They must be formatted following the ACM SIGPLAN Proceedings format using the acmart style with the sigplan option, which provides a two-column style, using 10 point font for the main text, and a header for double blind review submission, i.e., \documentclass[sigplan,10pt,anonymous,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false} The submitted papers should not exceed 12 pages, including tables and figures, but excluding bibliography and clearly marked appendices. The papers should be self-contained without the appendices. Shorter papers are welcome and will be given equal consideration. Submissions not conforming to the requirements concerning format and maximum length may be rejected without further consideration. CPP 2022 will employ a lightweight double-blind reviewing process. To facilitate this, the submissions must adhere to two rules: (1) author names and institutions must be omitted, and (2) references to authors’ own related work should be in the third person (e.g., not "We build on our previous work ..." but rather "We build on the work of ..."). The purpose of this process is to help the PC and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing it more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors are free to disseminate their ideas or draft versions of their papers as usual. For example, authors may post drafts of their papers on the web or give talks on their research ideas. POPL has answers to frequently asked questions addressing many common concerns: https://popl20.sigplan.org/track/POPL-2020-Research-Papers#Submission-and-R… We strongly encourage the authors to provide any supplementary material that supports the claims made in the paper, such as proof scripts or experimental data. This material must be uploaded at submission time, as an archive, not via a URL. Two forms of supplementary material may be submitted: (1) Anonymous supplementary material is made available to the reviewers before they submit their first-draft reviews. (2) Non-anonymous supplementary material is made available to the reviewers after they have submitted their first-draft reviews and have learned the identity of the authors. Please use anonymous supplementary material whenever possible, so that it can be taken into account from the beginning of the reviewing process. The submitted papers must adhere to the SIGPLAN Republication Policy (https://www.sigplan.org/Resources/Policies/Republication/) and the ACM Policy on Plagiarism (https://www.acm.org/publications/policies/plagiarism). Concurrent submissions to other conferences, journals, workshops with proceedings, or similar forums of publication are not allowed. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. One author of each accepted paper is expected to present it at the (possibly virtual) conference. PUBLICATION, COPYRIGHT AND OPEN ACCESS The CPP 2022 proceedings will be published by the ACM, and authors of accepted papers will be required to choose one of the following publication options: (1) Author retains copyright of the work and grants ACM a non-exclusive permission-to-publish license and, optionally, licenses the work under a Creative Commons license. (2) Author retains copyright of the work and grants ACM an exclusive permission-to-publish license. (3) Author transfers copyright of the work to ACM. For authors who can afford it, we recommend option (1), which will make the paper Gold Open Access, and also encourage such authors to license their work under the CC-BY license. ACM will charge you an article processing fee for this option (currently, US$700), which you have to pay directly with the ACM. For everyone else, we recommend option (2), which is free and allows you to achieve Green Open Access, by uploading a preprint of your paper to a repository that guarantees permanent archival such as arXiv or HAL. This is anyway a good idea for timely dissemination even if you chose option 1. Ensuring timely dissemination is particularly important for this edition, since, because of the very tight schedule, the official proceedings might not be available in time for CPP. The official CPP 2022 proceedings will also be available via SIGPLAN OpenTOC (http://www.sigplan.org/OpenTOC/#cpp). For ACM’s take on this, see their Copyright Policy (http://www.acm.org/publications/policies/copyright-policy) and Author Rights (http://authors.acm.org/main.html). PROGRAM COMMITTEE Andrei Popescu, University of Sheffield, United Kingdom (co-chair) Steve Zdancewic, University of Pennsylvania, United States (co-chair) Mohammad Abdulaziz, TU München, Germany Mauricio Ayala-Rincón, Universidade de Brasília, Brazil Andrej Bauer, University of Ljubljana, Slovenia Thomas Bauereiss, University of Cambridge, United Kingdom Yves Bertot, Inria and Université Cote d'Azur, France Lars Birkedal, Aarhus University, Denmark Sylvie Boldo, Inria and Université Paris-Saclay, France Qinxiang Cao, Shanghai Jiao Tong University, China Évelyne Contejean, Laboratoire Méthodes Formelles, CNRS, France Benjamin Delaware, Purdue University, United States Simon Foster, University of York, United Kingdom Alwyn Goodloe, NASA Langley Research Center, United States Armaël Guéneau, Aarhus University, Denmark John Harrison, Amazon Web Services, United States Joe Hendrix, Galois, Inc, United States Aquinas Hobor, National University of Singapore, Singapore Ralf Jung, MPI-SWS, Germany Cezary Kaliszyk, University of Innsbruck, Austria Jeehoon Kang, KAIST, South Korea Hongjin Liang, Nanjing University, China Gregory Malecha, BedRock Systems, Inc, United States Anders Mörtberg, Stockholm University, Sweden Toby Murray, University of Melbourne, Australia Zoe Paraskevopoulou , Northeastern University, United States Brigitte Pientka, McGill University, Canada Aseem Rastogi, Microsoft Research, India Bas Spitters, Aarhus University, Denmark Kathrin Stark, Princeton University, United States Hira Taqdees Syeda, Chalmers University of Technology, Sweden Joseph Tassarotti, Boston College, United States Laura Titolo, NIA/NASA LaRC, United States Sophie Tourret, Inria, France Dmitriy Traytel, University of Copenhagen, Denmark Floris van Doorn, Paris-Saclay University, France Freek Verbeek, Open University of The Netherlands, Netherlands Freek Wiedijk, Radboud Universiteit Nijmegen, Netherlands ORGANIZERS Lennart Beringer, Princeton University, United States (conference co-chair) Robbert Krebbers, Radboud University, Netherlands (conference co-chair) Andrei Popescu, University of Sheffield, United Kingdom (PC co-chair) Steve Zdancewic, University of Pennsylvania, United States (PC co-chair) CONTACT For any questions please contact the two PC chairs: Andrei Popescu <a.popescu(a)sheffield.ac.uk> Steve Zdancewic <stevez(a)seas.upenn.edu>

1 0

FSCD 2021: Call for (Online) Participation
by Carsten Fuhs 14 Jun '21

14 Jun '21

CALL FOR PARTICIPATION Sixth International Conference on Formal Structures for Computation and Deduction (FSCD 2021) July 17 – July 24, 2021, Buenos Aires, Argentina https://fscd2021.github.io/ In-cooperation with ACM SIGLOG and SIGPLAN The 2021 edition of FSCD and of its satellite workshops will be held online. Participation will, a priori, be free of charge, unless we receive way too many requests, in which case we will invite those who can to pay the modest amount of 7 USD. FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation (e.g., quantum computing, probabilistic computing, homotopy type theory), semantics and verification in new challenging areas (e.g., blockchain protocols or deep learning algorithms). REGISTRATION --------------- The registration page is already open and linked from: https://fscd2021.dc.uba.ar/registration.html This link should be used also to register for affiliated workshops. Registration is open until July 11. FSCD 2021 will run over the Clowdr platform. After the registration is closed, you will receive an invitation link and instructions on how to participate. INVITED SPEAKERS ---------------- - Zena M. Ariola https://ix.cs.uoregon.edu/~ariola/ - Nao Hirokawa https://www.jaist.ac.jp/~hirokawa/ - Elaine Pimentel https://sites.google.com/site/elainepimentel/ - Sam Staton https://www.cs.ox.ac.uk/people/samuel.staton/main.html FSCD AFFILIATED WORKSHOPS: -------------------------- - HoTT/UF (6th Workshop on Homotopy Type Theory/Univalent Foundations, July 17-18) - ITRS (10th Workshop on Intersection Types and Related Systems, July 17) - WPTE (7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, July 18) - UNIF (35th International Workshop on Unification, July 18) - LSFA (16th Logical and Semantics Frameworks with Applications, July 23-24) - IWC (10th International Workshop on Confluence, July 23) - IFIP WG 1.6 (24th meeting of the IFIP Working Group 1.6: Rewriting, July 24) PROGRAM COMMITTEE CHAIR ----------------------- Naoki Kobayashi, The University of Tokyo fscd2021(a)easychair.org PROGRAM COMMITTEE ----------------- Mauricio Ayala-Rincón, Universidade de Brasília Stefano Berardi, University of Torino Frédéric Blanqui, INRIA Eduardo Bonelli, Stevens Institute of Technology Évelyne Contejean, CNRS, Université Paris-Saclay Thierry Coquand, University of Gothenburg Thomas Ehrhard, Université de Paris, CNRS Santiago Escobar, Univ. Politècnica de València José Espírito Santo, University of Minho Claudia Faggian, Université de Paris, CNRS Amy Felty, University of Ottawa Santiago Figueira, Universidad de Buenos Aires Marcelo Fiore, University of Cambridge Marco Gaboardi, Boston University Silvia Ghilezan, University of Novi Sad Ichiro Hasuo, National Institute of Informatics Delia Kesner, Université de Paris Robbert Krebbers, Radboud University Nijmegen Temur Kutsia, Johannes Kepler University Linz Barbara König, University of Duisburg-Essen Marina Lenisa, University of Udine Naoki Nishida, Nagoya University Luke Ong, University of Oxford Paweł Parys, University of Warsaw Jakob Rehof, TU Dortmund University Camilo Rocha, Pontificia Univ. Javeriana Cali Alexandra Silva, University College London Alwen Tiu, Australian National University Sarah Winkler, University of Verona Hongseok Yang, KAIST, South Korea CONFERENCE CHAIR ---------------- Alejandro Díaz-Caro, Quilmes Univ. & ICC/CONICET ORGANIZING COMMITTEE -------------------- Mauricio Ayala-Rincón (Workshops co-chair), Universidade de Brasília Santiago Figueira, Universidad de Buenos Aires & ICC Malena Ivnisky (Virtualization co-chair), Universidad de Buenos Aires & ICC Mauro Jaskelioff, Universidad Nacional de Rosario & CIFASIS Carlos López Pombo (Workshops co-chair), Universidad de Buenos Aires & ICC Ricardo Rodríguez (Virtualization co-chair), Universidad de Buenos Aires & ICC Rafael Romero (Virtualization co-chair), Universidad de Buenos Aires & ICC Nora Szasz, Universidad ORT Uruguay Beta Ziliani, Universidad Nacional de Córdoba FSCD STEERING COMMITTEE ----------------------- Zena M. Ariola, University of Oregon Mauricio Ayala-Rincón, University of Brasilia Carsten Fuhs (Publicity Chair), Birkbeck, University of London Herman Geuvers, Radboud University Silvia Ghilezan, University of Novi Sad Stefano Guerrini, University of Paris 13 Delia Kesner (SC Chair), University of Paris Diderot Hélène Kirchner, Inria Cynthia Kop, Radboud University Damiano Mazza, University of Paris 13 Luke Ong, Oxford University Jakob Rehof, TU Dortmund Jamie Vicary (SC Workshop Chair), Oxford University

1 0