Automated synthesis techniques generate systems—such as functions or circuits—that provably satisfy a formal specification. Traditional synthesis frameworks often adopt an all-or-nothing approach: either the system satisfies all constraints, or synthesis fails. However, in many practical settings, such strict completeness is either infeasible or too costly to achieve, especially in terms of resources like time, memory, or circuit area. This work addresses such scenarios by moving beyond the all-or-nothing paradigm. We propose a novel synthesis framework that distinguishes between hard constraints, which must be strictly satisfied, and soft constraints, which may be relaxed. The goal is to synthesize systems that provably satisfy all hard constraints while achieving a user-defined threshold of satisfiability on the soft constraints. We quantify this relaxation using a satisficing measure, such as accuracy—i.e., the proportion of inputs for which the system satisfies all constraints.Our approach integrates AI-based methods to generate candidate systems and automated reasoning techniques to ensure formal guarantees. Through extensive experiments, we show that our framework significantly reduces synthesis time compared to traditional approaches. Moreover, the synthesized systems (e.g., circuits) tend to be smaller, connecting our method naturally to the domain of approximate circuit synthesis. Unlike existing approximate synthesis techniques, our framework provides formal guarantees on both correctness (for hard constraints) and quality (for soft constraints).

Designing abstract transformers for program-analysis tools is a challenging task. In the past, bugs have been discovered in such transformers, showing the difficulty of designing such transformers manually, and providing motivation for automated techniques. Recently, Kalita et al. showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) \({\mathcal{L}}\) (i.e., “ \({\mathcal{L}}\) -transformers”). Their technique creates provably sound and maximally precise \({\mathcal{L}}\) -transformers for an abstract domain \( A \) —i.e., given specifications of a concrete operation op , DSL \({\mathcal{L}}\) , and abstract domain \( A \) , it finds a best abstract \({\mathcal{L}}\) -transformer for op in \( A \) . However, we found that the algorithm of Kalita et al. does not succeed when applied to reduced-product domains: The need to synthesize transformers for all of the domains simultaneously blows up the search space. Because reduced-product domains are an important device for improving the precision of abstract interpretation, in this article, we propose an algorithm to synthesize reduced \({\mathcal{L}}\) -transformers \(\langle{f}^{\sharp\textsf{R}}_{1},{f}^{\sharp\textsf{R}}_{2},\dots,{f}^{\sharp \textsf{R}}_{n}\rangle\) for a product domain \(A_{1}\times A_{2}\times\dots\times A_{n}\) , using multiple DSLs: \({\mathcal{L}}\) \(=\langle{\mathcal{L}}_{1},{\mathcal{L}}_{2},\ldots,{\mathcal{L}}_{n}\rangle\) . Synthesis of reduced-product transformers is quite challenging: First, the synthesis task has to tackle an increased “feature set” because each component transformer now has access to the abstract inputs from all component domains in the product. Second, to ensure that the product transformer is maximally precise, the synthesis task needs to arrange for the component transformers to cooperate with each other. We implemented our algorithm in a tool, Amurth2 , and used it to synthesize abstract transformers for two product domains—SAFE and JSAI—available within the SAFE str framework for JavaScript program analysis. For four of the six operations supported by SAFE str , Amurth2 synthesizes more precise abstract transformers than the manually written ones available in SAFE str .

Memory safety violations in low-level code, written in languages like C, continues to remain one of the major sources of software vulnerabilities. One method of removing such violations by construction is to port C code to a safe C dialect. Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead. This porting, however, is a manual process that imposes significant burden on the programmer and, hence, there has been limited adoption of this technique. The task of porting not only requires inferring annotations, but may also need refactoring/rewriting of the code to make it amenable to such annotations. In this paper, we use Large Language Models (LLMs) towards addressing both these concerns. We show how to harness LLM capabilities to do complex code reasoning as well as rewriting of large codebases. We also present a novel framework for whole-program transformations that leverages lightweight static analysis to break the transformation into smaller steps that can be carried out effectively by an LLM. We implement our ideas in a tool called MSA that targets the CheckedC dialect. We evaluate MSA on several micro-benchmarks, as well as real-world code ranging up to 20K lines of code. We showcase superior performance compared to a vanilla LLM baseline, as well as demonstrate improvement over a state-of-the-art symbolic (non-LLM) technique.

We present our tool, AndroFL, that provides an infrastructure for an evolutionary algorithm-based test-suite generation backed by a statistical fault localization module for diagnosing faults. AndroFL’s evolutionary test-generator supports configurable fitness functions (e.g., coverage, diagnosability metrics like Ulysis). The statistical fault localization engine supports popular metrics like Ochiai, Tarantula and Barinel, and allows adding custom fault localization metrics. We evaluated AndroFL on 20 open-sourced apps from F-Droid, and demonstrates significant efficiency gains: it reduces debugging effort by 74% (median EXAM score) compared to random testing—enabling developers to pinpoint faults ≈ 4× faster. Furthermore, AndroFL localizes 25% and 50% more faults compared to random testing in the top-5 and top-10 ranked list in worst case ranking scenario.

