The 9th International Workshop on Satisfiability Checking and Symbolic Computation was held on 2 July 2024 at LORIA, the Lorraine Research Laboratory in Computer Science and its Applications, in Nancy, France. It was collocated with IJCAR 2024.

Nancy is a university town in the northeast of France. The workshop was held at LORIA, the Lorraine Research Laboratory in Computer Science and its Applications, which hosted IJCAR and its satellite events, like SC2.

The proceedings of the workshop have been published as Volume 3717 through CEUR-WS.org, and include full papers and extended abstracts.

Program

Registration: 8:30
Session 1: 9:00 - 10:30
  • 9:00-10:00 Invited talk by Manuel Kauers: Separating Variables in Polynomial Ideals show abstract
    For a given ideal I ⊆ K[x1,…,xn,y1,…,ym] in a polynomial ring with n+m variables, we want to find all elements that can be written as f-g for some f ∈ K[x1,…,xn] and some g ∈ K[y1,…,ym], i.e., all elements of I that contain no term involving at the same time one of the x1,…,xn and one of the y1,…,ym. We cannot solve this problem in full generality, but we report on some constructive results in this context that were first obtained in collaboration with Buchacher and Pogudin and recently generalized further in collaboration with Buchacher.
  • 10:00-10:30 Symbolic Computation for All the Fun — Chad Brown, Mikolas Janota and Mirek Olsak
    • Coffee Break: 10:30 - 11:00
    Session 2: 11:00 - 12:30
  • 11:00-11:30 Solving Quantified Non-linear Real Arithmetic using Cylindrical Algebraic Coverings — Jasper Nalbach and Gereon Kremer
  • 11:30-12:00 Projective Delineability — Erika Ábrahám, James H. Davenport, Matthew England, Pierre Mathonet, Lucas Michel, Jasper Nalbach and Naïm Zénaïdi
  • 12:00-12:30 Under-Approximation of a Single Algebraic Cell — Valentin Promies, Jasper Nalbach and Erika Abraham
    • Lunch: 12:30 - 14:00
    Session 3: 14:00 - 16:00
  • 14:00-15:00 Invited talk by Lawrence Paulson: Computer Algebra and the Formalisation of New Mathematics show abstract
    Although people have sought to integrate computer algebra with theorem proving since the 1990s, none of today’s proof assistants claim to offer such an integration. However, Isabelle is capable of some basic computer algebra tasks including symbolic differentiation (and hence symbolic integration via the FTC), deductive limit finding and exact arbitrary-precision real arithmetic. These facilities will be presented, along with an application to formalising last year’s celebrated result of an exponentially smaller upper bound for Ramsey numbers.
  • 15:00-15:30 SHA-256 Collision Attack with Programmatic SAT — Nahiyan Alamgir, Saeed Nejati and Curtis Bright
  • 15:30-16:00 A technological approach to teaching inequalities, propositional and predicate logic — Zoltán Kovács and Reinhard Oldenburg
    • Coffee Break: 16:00 - 16:30

    Workshop Scope

    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.

    Keynote Speakers:

  • Manuel Kauers (Johannes Kepler University, Austria)
  • Lawrence Paulson (University of Cambridge, UK)

    • Sponsors

    We thank our sponsors for their support:

    Submissions and Participation

    The workshop series has emerged from an H2020 FETOPEN CSA project "SC-Square", which ran from 2016 to 2018. It has been continued aiming at building bridges bewteen Satisfiability Checking and Symbolic Computation. It is open for submission and participation to everyone interested in the topics, whether or not they were members or associates of the original project.

    The topics of interest include but are not limited to:

    Registration

    Registration to the workshop will be available via IJCAR 2024 web site

    Submission guidelines

    Submission implies a committment that, in case of acceptance, at least one of the authors attends and presents at the workshop. We are now accepting submissions in the following categories:

    Submissions should be in English, formatted in Springer LNCS style and submitted via EasyChair using this link:
    https://easychair.org/conferences/?conf=scsquare2024

    To receive the appropriate level of peer review, please declare your category of your submission by prefixing the title on the EasyChair form with "FP", "EA" or "PO" accordingly. For consistency, all submissions must use the LNCS style. Current llncs latex files are available from "LaTeX2e Proceedings Templates download" at:
    https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines

    Furthermore, we are working to organize post-proceedings in an issue of the Springer journal Mathematics in Computer Science dedicated to the workshop. Authors of all four categories will be eligible for submission of a corresponding journal article. Journal versions of full papers require at least 30% new material compared to the version originally accepted. All journal submissions will be thoroughly peer-reviewed according to the standards of the journal.

    Important Dates

    All deadlines are by the end of the day anywhere on earth. *This year, considering the rather tight schedule between the ISSAC conference authors notification (April 30 extended to May 11) and the workshop (July 2), we will allow an ISSAC fast track for papers, i.e., (1) papers that do not make it to ISSAC on topics related to SC-Square will have the opportunity to be submitted late to SC-Square as full papers; (2) papers that do make it to ISSAC on topics related to SC-Square will have the opportunity to be submitted late to SC-Square as presentation-only papers. Notification for these papers will be May 24.

    Committees

    Workshop Co-chairs

    Program Committee

    Earlier Workshops and Their Published Proceedings

    This is the 8th workshop in the series originally created by the H2020 FETOPEN CSA project "SC-Square".