Memory-safety bugs are a major source of vulnerabilities in C code. Much work has focused on spatial memory safety (e.g., buffer overflows), while temporal memory safety (e.g., use-after-free) has received less attention. One solution for achieving temporal memory safety is to apply an ownership model to an existing program and enforce it. In this paper, we describe the design and implementation of a new temporal memory safety model for C source code. Our design improves on CERT's Pointer Ownership Model with enhancements including use of a SAT solver to enforce constraint satisfaction, LLMs to complete a per-program model, and an improved mechanism to prevent use-after-free errors inspired by Rust's borrow checker and object lifetimes. Our implementation performed well on a large test suite of memory-safe and memory-unsafe code examples. We tested all 4,604 C code examples for the 5 CWEs associated with temporal memory safety (CWEs 401, 415, 416, 590, 761) from the Juliet C/C++ test suite. In our tests, all of the memory-unsafe examples were correctly recognized as unsafe, and 81% of the 2,302 memory-safe examples were correctly recognized as memory-safe.

The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form. Cardinality constraints are prevalent in numerous problems, prompting the development and study of various types of encoding. We present a novel approach to optimizing cardinality constraint encodings by exploring the impact of literal orderings within the constraints. By strategically placing related literals nearby each other, the encoding generates auxiliary variables in a hierarchical structure, enabling the solver to reason more abstractly about groups of related literals. Unlike conventional metrics such as formula size or propagation strength, our method leverages structural properties of the formula to redefine the roles of auxiliary variables to enhance the solver's learning capabilities. The experimental evaluation on benchmarks from the maximum satisfiability competition demonstrates that literal orderings can be more influential than the choice of the encoding type. Our literal ordering technique improves solver performance across various encoding techniques, underscoring the robustness of our approach.

Autonomous cyber-physical systems liker obots and self-driving cars could greatly benefit from using formal methods toreason reliably about their control decisions.However, beforea problem can be solved it needs to be stated.This requires writing af ormal physics model of the cyber-physical system, which is a complex task that traditionally requires human expertise and becomes ab ottleneck.This paper experimentally studies whetherL arge Language Models (LLMs) can automate the formalization process.A2 0 problem benchmark suite is designed drawing from undergraduate levelp hysics kinematics problems.In each problem, the LLM is provided with an atural language description of the objects' motion and must produce am odel in differentialg ame logic (dGL).The model is (1) syntax checked and iteratively refined based on parser feedback, and( 2) semantically evaluated by checking whether symbolically executing the dGL formula recovers the solution to the original physics problem.As uccess rate of 70% (best over 5s amples) is achieved.We analyze failing cases, identifying directions forf uturei mprovement.This provides afi rst quantitative baseline forL LM-based autoformalization from natural language to ah ybrid games logic with continuous dynamics.

The problem of software quality has motivated the development of a variety of techniques for Automatic Program Repair (APR). Meanwhile, recent advances in AI and Large Language Models (LLMs) have produced orders of magnitude performance improvements over previous code generation techniques, affording promising opportunities for program repair and its constituent subproblems (e.g., fault localization, patch generation). Because models are trained on large volumes of code in which defects are relatively rare, they tend to both simultaneously perceive faulty code as unlikely (or “unnatural”) and to produce generally correct code (which is more “natural”). This paper comprehensively revisits the idea of (un)naturalness for program repair. We argue that, fundamentally, LLMs can only go so far on their own in reasoning about and fixing buggy code. This motivates the incorporation of traditional tools, which compress useful contextual and analysis information, as a complement to LLMs for repair. We interrogate the role of entropy at every stage of traditional repair, and show that it is indeed usefully complementary to classic techniques. We show that combining measures of naturalness with class Spectrum-Based Fault Localization (SBFL) approaches improves Top-5 scoring by 50 % over SBFL alone. We show that entropy delta, or change in entropy induced by a candidate patch, can improve patch generation efficiency by 24 test suite executions per repair, on average, on our dataset. Finally, we show compelling results that entropy delta for patch classification is highly effective at distinguishing correct from overfitting patches. Overall, our results suggest that LLMs can effectively complement classic techniques for analysis and transformation, producing more efficient and effective automated repair techniques overall.