An open program is one for which the complete source code is not available, which is a reality for real-world program verification. Software verification tools tend to assume the worst about any unconstrained behavior and this can yield an enormous number of spurious warnings for open programs. For any serious verification effort, the engineer must invest time up-front in building a suitable model (or mock) of any missing code, which is time-consuming and error-prone. Inaccuracies in the mocks can lead to incorrect verification results. In this paper, we demonstrate a technique that is capable of distinguishing between false positives and actual bugs from potential memory-safety violations in an open program with high accuracy. Central to the technique is the ability of making angelic assumptions about missing code. To accomplish this, we first mine a set of idiomatic patterns in buffer-manipulating programs using a large language model (LLM). This is complemented by a formal synthesis strategy that performs property-directed reasoning to select, adapt and instantiate these idiomatic patterns into angelic assumptions on the target program. Overall, our system, Seeker, guarantees that a program is deemed correct only if it can be verified under a well-defined set of “trusted” idiomatic patterns. In our experiments over a set of benchmarks curated from popular open-source software, our tool Seeker is able to identify 79% of the false positives with zero false negatives.

Abstract Interactive theorem provers (ITPs) exploit the collaboration between humans and computers, enabling proof of complex theorems. Further, ITPs allow extraction of provably correct implementations from proofs. However, often, the extracted code interface with external libraries containing real-life complexities—proprietary library calls, remote/cloud APIs, complex models like ML models, inline assembly, highly non-linear arithmetic, vector instructions etc. We refer to such functions/operations as closed-box components . For such components, the user has to provide appropriate assumed lemmas to model the behavior of these functions. However, we found instances where these assumed lemmas are inconsistent with the actual semantics of these closed-box components. Hence, even correct-by-construction code extracted from an ITP may still behave incorrectly when interfaced with such closed-box components . To this end, we propose StarFuzz , that allows the $$\text {F}^\star $$ F ⋆ interactive theorem prover to provide better end-to-end assurance on the application— even when interfaced with the closed-box components . Under the hood, StarFuzz rides on Sādhak , an SMT solver that combines fuzz testing to allow satisfiability checking over closed-box components. On the $$\text {F}^\star $$ F ⋆ library that includes external implementations in OCaml, StarFuzz discovered four bugs—one bug that revealed an error on the assumed lemmas for a closed-box function, and three bugs in the external implementations of these components.

What-Comes-Next (WCN) puzzles challenge us to identify the next figure that "logically follows" a provided sequence of figures. WCN puzzles are a favorite of interviewers and examiners---there is hardly any aptitude test that misses WCN puzzles. In this work, we propose to automatically synthesize WCN puzzles. The key insight to our methodology is that generation of WCN problems can be posed as a program synthesis problem. We design a small yet expressive language, PuzzlerLang, to capture solutions to WCN puzzles. PuzzlerLang is expressive enough to explain almost all human generated WCN puzzles that we collected, and yet, small enough to allow synthesis in a reasonable time. To ensure that the generated puzzles are appealing to humans, we infer a machine learning model to approximate the appeal factor of given WCN puzzle to humans. We use this model within our puzzle synthesizer as an optimization function to generate highly appealing and correct-by-construction WCN puzzles. We implemented our ideas in a tool, PuzzleGen; we found that PuzzleGen is fast, clocking an average time of about 3.4s per puzzle. Further, statistical tests over the responses from a user-study supported that the PuzzleGen generated puzzles were indistinguishable from puzzles created by humans.

Abstract We propose a novel lazy bounded model checking (BMC) algorithm, Trace Inlining, that identifies relevant behaviors of the program to compute partial proofs as procedural summaries. Whenever procedures are reused in other contexts, Trace Inlining attempts to construct safety proofs using these summaries. If the current summaries are sufficient to complete the proof, it gains both in solving times and smaller encodings. If the summaries are found to be insufficient, they are automatically refined for future use. The partial proofs are enabled by a sequence of alternating underapproximation and overapproximation rounds until the program verification condition is found to be unsatisfiable. We evaluate our Trace Inlining algorithm on real-world benchmarks consisting of Windows and Linux device drivers. Our results show that the proposed algorithm is able to solve 12% additional benchmarks that were unsolved by state-of-the-art lazy BMC solvers Corral and Legion. Further, Trace Inlining is 6 $$\times $$ × faster than Corral and 3 $$\times $$ × faster than Legion in terms of verification time. The virtual best of all three verifiers is 4 $$\times $$ × faster than the virtual best of Corral and Legion, implying that our technique significantly improves on what is possible today.

Abstract Logic locking was designed to be a formidable barrier to IP piracy: given a logic design, logic locking modifies the logic design such that the circuit operates correctly only if operated with the “correct”secretkey. However, strong attacks (like SAT-based attacks) soon exposed the weakness of this defense.Stripped functionality logic locking(SFLL) was recently proposed as a strong variant of logic locking. SFLL was designed to be resilient against SAT attacks, which was the bane of conventional logic locking techniques. However, all SFLL-protected designs share certain “circuit patterns” that expose them to new attacks that employstructural analysisof the locked circuits. In this work, we propose a new methodology—Structurally Robust SFLL( $$\mathcal{S}\mathcal{R}$$ SR -SFLL)—that uses the power of modern satisfiability and synthesis engines to produce semantically equivalent circuits that are resilient against such structural attacks. On our benchmarks, $$\mathcal{S}\mathcal{R}$$ SR -SFLLwas able to defend all circuit instances against both structural and SAT attacks, while all of them were broken when defended using SFLL. Further, we show that designing such defenses is challenging: we design a variant of our proposal, $$\mathcal{S}\mathcal{R}$$ SR -SFLL(0), that is also robust against existing structural attacks but succumbs to a new attack,SyntAk(also proposed in this work).SyntAkuses synthesis technology to compile $$\mathcal{S}\mathcal{R}$$ SR -SFLL(0)locked circuits into semantically equivalent variants that have structural vulnerabilities. $$\mathcal{S}\mathcal{R}$$ SR -SFLL, however, remains resilient toSyntAk.

