<div dir="ltr"><span id="gmail-docs-internal-guid-cd9a6c25-7fff-4177-5e1c-5d2ea0d22f78"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="background-color:transparent;color:rgb(0,0,0);font-family:Arial;font-size:11pt;white-space:pre-wrap">[Apologies for multiple postings]</span><br></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><br></span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Call for SyGuS and SemGuS benchmarks and solvers for the Synthesis Standard Demonstration (Deadline July 1st 2022).</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Background</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The scope of synthesis problems in this demonstration fit into the following paradigms:</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">1) Syntax-Guided Synthesis (SyGuS) is a paradigm for specifying problems where the target program is an expression in an SMT theory. The input to SyGuS consists of a background theory, a semantic-correctness specification for the desired program given by a logical</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">formula, and a syntactic set of candidate implementations given by a grammar.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">2) Semantics-Guided Synthesis (SemGuS) is a paradigm for specifying problems where the target program lies in an arbitrary language. The key difference from SyGuS is that the SemGuS format allows one to specify both the syntax and semantics that define the search space.  The syntax is defined by giving a grammar; the semantics of the language is defined using constrained Horn clauses (CHCs).</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">For both paradigms, the computational problem then is to find an implementation</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">from the set of candidate programs that satisfies the specification. </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Aimed at stimulating innovations in SyGuS techniques, SyGuS-Comp, a competition of solvers for SyGuS benchmarks, was held every year from 2014 to 2019. There has been continued interest in both using SyGuS solvers for various synthesis applications and using SyGuS benchmarks for evaluating new solution strategies. In 2020, the SyGuS organization sent a call to the SyGuS community requesting new benchmarks, feedback on proposed new extensions, and suggestions for new features. Additionally, semantics-guided synthesis was introduced recently as a way of specifying user-defined semantics for expressions that do not fit an SMT-LIB background theory. We demo a range of baseline solvers for these domains at FloC 2022.  </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The demonstration will consist of 4 tracks. For each track, the organizers will curate a set of benchmarks and run all available solvers on them.  The tracks are:</span></p><ol style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:decimal;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SyGuS general track:  Benchmarks in SyGuS 2.1 format (</span><a href="https://urldefense.com/v3/__https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI1-TJM-xg$" style="text-decoration-line:none"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf</span></a><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">) whose logic is limited to standard SMT-LIB theories.</span></p></li><li dir="ltr" style="list-style-type:decimal;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Tables track: Benchmarks in SyGuS 2.1 format whose logic includes a recently developed SMT-LIB theory of tables.</span></p></li><li dir="ltr" style="list-style-type:decimal;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Oracles track: Benchmarks in SyGuS 2.1 format that use the oracles feature.</span></p></li><li dir="ltr" style="list-style-type:decimal;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SemGuS track: Benchmarks in the SemGuS format (<a href="https://urldefense.com/v3/__http://semgus.org/__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2KYRNmkQ$">http://semgus.org/</a>).</span></p></li></ol><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Solvers may be judged based on speed and quality of solutions. However, there will be no official scoring or awards. Instead, an emphasis will be put on showcasing available features in solvers and challenging benchmarks in current applications.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We invite the members of the synthesis community to participate in all tracks of this demonstration, either by submitting benchmarks and new solvers.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">New categories for this year’s demonstration</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Synthesis for a Theory of Tables:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Synthesizing table manipulation programs (e.g., SQL, Python Pandas, R tidyverse) can benefit data scientists by automating their data preparation and database querying pipelines. While table manipulation programs are often short, they have large parameter spaces and also operate over tables that are compound values (list of tuples); as a result, synthesizing table manipulation programs provide unique challenges for synthesizer developers. </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">In order to advance our synthesis algorithm development for tables, we start a new track of “Synthesis for a Theory of Tables” for Sygus with the following resources:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">An SMT-LIB compliant theory of tables that standardized signatures of common table operators including table join, filtering, and aggregation (</span><a href="https://urldefense.com/v3/__https://homepage.cs.uiowa.edu/*ajreynol/tableTheory.pdf__;fg!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI12L6AmXA$" style="text-decoration-line:none"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">https://homepage.cs.uiowa.edu/~ajreynol/tableTheory.pdf</span></a><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">).</span></p></li></ul><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We provide a set of programming-by-examples (PBE) benchmarks from the paper “Synthesizing Highly Expressive SQL Queries from Input-Output Examples (PLDI 2017)” over this domain in the standard SyGuS format for evaluation of the synthesizers.</span></p></li></ul><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We envision this as the first step towards developing a full “theory of relational tables” for developing general table program synthesizers.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Oracles:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Formal inductive synthesis, such as the algorithms typically deployed to solve SyGuS problems, typically work by querying an oracle multiple times. Typically a verification oracle, which uses the semantic constraints given in the SyGuS file to generate a verification query to give to an SMT solver. However, problems exist where it’s either not possible/difficult to encode these constraints as static first-order logic constraints in SyGuS-IF, or checking these constraints is difficult for an SMT solver and a custom reasoning engine would be better suited. The new oracles extension, based on work in the paper “Satisfiability and Synthesis Modulo Oracles”, allows a user to provide external oracles alongside a typical SyGuS specification. This enables the user to provide models that refer to external binaries treated as queryable black-boxes, and to use external reasoning engines as part of the verification condition.  </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The concrete syntax for specifying constraints involving oracles has been incorporated in the SyGuS IF 2.1 standard (</span><a href="https://urldefense.com/v3/__https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI1-TJM-xg$" style="text-decoration-line:none"><span style="font-size:11pt;font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf</span></a><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">).  Specifically, this track will involve benchmarks in the SyGuS format where the “oracles” feature (see Section 2.8) is enabled, and where the background theories are part of the SMT-LIB standard.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SemGuS:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The SemGuS problem formulation was first introduced in the paper “Semantics-guided synthesis,” together with a number of solvers that could handle various SemGuS problems. </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">While SyGuS is useful for synthesizing expressions over a fixed theory, SemGuS has the capability of defining a semantics for the programming language to be used in the synthesis problem in a domain-agnostic, logical format. This capability allows SemGuS to support a wider range of synthesis problems—in particular, synthesis problems for which SMT-LIB compliant background theories have not been developed, such as imperative programs, SQL queries, etc.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SemGuS is a new format, and so far only a handful of solvers have been developed for solving SemGuS problems. The SemGuS format and a parser for it are available at </span><a href="https://urldefense.com/v3/__http://semgus.org__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2qYPLz9g$" style="text-decoration-line:none"><span style="font-size:11pt;font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">semgus.org</span></a><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The purpose of this call is two-fold: 1. For developers of synthesis tools to develop new SemGuS solvers. 2. To gather a broader set of SemGuS benchmarks.  </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The original SemGuS paper compiled a set of 496 benchmarks, ranging over standard SyGuS problems, imperative program-synthesis problems, and synthesis problems over regular expressions. Like SyGuS, there is a need to grow the number of SemGuS benchmarks; in particular, as SemGuS promises to be a general format capable of expressing synthesis problems over arbitrary domains, we are looking for a wide variety of benchmarks coming from various domains and scenarios. Any contribution adding to the set of SemGuS benchmarks would be much appreciated. </span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Call for Solvers and Benchmarks (Deadline July 1st 2022)</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">1) Call for solvers:</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><br></span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">This year’s demonstration will run on the existing benchmarks and on the ones collected through this call. The demonstration will welcome solvers that can solve benchmarks in any of the categories mentioned in this call. Those interested in submitting a new solver can contact the organizers at the following email addresses:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SyGuS: </span><a href="mailto:sygus-organizers@seas.upenn.edu" style="text-decoration-line:none"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">sygus-organizers@seas.upenn.edu</span></a><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. </span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SemGuS: </span><a href="mailto:semgus@office365.wisc.edu" style="text-decoration-line:none"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">semgus@office365.wisc.edu</span></a></p></li></ul><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">2) Call for benchmarks: </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><br></span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Benchmarks can be submitted through the following ways for each category:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SyGuS: pull requests at <a href="https://urldefense.com/v3/__https://github.com/SyGuS-Org/benchmarks__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2BwyDF-w$">https://github.com/SyGuS-Org/benchmarks</a></span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">SemGuS: pull requests at </span><a href="https://urldefense.com/v3/__https://github.com/SemGuS-git/Semgus-Benchmarks/__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2QTDzeUQ$" style="text-decoration-line:none"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">https://github.com/SemGuS-git/Semgus-Benchmarks/</span></a><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p></li></ul><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">All solvers will be presented and advertised through a talk describing the results of this demonstration at SYNT, a workshop co-located with CAV22.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Organization</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The SyGuS infrastructure and competition was initiated as part of NSF Expeditions in Computing project ExCAPE, and is currently organized by Saswat Padhi (Amazon) and Andrew Reynolds (University of Iowa). For more information see the sygus webpage <a href="https://urldefense.com/v3/__https://sygus.org/__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI1_OdsXuQ$">https://sygus.org/</a> . For questions please contact the organizers at </span><a href="mailto:sygus-organizers@seas.upenn.edu" style="text-decoration-line:none"><span style="font-size:11pt;font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">sygus-organizers@seas.upenn.edu</span></a><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. The SemGuS framework and its infrastructure were initiated by Jinwoo Kim, Loris D’Antoni, and Tom Reps at the University of Wisconsin. The SemGuS specification language was designed with the help of Andrew Reynolds. For questions please contact </span><a href="mailto:semgus@office365.wisc.edu" style="text-decoration-line:none"><span style="font-size:11pt;font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">semgus@office365.wisc.edu</span></a><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p><br></span></div>