Logic programs are a powerful approach for solving NP-Hard problems. However, their declarative nature poses significant challenges in debugging. Unlike procedural paradigms, which allow for step-by-step inspection of program state, logic programs require reasoning about logical statements for fault localization. This complexity is especially significant in learning environments due to students' inexperience. We introduce FormHe, a novel tool that integrates logic-based techniques with Large Language Models (LLMs) to detect and correct issues in Answer Set Programming submissions. FormHe consists of two main components: a fault localization module and a program repair module. First, the fault localization module identifies specific faulty statements in need of modification. Next, FormHe applies program mutation techniques and leverages LLMs to repair the flawed code. The resulting repairs are then used to generate hints that guide students in correcting their programs. Our experiments with real buggy programs submitted by students show that FormHe accurately detects faults in 94% of cases and successfully repairs 58% of incorrect submissions.

Abstract In recent years, more people have seen their work depend on data manipulation tasks. However, many of these users do not have the background in programming required to write complex programs, particularly SQL queries. One way of helping these users is automatically synthesizing the SQL query given a small set of examples. Several program synthesizers for SQL have been recently proposed, but they do not leverage multicore architectures. This paper proposes Cubes, a parallel program synthesizer for the domain of SQL queries using input-output examples. Since input-output examples are an under-specification of the desired SQL query, sometimes, the synthesized query does not match the user’s intent. Cubes incorporates a new disambiguation procedure based on fuzzing techniques that interacts with the user and increases the confidence that the returned query matches the user intent. We perform an extensive evaluation on around 4000 SQL queries from different domains. Experimental results show that our parallel approach can scale up to 16 processes with super-linear speedups for many hard instances, and that our disambiguation approach is critical to achieving an accuracy of around 60%, significantly larger than other SQL synthesizers.

Fault Localization (FL) aims to automatically localize buggy lines of code, a key first step in many manual and automatic debugging tasks. Previous FL techniques assume the provision of input tests, and often require extensive program analysis, program instrumentation, or data preprocessing. Prior work on deep learning for APR struggles to learn from small datasets and produces limited results on real-world programs. Inspired by the ability of large language models (LLMs) of code to adapt to new tasks based on very few examples, we investigate the applicability of LLMs to line level fault localization. Specifically, we propose to overcome the left-to-right nature of LLMs by fine-tuning a small set of bidirectional adapter layers on top of the representations learned by LLMs to produce LLMAO, the first language model based fault localization approach that locates buggy lines of code without any test coverage information. We fine-tune LLMs with 350 million, 6 billion, and 16 billion parameters on small, manually curated corpora of buggy programs such as the Defects4J corpus. We observe that our technique achieves substantially more confidence in fault localization when built on the larger models, with bug localization performance scaling consistently with the LLM size. Our empirical evaluation shows that LLMAO improves the Top-1 results over the state-of-the-art machine learning fault localization (MLFL) baselines by 2.3%--54.4%, and Top-5 results by 14.4%-35.6%. LLMAO is also the first FL technique trained using a language model architecture that can detect security vulnerabilities down to the code line level.

Stateful firewalls (SFW) play a critical role in securing our network infrastructure. Incorrect implementation of the intended stateful semantics can lead to evasion opportunities, even if firewall rules are configured correctly. Uncovering these opportunities is challenging due to the (1) black-box and proprietary nature of firewalls; (2) diversity of deployments; and (3) complex stateful semantics. To tackle these challenges, we present Pryde. Pryde uses a modular model-guided workflow that generalizes across black-box firewall implementations and deployment-specific settings to generate evasion attacks. Pryde infers a behavioral model of the stateful firewall in the presence of potentially non-TCP-compliant packet sequences. It uses this model in conjunction with attacker capabilities and victim behavior to synthesize custom evasion attacks. Using Pryde, we identify more than 6,000 unique attacks against 4 popular firewalls and 4 host networking stacks, many of which cannot be uncovered by prior work on censorship circumvention and black-box fuzzing.