Quantified Boolean Formulas (QBF) extend propositional logic with quantification$\forall,\exists$. In QBF, an existentially quantified variable is allowed to depend on all universally quantified variables in its scope. Dependency Quantified Boolean Formulas (DQBF) restrict the dependencies of existentially quantified variables. In DQBF, existentially quantified variables have explicit dependencies on a subset of universally quantified variables, called Henkin dependencies. Given a Boolean specification between the set of inputs and outputs, the problem of Henkin synthesis is to synthesize each output variable as a function of its Henkin dependencies such that the specification is met. Henkin synthesis has wide-ranging applications, including verification of partial circuits, controller synthesis, and circuit realizability. This work proposes a data-driven approach for Henkin synthesis called Manthan3. On an extensive evaluation of over 563 instances arising from past DQBF solving competitions, we demonstrate that Manthan3 is competitive with state-of-the-art tools. Furthermore, Manthan3 solves 26 benchmarks that none of the current state-of-the-art techniques could solve.

The weakest pre-expectation framework from Morgan and McIver for deductive verification of probabilistic programs generalizes binary state assertions to real-valued expectations to measure expected values of expressions over probabilistic program variables. While loop-free programs can be analyzed by mechanically transforming expectations, verifying programs with loops requires finding an invariant expectation. We view invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. With this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach learns piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper- or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature.

Spectrum-based Fault Localization (SBFL) uses the coverage of test cases and their outcome (pass/fail) to predict the "suspiciousness'' of program components, e.g., lines of code. SBFL is, perhaps, the most successful fault localization technique due to its simplicity and scalability. However, SBFL heuristics do not perform well in scenarios where a program may have multiple faulty components. In this work, we propose a new algorithm that "augments'' previously proposed SBFL heuristics to produce a ranked list where faulty components ranked low by base SBFL metrics are ranked significantly higher. We implement our ideas in a tool, ARTEMIS, that attempts to "bubble up'' faulty components which are ranked lower by base SBFL metrics. We compare our technique to the most popular SBFL metrics and demonstrate statistically significant improvement in the developer effort for fault localization with respect to the basic strategies.

Program analysis, verification and testing are important topics in programming languages and software engineering. They aim to produce engineers who are not only capable of empirically evaluating but, also formally reasoning on the correctness of software systems. We propose a specialized framework, Chiron, designed to teach graduate-level courses on these topics. Chiron has a small code base for easy understanding, uses a unified intermediate representation across all its analysis modules, maintains a modular architecture for plugging in new algorithms and uses a “fun” programming language to provide a gamified experience. Currently, it packages a dataflow analysis engine for driving compiler optimizations, an abstract interpretation engine for verification, a symbolic execution engine, a fuzzer and an evolutionary test generator for program testing, and a spectrum based statistical bug localization module. Within Chiron, program analysis tasks are posed in an unconventional setting (as adventures of a turtle) to provide a gamified experience; the accompanying animations (showing the movements of the turtle) allow the student to understand the underlying concepts better, and the detailed logs allow the teaching assistants in their grading activities. Chiron has been used in two offerings of a graduate level course on program analysis, verification and testing. In response to our survey questionnaire, all the students unanimously held the opinion that Chiron was extremely helpful in aiding their learning, and recommended its use in similar courses.

Abstract Morgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task. We propose a new view of invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. Guided by this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach can learn piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper- or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature.

Abstract Bounded Model Checking (BMC) is a popularly used strategy for program verification and it has been explored extensively over the past decade. Despite such a long history, BMC still faces scalability challenges as programs continue to grow larger and more complex. One approach that has proven to be effective in verifying large programs is called Counterexample Guided Abstraction Refinement (CEGAR). In this work, we propose a complementary approach to CEGAR for bounded model checking of sequential programs: in contrast to CEGAR, our algorithm gradually widens underapproximations of a program, guided by the proofs of unsatisfiability. We implemented our ideas in a tool called Legion. We compare the performance of Legion against that of Corral, a state-of-the-art verifier from Microsoft, that utilizes the CEGAR strategy. We conduct our experiments on 727 Windows and Linux device driver benchmarks. We find that Legion is able to solve 12% more instances than Corral and that Legion exhibits a complementary behavior to that of Corral. Motivated by this, we also build a portfolio verifier, $$\textsc {Legion}^{+}$$ L E G I O N + , that attempts to draw the best of Legion and Corral. Our portfolio, $$\textsc {Legion}^{+}$$ L E G I O N + , solves 15% more benchmarks than Corral with similar computational resource constraints (i.e. each verifier in the portfolio is run with a time budget that is half of the time budget of Corral). Moreover, it is found to be $$2.9\times $$ 2.9 × faster than Corral on benchmarks that are solved by both Corral and $$\textsc {Legion}^{+}$$ L E G I O N + .

