SYNT 2024

Domain-specific languages (DSLs) have become integral to various software workflows. Such languages offer domain-specific optimizations and abstractions that improve code readability and maintainability. However, leveraging these languages requires developers to rewrite existing code using the specific DSL's API. While large language models (LLMs) have shown some success in automatic code transpilation, none of them provide any functional correctness guarantees on the rewritten code. Another approach for automating this task is verified lifting, which relies on program synthesis to find programs in the target language that are functionally equivalent to the source language program. While several verified lifting tools have been developed for various application domains, they are specialized for specific source-target languages or require significant expertise in domain knowledge to make the search efficient. In this paper, leveraging recent advances in LLMs, we propose an LLM-based approach to building verified lifting tools. We use the LLM's capabilities to reason about programs to translate a given program into its corresponding equivalent in the target language. Additionally, we use LLMs to generate proofs for functional equivalence. We develop lifting-based compilers for three DSLs targeting different application domains. Our approach outperforms previous symbolic-based tools in the number of benchmarks transpiled and also requires significantly less efforts to build.

Recently, the realizability problem of LTL Modulo Theories ($\LTLt$) specifications has been shown to be decidable whenever theories are decidable. However, such approaches suffer from a key limitation: memory of specifications is restricted. They allow to carry finite information of infinite theories. For instance, we can remember that "x" was odd in previous timesteps, but we cannot remember the concrete value of "x" in previous timesteps. This limits the ability of abstractions to properly encode richer dynamics in the specifications (e.g., it is currently not possible to specify that a variable increases monotonically over time). In this paper, we extend $\LTLt$ with operators that allow to fetch values of the variables in previous instants ($\LTLtf$). We show that realizability in $\LTLtf$ is undecidable in general, but we also propose a sound incomplete algorithm that works for expressive $\LTLtf$ formulae in which we can specify realistic environment dynamics. In addition, we present a novel procedure that abstracts tautologies in $\LTLtf$ to tautologies in $\LTLt$, which conveys memory across-time and thus helps pushing conclusiveness of our algorithm. Moreover, we show that we can encode inductive behaviour such as counters and averages. To the best of our knowledge, this is the first work that presents sound realizability algorithms that conclude in such expressive specifications.

Many state-of-the-art techniques are designed to automatically infer upper limits on the number of iterations a loop may execute, conventionally called bounds. Analysis of this kind is inspired by techniques to prove termination used in previous works, namely to instrument the program with a decrementing counter and find the conditions by which the counter’s value is above zero at the end of the program. However, in most cases, they do not capture the exact number of iterations which could be useful to estimate the number of cycles/iterations/time a process requires when it is distributed across many devices, relational verification and equivalence checking, and even non-termination. In this extended abstract, we present the ongoing work on synthesis of an exact loop bound for single-loop programs as a function over the program’s inputs.

Motivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that the Cross operation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.

Asynchronous and concurrent programming are fundamental concepts for building responsive and efficient software systems. To this end, we proposed an approach for refactoring a sequential program into an asynchronous program that uses async/await, called asynchronization, without introducing data races [1]. We showed that the delay complexity of enumerating all data race free asynchronizations, which quantifies the delay between outputting two consecutive data race free asynchronizations, is polynomial time modulo an oracle for solving reachability in sequential programs. In this paper, we show that this approach and the associated results extend to refactoring a sequential program into a data race free multi-threaded program that uses start/join.

This is the presentation of the SYNTCOMP results.