Rust type system constrains pointer operations, preventing bugs such as use-after-free. However, these constraints may be too strict for programming tasks such as implementing cyclic data structures. For such tasks, programmers can temporarily suspend checks using the unsafe keyword. Rust libraries wrap unsafe code blocks and expose higher-level APIs. They need to be extensively tested to uncover memory-safety bugs that can only be triggered by unexpected API call sequences or inputs. While prior works have attempted to automatically test Rust library APIs, they fail to test APIs with common Rust features, such as polymorphism, traits, and higher-order functions, or they have scalability issues and can only generate tests for a small number of combined APIs. We propose Crabtree, a testing tool for Rust library APIs that can automatically synthesize test cases with native support for Rust traits and higher-order functions. Our tool improves upon the test synthesis algorithms of prior works by combining synthesis and fuzzing through a coverage- and type-guided search algorithm that intelligently grows test programs and input corpus towards testing more code. To the best of our knowledge, our tool is the first to generate well-typed tests for libraries that make use of higher-order trait functions. Evaluation of Crabtree on 30 libraries found four previously unreported memory-safety bugs, all of which were accepted by the respective authors.

To keep up with changes in requirements, frameworks, and coding practices, software organizations might need to migrate code from one language to another. Source-to-source migration, or transpilation, is often a complex, manual process. Transpilation requires expertise both in the source and target language, making it highly laborious and costly. Languages models for code generation and transpilation are becoming increasingly popular. However, despite capturing code-structure well, code generated by language models is often spurious and contains subtle problems. We propose BatFix , a novel approach that augments language models for transpilation by leveraging program repair and synthesis to fix the code generated by these models. BatFix takes as input both the original program, the target program generated by the machine translation model, and a set of test cases and outputs a repaired program that passes all test cases. Experimental results show that our approach is agnostic to language models and programming languages. BatFix can locate bugs spawning multiple lines and synthesize patches for syntax and semantic bugs for programs migrated from Java to C++ and Python to C++ from multiple language models, including, OpenAI’s Codex .

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. We are hopeful that this is just a first step towards providing a unified proof logging approach that will extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

Software developers often struggle to update APIs, leading to manual, time-consuming, and error-prone processes. We introduce Melt, a new approach that generates lightweight API migration rules directly from pull requests in popular library repositories. Our key insight is that pull requests merged into open-source libraries are a rich source of information sufficient to mine API migration rules. By leveraging code examples mined from the library source and automatically generated code examples based on the pull requests, we infer transformation rules in Comby, a language for structural code search and replace. Since inferred rules from single code examples may be too specific, we propose a generalization procedure to make the rules more applicable to client projects. Melt rules are syntax-driven, interpretable, and easily adaptable. Moreover, unlike previous work, our approach enables rule inference to seamlessly integrate into the library workflow, removing the need to wait for client code migrations. We evaluated Melt on pull requests from four popular libraries, successfully mining 461 migration rules from code examples in pull requests and 114 rules from auto-generated code examples. Our generalization procedure increases the number of matches for mined rules by 9×. We applied these rules to client projects and ran their tests, which led to an overall decrease in the number of warnings and fixing some test cases demonstrating MELT's effectiveness in real-world scenarios.

It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.

Heuristics are ubiquitous in computer systems. Examples include congestion control, adaptive bit rate streaming, scheduling, load balancing, and caching. In some domains, theoretical proofs have provided clarity on the conditions where a heuristic is guaranteed to work well. This has not been possible in all domains because proving such guarantees can involve combinatorial reasoning making it hard, cumbersome and error-prone. In this paper we argue that computers should help humans with the combinatorial part of reasoning. We model reasoning questions as ∃∀ formulas [1] and solve them using the counterexample guided inductive synthesis (CEGIS) framework. As preliminary evidence, we prototype CCmatic, a tool that semi-automatically synthesizes congestion control algorithms that are provably robust. It rediscovered a recent congestion control algorithm that provably achieves high utilization and bounded delay under a challenging network model. It also found previously unknown variants of the algorithm that achieve different throughput-delay trade-offs.

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

Congestion Control Algorithms (CCAs) impact numerous desirable Internet properties such as performance, stability, and fairness. Hence, the networking community invests substantial effort into studying whether new algorithms are safe for wide-scale deployment. However, operators today are continuously innovating and some deployed CCAs are unpublished - either because the CCA is in beta or because it is considered proprietary. How can the networking community evaluate these new CCAs when their inner workings are unknown?