Real-life programs contain multiple operations whose semantics are unavailable to verification engines, like third-party library calls, inline assembly and SIMD instructions, special compiler-provided primitives, and queries to uninterpretable machine learning models. Even with the exceptional success story of program verification, synthesis of inductive invariants for such "open" programs has remained a challenge. Currently, this problem is handled by manually "closing" the program---by providing hand-written stubs that attempt to capture the behavior of the unmodelled operations; writing stubs is not only difficult and tedious, but the stubs are often incorrect---raising serious questions on the whole endeavor. In this work, we propose Almost Correct Invariants as an automated strategy for synthesizing inductive invariants for such "open" programs. We adopt an active learning strategy where a data-driven learner proposes candidate invariants. In deviation from prior work that attempt to verify invariants, we attempt to falsify the invariants: we reduce the falsification problem to a set of reachability checks on non-deterministic programs; we ride on the success of modern fuzzers to answer these reachability queries. Our tool, Achar, automatically synthesizes inductive invariants that are sufficient to prove the correctness of the target programs. We compare Achar with a state-of-the-art invariant synthesis tool that employs theorem proving on formulae built over the program source. Though Achar is without strong soundness guarantees, our experiments show that even when we provide almost no access to the program source, Achar outperforms the state-of-the-art invariant generator that has complete access to the source. We also evaluate Achar on programs that current invariant synthesis engines cannot handle---programs that invoke external library calls, inline assembly, and queries to convolution neural networks; Achar successfully infers the necessary inductive invariants within a reasonable time.

Abstract Logic locking “hides” the functionality of a digital circuit to protect it from counterfeiting, piracy, and malicious design modifications. The original design is transformed into a “locked” design such that the circuit reveals its correct functionality only when it is “unlocked” with a secret sequence of bits—the key bit-string. However, strong attacks, especially the SAT attack that uses a SAT solver to recover the key bit-string, have been profoundly effective at breaking the locked circuit and recovering the circuit functionality. We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a higher-order relation, instead of a key of independent values, challenging the attacker to discover this key relation to recreate the circuit functionality. Our technique uses program synthesis to construct the locked design and synthesize a corresponding key relation. HOLL has low overhead and existing attacks for logic locking do not apply as the entity to be recovered is no more a value. To evaluate our proposal, we propose a new attack (SynthAttack) that uses an inductive synthesis algorithm guided by an operational circuit as an input-output oracle to recover the hidden functionality. SynthAttack is inspired by the SAT attack, and similar to the SAT attack, it is verifiably correct, i.e., if the correct functionality is revealed, a verification check guarantees the same. Our empirical analysis shows that SynthAttack can break HOLL for small circuits and small key relations, but it is ineffective for real-life designs.

This paper addresses the problem of creating abstract transformers automatically. The method we present automates the construction of static analyzers in a fashion similar to the way yacc automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides specifications of (i) the concrete semantics of a given operation op , (ii) the abstract domain A to be used by the analyzer, and (iii) the semantics of a domain-specific language L in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for op in abstract domain A , expressed in L (an “ L -transformer for op over A ”). Moreover, the abstract transformer obtained is a most-precise L -transformer for op over A ; that is, there is no other L -transformer for op over A that is strictly more precise. We implemented our method in a tool called AMURTH. We used AMURTH to create sets of replacement abstract transformers for those used in two existing analyzers, and obtained essentially identical performance. However, when we compared the existing transformers with the transformers obtained using AMURTH, we discovered that four of the existing transformers were unsound, which demonstrates the risk of using manually created transformers.

Programming languages and software engineering tools routinely encounter components that are difficult to reason on via formal techniques or whose formal semantics are not even available—third-party libraries, inline assembly code, SIMD instructions, system calls, calls to machine learning models, etc. However, often access to these components is available as input-output oracles—interfaces are available to query these components on certain inputs to receive the respective outputs. We refer to such functions as closed-box functions . Regular SMT solvers are unable to handle such closed-box functions. We propose Sādhak, a solver for SMT theories modulo closed-box functions. Our core idea is to use a synergistic combination of a fuzzer to reason on closed-box functions and an SMT engine to solve the constraints pertaining to the SMT theories. The fuzz and the SMT engines attempt to converge to a model by exchanging a rich set of interface constraints that are relevant and interpretable by them. Our implementation, Sādhak, demonstrates a significant advantage over the only other solver that is capable of handling such closed-box constraints: Sādhak solves 36.45% more benchmarks than the best-performing mode of this state-of-the-art solver and has 5.72x better PAR-2 score; on the benchmarks that are solved by both tools, Sādhak is (on an average) 14.62x faster.

We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of probabilistic symbolic variables , which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the KLEE symbolic execution engine alongside multiple optimizations and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds’ algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against Psi, an exact probabilistic symbolic inference engine, and Storm, a probabilistic model checker, and show that our method significantly outperforms both tools.

