Satisfiability Modulo Theory (SMT) solvers are a useful tool that can be applied to a variety of problems, such as configuring relationships in distributed systems, detecting race conditions, and program analysis. String constraints are particularly difficult for SMT solvers to navigate, as the search space is generally large. Often times, classical SMT solvers will have to quit generating a solution for string constraints because it takes too long to find the solution. Quantum computing offers the advantages of quantum mechanics (e.g., superposition), which allows a system to explore a large search space much more efficiently. In this work, we explore creating a quantum-enabled SMT solver for string theory by using quantum annealing and Quadratic Unconstrained Binary Optimization (QUBO). Our preliminary results demonstrate that it is feasible to transform these string constraints to QUBO, and generate solutions for given constraints.

In recent years, the use of automated source code generation utilizing transformer-based generative models has grown in popularity. These models can generate code according to the developers' requirements. However, recent research showed that these automatically generated source codes can contain vulnerabilities and other quality issues. Despite researchers' and practitioners' attempts to enhance code generation models, retraining and fine-tuning large language models is not only time-consuming but also resource-intensive and costly. Thus, in this paper, we describe FRANC, a lightweight framework for recommending more secure and high-quality source code derived from transformer-based code generation models. FRANC includes a static filter to make the generated code compilable with heuristics and a quality-aware ranker to sort the code snippets based on a quality score. Moreover, the framework uses prompt engineering to fix persistent quality issues. We evaluated FRANC with five Python and Java code generation models and six prompt datasets, including a newly created one in this work (FRANC). The static filter improves 9% to 46% Java suggestions and 10% to 43% Python suggestions regarding compilability. The average improvement over the NDCG@10 score for the ranking system is 0.0763, and the repairing techniques repair the highest 80% of prompts. FRANC takes, on average, 1.98 seconds for Java; for Python, it takes 0.08 seconds.