With the growth of the open-source data science community, both the number of data science libraries and the number of versions for the same library are increasing rapidly. To match the evolving APIs from those libraries, open-source organizations often have to exert manual effort to refactor the APIs used in the code base. Moreover, due to the abundance of similar open-source libraries, data scientists working on a certain application may have an abundance of libraries to choose, maintain and migrate between. The manual refactoring between APIs is a tedious and error-prone task. Although recent research efforts were made on performing automatic API refactoring between different languages, previous work relies on statistical learning with collected pairwise training data for the API matching and migration. Using large statistical data for refactoring is not ideal because such training data will not be available for a new library or a new version of the same library. We introduce Synthesis for Open-Source API Refactoring (SOAR), a novel technique that requires no training data to achieve API migration and refactoring. SOAR relies only on the documentation that is readily available at the release of the library to learn API representations and mapping between libraries. Using program synthesis, SOAR automatically computes the correct configuration of arguments to the APIs and any glue code required to invoke those APIs. SOAR also uses the interpreter's error messages when running refactored code to generate logical constraints that can be used to prune the search space. Our empirical evaluation shows that SOAR can successfully refactor 80% of our benchmarks corresponding to deep learning models with up to 44 layers with an average run time of 97.23 seconds, and 90% of the data wrangling benchmarks with an average run time of 17.31 seconds.

Rust’s type system ensures the safety of Rust programs; however, programmers can side-step some of the strict typing rules by using the unsafe keyword. A common use of unsafe Rust is by libraries. Bugs in these libraries undermine the safety of the entire Rust program. Therefore, it is crucial to thoroughly test library APIs to rule out bugs. Unfortunately, such testing relies on programmers to manually construct test cases, which is an inefficient and ineffective process.

Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems.

Abstract Form validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users. We presentForest, a regular expression synthesizer for digital form validations.Forestproduces a regular expression that matches the desired pattern for the input values and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesize capture conditions for a given regular expression. To increase confidence in the synthesized regular expression, we implement user interaction based on distinguishing inputs. We evaluatedForeston real-world form-validation instances using regular expressions. Experimental results show thatForestsuccessfully returns the desired regular expression in 70% of the instances and outperformsRegel, a state-of-the-art regular expression synthesizer.

Charts are commonly used for data visualization. Generating a chart usually involves performing data transformations, including data pre-processing and aggregation. These tasks can be cumbersome and time-consuming, even for experienced data scientists. Reproducing existing charts can also be a challenging task when information about data transformations is no longer available.

Satisfiability (SAT) solving has become an important technology in computer-aided mathematics with various successes in number and graph theory. In this paper we apply SAT solvers to color infinitely long strips in the plane with a given height and number of colors. The coloring is constrained as follows: two points that are exactly unit distance apart must be colored differently. To finitize the problem, we tile the strips and all points on a tile have the same color. We evaluated our approach using two different tile shapes: squares and hexagons. The visualization of bounded height strips using 3 to 6 colors reveal patterns that are similar to the best known lower bounds for infinite strips. Our method can be a useful tool for mathematicians to search for patterns that can be generalized to infinite strips and allowed us to increase the lower bound for the strip height with 5 colors to an improved height of 1.700084.

In courses that involve programming assignments, giving meaningful feedback to students is an important challenge. Human beings can give useful feedback by manually grading the programs but this is a time-consuming, labor intensive, and usually boring process. Automatic graders can be fast and scale well but they usually provide poor feedback. Although there has been research on improving automatic graders, research on scaling and improving human grading is limited. We propose to scale human grading by augmenting the manual grading process with an equivalence algorithm that can identify the equivalences between student submissions. This enables human graders to give targeted feedback for multiple student submissions at once. Our technique is conservative in two aspects. First, it identifies equivalence between submissions that are algorithmically similar, e.g., it cannot identify the equivalence between quicksort and mergesort. Second, it uses formal methods instead of clustering algorithms from the machine learning literature. This allows us to prove a soundness result that guarantees that submissions will never be clustered together in error. Despite only reporting equivalence when there is algorithmic similarity and the ability to formally prove equivalence, we show that our technique can significantly reduce grading time for thousands of programming submissions from an introductory functional programming course.