Given a propositional formula ψ, the model counting problem, also referred to as #SAT, seeks to compute the number of satisfying assignments (or models) of ψ. Modern search-based model counting algorithms are built on conflict-driven clause learning, combined with the caching of certain subformulas (called components) encountered during the search process. Despite significant progress in these algorithms over the years, state-of-the-art model counters often struggle to handle large but structured instances that typically arise in combinatorial settings. Motivated by the observation that these counters do not exploit the inherent symmetries exhibited in such instances, we revisit the component caching architecture employed in current counters and introduce a novel caching scheme that focuses on identifying symmetric components. We first prove the soundness of our approach, and then integrate it into the state-of-the-art model counter GANAK. Our extensive experiments on hard combinatorial instances demonstrate that the resulting counter, SymGANAK, leads to improvements over GANAK both in terms of PAR-2 score and the number of instances solved.

Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state-of-the-art approach combines machine learning and automated reasoning to synthesise Boolean functions efficiently. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates. We implement these improvements in the state-of-the-art framework, called Manthan. The proposed framework is called Manthan2. Manthan2 shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan - an increment of 153 instances over the state-of-the-art. To put this into perspective, Manthan improved on the prior state-of-the-art by only 76 instances.

Given a specification φ(X, Y ) over inputs X and output Y and defined over a background theory T, the problem of program synthesis is to design a program f such that Y = f (X), satisfies the specification φ. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach to program synthesis where in addition to the specification φ, the end-user also specifies a grammar L to aid the underlying synthesis engine. This paper investigates the feasibility of synthesis techniques without grammar, a sub-class defined as T constrained synthesis. We show that T-constrained synthesis can be reduced to DQF(T),i.e., to the problem of finding a witness of a dependency quantified formula modulo theory. When the underlying theory is the theory of bitvectors, the corresponding DQF problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific program synthesis techniques; thereby positioning DQBF as a core representation language for program synthesis. Our empirical analysis shows that T-constrained synthesis can achieve significantly better performance than syntax-guided approaches. Furthermore, the general-purpose DQBF solvers perform on par with domain-specific synthesis techniques.

Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decade. Despite intense algorithmic development, a large number of problems remain beyond the reach of the state of the art techniques. Motivated by the progress in machine learning, we propose $$\textsf {Manthan}$$ , a novel data-driven approach to Boolean functional synthesis. $$\textsf {Manthan}$$ views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that $$\textsf {Manthan}$$ significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. Furthermore, $$\textsf {Manthan}$$ solves 60 benchmarks that none of the current state of the art techniques could solve. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.

Programming environments for sequential programs provide strong debugging support. However, concurrent programs, especially under relaxed memory models, lack powerful interactive debugging tools. In this work, we present Gambit, an interactive debugging environment that uses gdb to run a concrete debugging session on a concurrent program, while employing a symbolic execution on the program trace in the background simultaneously. The symbolic execution is analysed by a theorem prover to answer queries from the programmer on possible scenarios resulting from alternate thread interleavings or due to reorderings on other relaxed memory models.

Program verification is a resource-hungry task.This paper looks at the problem of parallelizing SMT-based automated program verification, specifically bounded model-checking, so that it can be distributed and executed on a cluster of machines.We present an algorithm that dynamically unfolds the call graph of the program and frequently splits it to create sub-tasks that can be solved in parallel.The algorithm is adaptive, controlling the splitting rate according to available resources, and also leverages information from the SMT solver to split where most complexity lies in the search.We implemented our algorithm by modifying CORRAL, the verifier used by Microsoft's Static Driver Verifier (SDV), and evaluate it on a series of hard SDV benchmarks.

Spectrum-based Fault Localization (SFL) approaches aim to efficiently localize faulty components from examining program behavior. This is done by collecting the execution patterns of various combinations of components and the corresponding outcomes into a spectrum. Efficient fault localization depends heavily on the quality of the spectra. Previous approaches, including the current state-of-the-art Density- Diversity-Uniqueness (DDU) approach, attempt to generate “good” test-suites by improving certain structural properties of the spectra. In this work, we propose a different approach, Multiverse Analysis, that considers multiple hypothetical universes, each corresponding to a scenario where one of the components is assumed to be faulty, to generate a spectrum that attempts to reduce the expected worst-case wasted effort over all the universes. Our experiments show that the Multiverse Analysis not just improves the efficiency of fault localization but also achieves better coverage and generates smaller test-suites over DDU, the current state-of-the-art technique. On average, our approach reduces the developer effort over DDU by over 16% for more than 92% of the instances. Further, the improvements over DDU are indeed statistically significant on the paired Wilcoxon Signed-rank test.

Given a Boolean formula F, the problem of model counting, also referred to as #SAT, seeks to compute the number of solutions of F. Model counting is a fundamental problem with a wide variety of applications ranging from planning, quantified information flow to probabilistic reasoning and the like. The modern #SAT solvers tend to be either based on static decomposition, dynamic decomposition, or a hybrid of the two. Despite dynamic decomposition based #SAT solvers sharing much of their architecture with SAT solvers, the core design and heuristics of dynamic decomposition-based #SAT solvers has remained constant for over a decade. In this paper, we revisit the architecture of the state-of-the-art dynamic decomposition-based #SAT tool, sharpSAT, and demonstrate that by introducing a new notion of probabilistic component caching and the usage of universal hashing for exact model counting along with the development of several new heuristics can lead to significant performance improvement over state-of-the-art model-counters. In particular, we develop GANAK, a new scalable probabilistic exact model counter that outperforms state-of-the-art exact and approximate model counters sharpSAT and ApproxMC3 respectively, both in terms of PAR-2 score and the number of instances solved. Furthermore, in our experiments, the model count returned by GANAK was equal to the exact model count for all the benchmarks. Finally, we observe that recently proposed preprocessing techniques for model counting benefit exact model counters while hurting the performance of approximate model counters.

Concretization is an effective weapon in the armory of symbolic execution engines. However, concretization can lead to loss in coverage, path divergence, and generation of test-cases on which the intended bugs are not reproduced. In this paper, we propose an algorithm, Deferred Concretization, that uses a new category for values within symbolic execution (referred to as the symcrete values) to pend concretization till they are actually needed. Our tool, COLOSSUS, built around these ideas, was able to gain an average coverage improvement of 66.94% and reduce divergence by more than 55% relative to the state-of-the-art symbolic execution engine, KLEE. Moreover, we found that KLEE loses about 38.60% of the states in the symbolic execution tree that COLOSSUS is able to recover, showing that COLOSSUS is capable of covering a much larger coverage space.

Given a set of constraints F and a user-defined weight function W on the assignment space, the problem of constrained sampling is to sample satisfying assignments of F conditioned on W. Constrained sampling is a fundamental problem with applications in probabilistic reasoning, synthesis, software and hardware testing. Consequently, the problem of sampling has been subject to intense theoretical and practical investigations over the years. Despite such intense investigations, there still remains a gap between theory and practice. In particular, there has been significant progress in the development of sampling techniques when W is a uniform distribution, but such techniques fail to handle general weight functions W. Furthermore, we are, often, interested in $$\varSigma _1^1$$ formulas, i.e., $$G(X):=\,\exists Y F(X, Y)$$ for some F; typically the set of variables Y are introduced as auxiliary variables during encoding of constraints to F. In this context, one wonders whether it is possible to design sampling techniques whose runtime performance is agnostic to the underlying weight distribution and can handle $$\varSigma _1^1$$ formulas? The primary contribution of this work is a novel technique, called $$\mathsf {WAPS}$$ , for sampling over $$\varSigma _1^1$$ whose runtime is agnostic to W. $$\mathsf {WAPS}$$ is based on our recently discovered connection between knowledge compilation and uniform sampling. $$\mathsf {WAPS}$$ proceeds by compiling F into a well studied compiled form, d-DNNF, which allows sampling operations to be conducted in linear time in the size of the compiled form. We demonstrate that $$\mathsf {WAPS}$$ can significantly outperform existing state-of-the-art weighted and projected sampler $$\mathsf {WeightGen}$$ , by up to 3 orders of magnitude in runtime while achieving a geometric speedup of $$296{\times }$$ and solving 564 more instances out of 773. The distribution generated by $$\mathsf {WAPS}$$ is statistically indistinguishable from that generated by an ideal weighted and projected sampler. Furthermore, $$\mathsf {WAPS}$$ is almost oblivious to the number of samples requested.

Uniform sampling has drawn diverse applications in programming languages and software engineering, like in constrained-random verification (CRV), constrained-fuzzing and bug synthesis. The effectiveness of these applications depend on the uniformity of test stimuli generated from a given set of constraints. Despite significant progress over the past few years, the performance of the state of the art techniques still falls short of those of heuristic methods employed in the industry which sacrifice either uniformity or scalability when generating stimuli. In this paper, we propose a new approach to the uniform generation that builds on recent progress in knowledge compilation. The primary contribution of this paper is marrying knowledge compilation with uniform sampling: our algorithm, KUS, employs the state-of-the-art knowledge compilers to first compile constraints into d-DNNF form, and then, generates samples by making two passes over the compiled representation. We show that KUS is able to significantly outperform existing state-of-the-art algorithms, SPUR and UniGen2, by up to 3 orders of magnitude in terms of runtime while achieving a geometric speedup of 1.7× and 8.3× over SPUR and UniGen2 respectively. Also, KUS achieves a lower PAR-21 score, around 0.82× that of SPUR and 0.38× that of UniGen2. Furthermore, KUS achieves speedups of up to 3 orders of magnitude for incremental sampling. The distribution generated by KUS is statistically indistinguishable from that generated by an ideal uniform sampler. Moreover, KUS is almost oblivious to the number of samples requested.

In this work, we propose the notion of a Parse Condition—a logical condition that is satisfiable if and only if a given string w can be successfully parsed using a grammar G. Further, we propose an algorithm for building an SMT encoding of such parse conditions for LL(1) grammars and demonstrate its utility by building two applications over it: automated repair of syntax errors in Tiger programs and automated parser synthesis to automatically synthesize LL(1) parsers from examples. We implement our ideas into a tool, Cyclops, that is able to successfully repair 80% of our benchmarks (675 buggy Tiger programs), clocking an average of 30 seconds per repair and synthesize parsers for interesting languages from examples. Like verification conditions (encoding a program in logic) have found widespread applications in program analysis, we believe that Parse Conditions can serve as a foundation for interesting applications in syntax analysis.