Nowadays, many data analysts are domain experts, but they lack programming skills. As a result, many of them can provide examples of data transformations but are unable to produce the desired query. Hence, there is an increasing need for systems capable of solving the problem of Query Reverse Engineering (QRE). Given a database and output table, these systems have to find the query that generated this table. We present SQUARES, a program synthesis tool based on input-output examples that can help data analysts to extract and transform data by synthesizing SQL queries, and table manipulation programs using the R language.

There has been a significant interest in applying programming-by-example to automate repetitive and tedious tasks. However, due to the incomplete nature of input-output examples, a synthesizer may generate programs that pass the examples but do not match the user intent. In this paper, we propose MARS, a novel synthesis framework that takes as input a multi-layer specification composed by input-output examples, textual description, and partial code snippets that capture the user intent. To accurately capture the user intent from the noisy and ambiguous description, we propose a hybrid model that combines the power of an LSTM-based sequence-to-sequence model with the apriori algorithm for mining association rules through unsupervised learning. We reduce the problem of solving a multi-layer specification synthesis to a Max-SMT problem, where hard constraints encode well-typed concrete programs and soft constraints encode the user intent learned by the hybrid model. We instantiate our hybrid model to the data wrangling domain and compare its performance against Morpheus, a state-of-the-art synthesizer for data wrangling tasks. Our experiments demonstrate that our approach outperforms MORPHEUS in terms of running time and solved benchmarks. For challenging benchmarks, our approach can suggest candidates with rankings that are an order of magnitude better than MORPHEUS which leads to running times that are 15x faster than MORPHEUS.

In this demo paper, we introduce Trinity, a general-purpose framework that can be used to quickly build domain-specific program synthesizers for automating many tedious tasks that arise in data science. We illustrate how Trinity can be used by three different users: First, we show how end-users can use Trinity's built-in synthesizers to automate data wrangling tasks. Second, we show how advanced users can easily extend existing synthesizers to support additional functionalities. Third, we show how synthesis experts can change the underlying search engine in Trinity. Overall, this paper is intended to demonstrate how users can quickly use, modify, and extend the Trinity framework with the goal of automating many tasks that are considered to be the "janitor" work of data science.

We propose a new conflict-driven program synthesis technique that is capable of learning from past mistakes. Given a spurious program that violates the desired specification, our synthesis algorithm identifies the root cause of the conflict and learns new lemmas that can prevent similar mistakes in the future. Specifically, we introduce the notion of equivalence modulo conflict and show how this idea can be used to learn useful lemmas that allow the synthesizer to prune large parts of the search space. We have implemented a general-purpose CDCL-style program synthesizer called Neo and evaluate it in two different application domains, namely data wrangling in R and functional programming over lists. Our experiments demonstrate the substantial benefits of conflict-driven learning and show that Neo outperforms two state-of-the-art synthesis tools, Morpheus and Deepcoder, that target these respective domains.

This paper presents a novel component-based synthesis algorithm that marries the power of type-directed search with lightweight SMT-based deduction and partial evaluation. Given a set of components together with their over-approximate first-order specifications, our method first generates a program sketch over a subset of the components and checks its feasibility using an SMT solver. Since a program sketch typically represents many concrete programs, the use of SMT-based deduction greatly increases the scalability of the algorithm. Once a feasible program sketch is found, our algorithm completes the sketch in a bottom-up fashion, using partial evaluation to further increase the power of deduction for rejecting partially-filled program sketches. We apply the proposed synthesis methodology for automating a large class of data preparation tasks that commonly arise in data science. We have evaluated our synthesis algorithm on dozens of data wrangling and consolidation tasks obtained from on-line forums, and we show that our approach can automatically solve a large class of problems encountered by R users.

Component-based approaches to program synthesis assemble programs from a database of existing components, such as methods provided by an API. In this paper, we present a novel type-directed algorithm for component-based synthesis. The key novelty of our approach is the use of a compact Petri-net representation to model relationships between methods in an API. Given a target method signature S, our approach performs reachability analysis on the underlying Petri-net model to identify sequences of method calls that could be used to synthesize an implementation of S. The programs synthesized by our algorithm are guaranteed to type check and pass all test cases provided by the user.