In spite of decades of research in bug detection tools, there is a surprising dearth of ground-truth corpora that can be used to evaluate the efficacy of such tools. Recently, systems such as LAVA and EvilCoder have been proposed to automatically inject bugs into software to quickly generate large bug corpora, but the bugs created so far differ from naturally occurring bugs in a number of ways. In this work, we propose a new automated bug injection system, Apocalypse, that uses formal techniques—symbolic execution, constraint-based program synthesis and model counting—to automatically inject fair (can potentially be discovered by current bug-detection tools), deep (requiring a long sequence of dependencies to be satisfied to fire), uncorrelated (each bug behaving independent of others), reproducible (a trigger input being available) and rare (can be triggered by only a few program inputs) bugs in large software code bases. In our evaluation, we inject bugs into thirty Coreutils programs as well as the TCAS test suite. We find that bugs synthesized by Apocalypse are highly realistic under a variety of metrics, that they do not favor a particular bug-finding strategy (unlike bugs produced by LAVA), and that they are more difficult to find than manually injected bugs, requiring up around 240× more tests to discover with a state-of-the-art symbolic execution tool.

The Hot Path SSA (HPSSA) form filled a long-standing void by providing an SSA-like intermediate representation that could weave static program code and run-time profile information in a single data structure, thereby facilitating speculative analyses and optimizations. The original algorithm proposed for the Hot Path SSA construction builds HPSSA over non-SSA programs with interleaved SSA and HPSSA construction passes. In this work, we propose a new algorithm for constructing HPSSA programs from programs in the SSA form.

We present Wolverine, an integrated Debug-Repair environment for heap manipulating programs. Wolverine facilitates stepping through a concrete program execution, provides visualizations of the abstract program states (as box-and-arrow diagrams) and integrates a novel, proof-directed repair algorithm to synthesize repair patches. To provide a seamless environment, Wolverine supports "hot-patching" of the generated repair patches, enabling the programmer to continue the debug session without requiring an abort-compile-debug cycle. We also propose new debug-repair possibilities, "specification refinement" and "specification slicing" made possible by Wolverine. We evaluate our framework on 1600 buggy programs (generated using fault injection) on a variety of data-structures like singly, doubly and circular linked-lists, Binary Search Trees, AVL trees, Red-Black trees and Splay trees; Wolverine could repair all the buggy instances within reasonable time (less than 5 sec in most cases). We also evaluate Wolverine on 247 (buggy) student submissions; Wolverine could repair more than 80% of programs where the student had made a reasonable attempt.

Profile-guided optimizing compilers learn from representative executions of a program to "tune" transformations so as to benefit frequent paths. However, these optimizations view the whole run of a program in a monolithic manner. It is known that a program execution proceeds in phases—each phase corresponding to an identifiable set of control-flow behaviors. This implies that not all control-flows are hot (i.e. executed with a high frequency) all the times. Hence, if a program can switch among a set of hot paths for guiding the optimizations in the different phases, the optimizations may yield powerful results. We propose an algorithm that optimizes the clones of a function according to the different phase behaviors exhibited by the function, and dispatches its calls to the (potentially) most beneficial clone at runtime. This makes it possible to use profile information at a finer granularity than existing approaches. We start off by identifying critical functions that exhibit a high differential in its control-flow profiles, thereby exhibiting widely varying phase behavior. For these critical functions, we compile specialized clones that are tuned for each distinct phase behavior. Finally, we build a phase predictor that, at run-time, predicts the phase that a yet-to-be-executed function invocation would evoke (when executed), and guides the function invocation to the respective clone of the function. We build the predictor by learning a classifier over features extracted from the state of the program with the distinct phases acting as class labels. We demonstrate our algorithm by building a concrete phase-directed optimizer for register allocation (pdra) within the PBQP-based register allocator in the LLVM compiler infrastructure. We compare our allocator against the base allocator and a profile-guided allocator (pgra) that uses the profile information in a monolithic manner without extracting phase information.

Interacting with computers is a ubiquitous activity for millions of people. Repetitive or specialized tasks often require creation of small, often one-off, programs. End-users struggle with learning and using the myriad of domain-specific languages (DSLs) to effectively accomplish these tasks.

Given an input that can trigger a concurrency bug, only a subset of possible thread schedules satisfying certain constraints can actually cause such a bug to manifest. Recent proposals on controlled randomization of thread schedules with concrete guarantees on bug detection probabilities have opened promising avenues in this direction. However, to boost the bug detection probability, these techniques typically require a significant number of schedules to be explored. As a result, it is, in general, beneficial to accelerate the schedule space exploration of the multi-threaded programs. In this paper, we introduce Simultaneous Interleaving Exploration with Controlled Sequencing (SINECOSEQ), a generic framework that leverages the high-performance graphics processing units (GPUs) to significantly accelerate schedule space navigation of general-purpose multi-threaded programs. The SINE framework accepts POSIX compliant multi-threaded programs, instruments them to intercept all shared memory accesses, and automatically generates CUDA (Compute Unified Device Architecture) compliant code that navigates the schedule space of the input multi-threaded program on an NVIDIA GPU. Each GPU thread typically explores one schedule of the input program. The COSEQ framework decides how the schedule space is navigated by architecting the schedules on the fly. While it is straightforward to construct and navigate a different schedule on each GPU thread, the performance of the resulting technique can be very poor due to disparate pieces of codes executed by each GPU thread leading to full control divergence. In this paper, we demonstrate one application of SINECOSEQ by proposing a new GPU-friendly scheduler for accelerated concurrency testing (ACT), which is inspired by the recently proposed randomized scheduler of probabilistic concurrency testing (PCT). Compared to the state-of-the-art parallel PCT (PPCT) implementation on a twelve-core CPU, our proposal implemented on an NVIDIA Kepler K20c GPU card significantly speeds up schedule space exploration for eight multi-threaded applications and kernels drawn from the Phoenix and the PARSEC suites.