Abstract Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and test case generation are some of the most common applications of automated verification tools based on bounded model checking (BMC). Existing industrial tools for embedded software use an off-the-shelf bounded model checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This article reports on the extension of the software model checker C BMC to support incremental BMC and its successful integration with the industrial embedded software verification tool BTC E MBEDDED TESTER . We present an extensive evaluation over large industrial embedded programs, mainly from the automotive industry. We show that incremental BMC cuts runtimes by one order of magnitude in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software. We furthermore report promising results on analysing programs with arbitrary loop structure using incremental BMC, demonstrating its applicability and potential to verify general software beyond the embedded domain.

In many common scenarios, programmers need to implement functionality that is already provided by some third party library. This paper presents a tool called Hunter that facilitates code reuse by finding relevant methods in large code bases and automatically synthesizing any necessary wrapper code. Since Hunter internally uses advanced program synthesis technology, it can automatically reuse existing methods even when code adaptation is necessary. We have implemented Hunter as an Eclipse plug-in and evaluate it by (a) comparing it against S6, a state-of-the-art code reuse tool, and (b) performing a user study. Our evaluation shows that Hunter compares favorably with S6 and increases programmer productivity.

Linear search algorithms have been shown to be particularly effective for solving partial Maximum Satisfiability (MaxSAT) problem instances. These algorithms start by adding a new relaxation variable to each soft clause and solving the resulting formula with a SAT solver. Whenever a Model is found, a new constraint on the relaxation variables is added such that Models with a greater or equal value are excluded. However, if the problem instance has a large number of relaxation variables, then adding a new constraint over these variables can lead to the exploration of a much larger search space. This article proposes new algorithms to improve the performance of linear search algorithms for MaxSAT by using Models found by the SAT solver to partition the relaxation variables. These algorithms add a new constraint on a subset of relaxation variables, thus intensifying the search on that subspace. In addition, the proposed algorithms are further enhanced by using incremental approaches where learned clauses are kept between calls to the SAT solver. Experimental results show that Model-based algorithms can outperform a classic linear search algorithm in several problem instances. Moreover, incremental approaches further improve the performance of linear search and Model-based algorithms for MaxSAT. Overall, Model-based algorithms are competitive with state-of-the-art MaxSAT solvers, and can improve their performance when solving problem instances with a large number of soft clauses.

Cardinality constraints appear in many practical problems and have been well studied in the past. There are many CNF encodings for cardinality constraints, although it is not clear which encodings perform better. Indeed, different encodings can perform well over different problems. This paper examines a large number of cardinality encodings and evaluates their performance for solving the problem of Maximum Satisfiability (MaxSAT). Taking advantage of the diversification of cardinality encodings, we propose to exploit those encodings in parallel MaxSAT solving. Our parallel solver, pMAX, simultaneously searches in the lower and upper bound of the optimum value, and different cardinality encodings are used in each thread to increase the diversification of the search. Moreover, learned clauses are shared between threads during the search. Experimental results show that our parallel solver outperforms other sequential and parallel state-of-the-art MaxSAT solvers.

The last two decades progresses have led Propositional Satisfiability (SAT) to be a competitive practical approach to solve a wide range of industrial and academic problems. Thanks to these advances, the size and difficulty of the SAT instances have grown significantly. The demand for more computational power led to the creation of new computer architectures and paradigms composed by multiple machines connected by a network to act as one machine, like clusters and grids. However, extra computing power is not coming anymore from higher processor frequencies, but rather from a growing number of computing cores and processors. It becomes clear that exploiting this new architecture is essential for the evolution of SAT solvers. Search space splitting is probably the most commonly used strategy to explore the parallelism provided by the search space. However, it is not clear how to find the relevant set of variables to divide the search space. This paper extends a method based on the VSIDS heuristic to find the initial set of partition variables. A drawback of search space splitting is load balancing. To overcome this problem, we propose the use of a hybrid approach between search space splitting and portfolio. Preliminary results show that both these techniques improve the performance of the solver and reveal that combining search space splitting and portfolio approaches can lead to better results.