Bounded model checking based debugging solutions search for mutations of program expressions that produce the expected output for a currently failing test. However, the current localization tools are not regression aware: they do not use information from the passing tests in their localization formula. On the other hand, the current repair tools attempt to guarantee regression freedom: when provided with a set of passing tests, they guarantee that none of these tests can break due to the suggested repair patch, thereby constructing a large repair formula.

Generating invariants for loops is often a grueling obstacle in formal program verification. Researchers have employed methods from formal techniques based on abstract interpretation to test-driven dynamic analysis to tackle this problem. Even though powerful techniques for generating conjunctive invariants (invariants that employ only conjunction of terms) have been developed, disjunctive invariants have remained a sore thumb for formal techniques. In this paper, we propose a technique to transform certain category of loops, those that have a static iteration pattern, into loops that can be handled by conjunctive invariant generators. The key idea is to identify a static iteration pattern that distributes the disjunction in an invariant in a manner that can be captured by only conjunctive invariants. To broaden the scope of our algorithm, we also propose the idea of parametric verification, while attempting to verify specialized versions of the program where a subset of the input variables is instantiated with certain test-inputs. Note that parametric verification distinguishes it from program testing as testing requires all of its variables to be instantiated with test-inputs. We discuss our ideas on loops drawn from real programs to establish real-world applicability of our algorithms.

Acyclic path profiles are an indispensable tool geared towards multiple ends, with applications spanning from compiler optimizations to software engineering. Though such profiles provide an usable approximation to the program trace, many a times programmers are more interested in uncovering high-level interactions among a set of pertinent statements - not so much in the overall control-flow profile of the program. We propose a new profiling technique, Pertinent Path Profiling, which attempts to unveil such high-level interactions efficiently: given a control-flow graph and a set of pertinent basic-blocks (containing the relevant statements, Pertinent Path Profiling uniquely and efficiently identifies these high-level interactions, revealing execution demeanors that are otherwise difficult to discover via current control-flow profiling schemes. Additionally, if the number of pertinent basic-blocks is small, most of the time our algorithm yields much smaller path-frequency tables than those obtained by acyclic path profilers: if we are interested in a pertinent path profile with about 30% of the basic-blocks marked pertinent, most functions shrink their path-tables to about 15% of that of the acyclic path profiler. We illustrate a couple of possible applications of this new technology and provide experimental results on a set of benchmark programs to testify the utility of this new profiling technique.

Statistical bug isolation techniques attempt to capture a correlation of various program features (like predicates and profiled paths) for debugging. These techniques collect profile data for multiple executions, both with successful and faulty runs, and propose using various statistical tests to capture this correlation. In this paper, we explore the utility of program phases, a concept which is primarily used by computer architects to speed up architectural simulations, for statistical bug isolation. Program phases represent sets of execution intervals in a program's execution where the rates of architectural statistics like branch mispredictions, CPU/Memory usage and cache misses remain almost the same. We found multiple scenarios where coupling program phases with predicates achieves higher accuracy to bug localization than when predicates are used alone. We demonstrate the use of program phases for bug isolation by presenting experimental results and concrete case studies on medium-size programs, showing an improved ranking of the program points that are critical to debugging over when program phases are not used.

Speculative optimizations are increasingly becoming popular for improving program performance by allowing transformations that benefit frequently traversed program paths. Such optimizations are based on dataflow facts which are mostly true, though not always safe. Probabilistic dataflow analysis frameworks infer such facts about a program, while also providing the probability with which a fact is likely to be true. We propose a new Probabilistic Dataflow Analysis Framework which uses path profiles and information about the nesting structure of loops to obtain improved probabilities of dataflow facts.

The Ball-Larus path-profiling algorithm is an efficient technique to collect acyclic path frequencies of a program. However, longer paths — those extending across loop iterations — describe the runtime behaviour of programs better. We generalize the Ball-Larus profiling algorithm for profiling k-iteration paths — paths that can span up to to k iterations of a loop. We show that it is possible to number such k-iteration paths perfectly, thus allowing for an efficient profiling algorithm for such longer paths. We also describe a scheme for mixed-mode profiling: profiling different parts of a procedure with different path lengths. Experimental results show that k-iteration profiling is realistic.

We describe a library of parameterized VHDL models for various concurrent fault detection circuits and maintenance functions developed for simulation and synthesis of ASICs which support on-line testing and diagnostics in systems designed for high reliability and availability. Issues associated with the selection and modeling of the various online testing functions are also discussed.