Test-based automated program repair (TB-APR) techniques automatically fix buggy programs by relying on a failing test suite. This test suite serves a dual purpose: pinpointing bugs and evaluating the validity of potential patches. However, the effectiveness of TB-APR techniques in generating correct patches is highly dependent on the test suite utilized. The primary shortcoming of TB-APR techniques arises from the intrinsic incompleteness of test suites, resulting in a significant drawback: overfitting, i.e., the generation of ‘overfitted patches’, patches that pass the given test suites but fail to repair the subject program correctly regarding its more general intended behavior.To address this challenge, we present a novel technique designed to enhance the effectiveness of TB-APR methods by automatically generating test suites tailored for program repair. Unlike prior TB-APR techniques, it is rooted in the recognition that edge cases that invalidate overfitted patches play a pivotal role in guiding the repair process away from incorrect solutions. This technique leverages formal specifications and bounded verification to evaluate candidate patches and transforms the counterexamples (CEs) obtained from verifying candidate patches into tests for program repair. The efficacy of iteratively using such CEs as tests for TB-APR is substantiated by Iter-T our implementation of this technique for Java programs and JML specifications, evaluated on a benchmark of 717 buggy Java programs drawn from the APR literature. By progressively constructing test suites exclusively from CEs of overfitted candidate patches, Iter-T increases the odds of fixing a bug by about 58% compared to the originally provided test suites. Moreover, in cases where a TB-APR tool repairs a program using its original suite, employing CEs alone as test suites reduces the median time required to generate a correct patch by 42%. Remarkably, the generated CEs-based test suites are very small, accomplishing these results with only 2.4 tests on average.

Differential testing is a highly effective technique for automatically detecting software bugs and vulnerabilities when the specifications involve an analysis over multiple executions simultaneously. Differential fuzzing, in particular, operates as a guided randomized search, aiming to find (similar) inputs that lead to a maximum difference in software outputs or their behaviors. However, fuzzing, as a dynamic analysis, lacks any guarantees on the absence of bugs: from a differential fuzzing campaign that has observed no bugs (or a minimal difference), what is the risk of observing a bug (or a larger difference) if we run the fuzzer for one or more steps?This paper investigates the application of Extreme Value Theory (EVT) to address the risk of missing or underestimating bugs in differential fuzzing. The key observation is that differential fuzzing as a random process resembles the maximum distribution of observed differences. Hence, EVT, a branch of statistics dealing with extreme values, is an ideal framework to analyze the tail of the differential fuzzing campaign to contain the risk. We perform experiments on a set of real-world Java libraries and use differential fuzzing to find information leaks via side channels in these libraries. We first explore the feasibility of EVT for this task and the optimal hyperparameters for EVT distributions. We then compare EVT-based extrapolation against baseline statistical methods like Markov’s as well as Chebyshev’s inequalities, and the Bayes factor. EVT-based extrapolations outperform the baseline techniques in 14.3% of cases and tie with the baseline in 64.2% of cases. Finally, we evaluate the accuracy and performance gains of EVT-enabled differential fuzzing in real-world Java libraries, where we reported an average saving of tens of millions of bytecode executions by an early stop.

Specifications are an essential component of software development, and getting specifications right, especially formal specifications, can be very challenging. While the use of tools such as model finders and model checkers can be very effective for specification analysis through property checking, researchers have also realized that by the explicit provision of wanted and unwanted specification scenarios, in the style of testing in programs, specification assessment can be significantly enhanced. Thus, various testing and test generation techniques have been recently proposed for assessing formal specifications.In this paper, we present such a specification testing approach, in the form of a novel combinatorial testing technique for Alloy specifications, called COMBA. COMBA implements an automated partitioning of the state space of Alloy specifications solely based on elements of the specification (thus not requiring user intervention), and defines a family of test criteria, that indicate how such partitions are to be covered. The coverage of the partitions is defined by a family of combinatorial criteria that, given a positive integer t, require to cover through test cases all feasible t-uples of elements from different partitions. Finally, COMBA introduces an efficient algorithm to generate test cases that satisfy the combinatorial criteria. By leveraging on incremental SAT solving techniques, COMBA achieves significantly better performance in test generation.We experimentally assess COMBA against existing test generation approaches for Alloy, using a large number of specifications with known errors. The results show that COMBA(with t = 2) runs faster, produces smaller test suites, and finds a significantly larger number of real bugs than related approaches.

In this article, we empirically study the suitability of tests as acceptance criteria for automated program fixes, by checking patches produced by automated repair tools using a bug-finding tool, as opposed to previous works that used tests or manual inspections. We develop a number of experiments in which faulty programs from IntroClass , a known benchmark for program repair techniques, are fed to the program repair tools GenProg, Angelix, AutoFix, and Nopol, using test suites of varying quality, including those accompanying the benchmark. We then check the produced patches against formal specifications using a bug-finding tool. Our results show that, in the studied scenarios, automated program repair tools are significantly more likely to accept a spurious program fix than producing an actual one. Using bounded-exhaustive suites larger than the originally given ones (with about 100 and 1,000 tests) we verify that overfitting is reduced but (a) few new correct repairs are generated and (b) some tools see their performance reduced by the larger suites and fewer correct repairs are produced. Finally, by comparing with previous work, we show that overfitting is underestimated in semantics-based tools and that patches not discarded using held-out tests may be discarded using a bug-finding tool.

Abstract Bounded exhaustive input generation (BEG) is an effective approach to reveal software faults. However, existing BEG approaches require a precise specification of the valid inputs, i.e., a , that must be provided by the user. Writing s for BEG is challenging and time consuming, and they are seldom available in software. In this paper, we introduce , an efficient approach that employs routines from the API of the software under test to perform BEG. Like API-based test generation approaches, creates sequences of calls to methods from the API, and executes them to generate inputs. As opposed to existing BEG approaches, does not require a to be provided by the user. To make BEG from the API feasible, implements three key pruning techniques: (i) discarding test sequences whose execution produces exceptions violating API usage rules, (ii) state matching to discard test sequences that produce inputs already created by previously explored test sequences, and (iii) the automated identification and use of a subset of methods from the API, called builders, that is sufficient to perform BEG. Our experimental assessment shows that ’s efficiency and scalability is competitive with existing BEG approaches, without the need for s. We also show that can assist the user in finding flaws in s, by (automatically) comparing inputs generated by with those generated from a . Using this approach, we revealed several errors in s taken from the assessment of related tools, demonstrating the difficulties of writing precise s for BEG.

Lazy initialization enables symbolic execution for programs with heap-allocated inputs. It starts the program execution with a symbolic heap and concretizes it on demand as the program accesses it. However, the main challenge of lazy initialization is efficiently determining whether the current symbolic heap becomes infeasible with respect to the program’s precondition. Pruning infeasible heaps is crucial to avoid significant runtime overhead and false alarms.In this paper, we propose PLI (Precise Lazy Initialization), an approach that precisely decides whether there exists a concretization of the current symbolic heap that satisfies the program’s precondition. Unlike previous approaches, PLI also takes into account the constraints in the path condition to determine the feasibility of the current symbolic heap. Furthermore, PLI allows preconditions to be specified as standard operational predicates for concrete structures, eliminating the need for additional specifications tailored to symbolic heaps.In our empirical evaluation, PLI demonstrated comparable performance to existing lazy approaches while reducing the number of explored paths by 43% (all infeasible) and eliminating all false alarms in the analysis. Moreover, PLI exhibited faster execution and better scalability compared to "eager" (enumeration-based) approaches, achieving a 67% reduction in explored paths.

Postconditions are predicates that specify the intended behavior of a program by capturing properties about the program state when the program finishes its execution. Although postconditions can help to improve many software reliability analyses, they are seldom found accompanying source code. Thus, tools that assist developers in specifying postconditions are useful. This tool demo paper presents EvoSpex, a tool based on evolutionary computation that automatically infers postconditions of Java methods. Given a target Java method and a test suite for it, our tool executes the test suite to obtain valid pre/post state pairs for the method under analysis. Then, these pairs are mutated to obtain (allegedly) invalid ones, and finally a postcondition assertion characterizing the current method behavior is produced, by using an evolutionary algorithm that searches for an assertion that is satisfied by the valid pre/post state pairs and leaves out the invalid ones. EvoSpex implements a classic genetic algorithm that explores the space of candidate postconditions over a JML-like specification language. The algorithm is guided by a fitness function that aims at precisely capturing the valid state pairs, rejecting the invalid ones, and that also favors more succinct assertions.

Alloyis a formal specification language, which despite featuring a simple syntax and relational semantics, is very expressive and supports efficient automated specification analysis, based on SAT solving. While the language is sufficiently expressive to accommodate bothstaticanddynamicproperties of systems within specifications, the latter kind of properties require intricate, ad-hoc, constructions to encode system executions. Thus, extensions to the language have been proposed, that internalize these encodings and provide analysis techniques, specifically tailored to properties of executions. In this paper we study two particular extensions toAlloythat incorporate elements for the specification of properties of executions. These areDynAlloy, whose syntax and semantics are inspired by dynamic logic, andElectrum, based on linear-time temporal logic and inspired by languages such asTLA+. We analyze and compare the syntactic characteristics of the languages, their corresponding expressiveness, and the effectiveness and efficiency of their associated analysis tools. The comparison is based on a set ofAlloyspecifications that are taken from the literature and demand dynamic behavior analysis, including anAlloymodel of the Chord ring-maintenance protocol, that drives our qualitative comparison of the notations.

Symbolic execution allows one to systematically explore program paths by executing programs on symbolic inputs, and constructing path conditions that can be analyzed using constraint solving. When programs handle heap-allocated structures, and executions are assumed to begin in states satisfying a property like a precondition or invariant, symbolic execution not only needs to maintain path conditions, but also partially concrete heaps. Partially concrete heaps are increasingly concretized as symbolic execution progresses, and their feasibility (i.e., deciding whether they can be extended to fully concrete structures that satisfy the precondition) needs to be determined, to deem a path realizable and continue execution. This latter task generally requires the manual provision of routines to check the feasibility of partially concrete structures, which are often imprecise (e.g., do not detect all infeasible structures), and increase the cost of symbolic execution. In this paper, we improve the above situation by proposing an automated machine learning technique for determining whether a partially symbolic structure can be extended into a concrete structure satisfying a given invariant. Our approach does not require additional, manually provided routines for checking structure feasibility. It is based on recognizing feasible/infeasible partially symbolic structures by using a neural network, which is trained with automatically generated partially symbolic structures. These structures can be obtained by either symbolically executing the assumed invariant, or by generating and mutating structures using assumed-correct building routines. Our experiments, based on a benchmark of heap-allocated data structures of varying complexities, show that by incorporating our learned symbolic invariants as a pruning mechanism within Symbolic PathFinder, path infeasibility detection is greatly improved, as well as symbolic execution running times.

Automatic Program Repair (APR) is a practical research topic that studies techniques to automatically repair programs to fix bugs. Most existing APR techniques are designed for imperative programming languages, such as C and Java, and rely on analyzing correct and incorrect executions of programs to identify and repair suspicious statements.

Automated program repair (APR) techniques have shown great success in automatically finding fixes for programs in programming languages such as C or Java. In this work, we focus on repairing formal specifications, in particular for the Alloy specification language. As opposed to most APR tools, our approach to repair Alloy specifications, named ICEBAR, does not use test-based oracles for patch assessment. Instead, ICEBAR relies on the use of property-based oracles, commonly found in Alloy specifications as predicates and assertions. These property-based oracles define stronger conditions for patch assessment, thus reducing the notorious overfitting issue caused by using test-based oracles, typically observed in APR contexts. Moreover, as assertions and predicates are inherent to Alloy, whereas test cases are not, our tool is potentially more appealing to Alloy users than test-based Alloy repair tools.

Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs’ fields on demand, as the program under analysis accesses them. However, when the program’s assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE’s performance. repOK can only decide the feasibility of fully concrete structures, and thus previous work relied on manually crafted specifications designed to decide the (in)validity of partially symbolic inputs, to avoid producing spurious symbolic structures. However, these additional specifications require significant further effort from the developers.

Abstract Software model checkers are able to exhaustively explore different bounded program executions arising from various sources of non-determinism. These tools provide statements to produce non-deterministic values for certain variables, thus forcing the corresponding model checker to considerallpossible values for these during verification. While these statements offer an effective way of verifying programs handling basic data types and simple structured types, they are inappropriate as a mechanism for nondeterministic generation of pointers, favoring the use of insertion routines to produce dynamic data structures when verifying, via model checking, programs handling such data types. We present a technique to improve model checking of programs handling heap-allocated data types, by taming the explosion of candidate structures that can be built when non-deterministically initializing heap object fields. The technique exploits precomputedrelational bounds, that disregard values deemed invalid by the structure’s type invariant, thus reducing the state space to be explored by the model checker. Precomputing the relational bounds is a challenging costly task too, for which we also present an efficient algorithm, based on incremental SAT solving. We implement our approach on top of the bounded model checker, and show that, for a number of data structures implementations, we can handle significantly larger input structures and detect faults that is unable to detect.

The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in the program repair of imperative languages, there is a dearth of repair techniques for declarative languages. This paper presents BeAFix, an automated repair technique for faulty models written in Alloy, a declarative language based on first-order relational logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet scalable, exploration of the spaces of fix candidates and a formally rigorous, sound pruning of such spaces. Moreover, different from the state-of-the-art in Alloy automated repair, that relies on the availability of unit tests, BeAFix does not require tests and can work with assertions that are naturally used in formal declarative languages. Our experience with using BeAFix to repair thousands of real-world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art.

Software reliability is a primary concern in the construction of software, and thus a fundamental component in the definition of software quality. Analyzing software reliability requires a specification of the intended behavior of the software under analysis, and at the source code level, such specifications typically take the form of assertions. Unfortunately, software many times lacks such specifications, or only provides them for scenario-specific behaviors, as assertions accompanying tests. This issue seriously diminishes the analyzability of software with respect to its reliability. In this paper, we tackle this problem by proposing a technique that, given a Java method, automatically produces a specification of the method's current behavior, in the form of postcondition assertions. This mechanism is based on generating executions of the method under analysis to obtain valid pre/post state pairs, mutating these pairs to obtain (allegedly) invalid ones, and then using a genetic algorithm to produce an assertion that is satisfied by the valid pre/post pairs, while leaving out the invalid ones. The technique, which targets in particular methods of reference-based class implementations, is assessed on a benchmark of open source Java projects, showing that our genetic algorithm is able to generate post-conditions that are stronger and more accurate, than those generated by related automated approaches, as evaluated by an automated oracle assessment tool. Moreover, our technique is also able to infer an important part of manually written rich postconditions in verified classes, and reproduce contracts for methods whose class implementations were automatically synthesized from specifications.

Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not "executed," but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion, and instances that do satisfy the assertion to find suspicious expressions in the input model. The experimental results show that FLACK is efficient (can handle complex, real-world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions).

This paper describes BeAFix, a tool for automated repair of faulty Alloy models. The tool builds upon the Alloy Analyzer, the analysis tool for Alloy. It generates repair candidates by mutating a faulty Alloy model, and employs a bounded-exhaustive approach to traverse the space of repair candidates. Since BeAFix’s mutation operators make the space of repair candidates to quickly grow, the tool supports some sound pruning techniques, that allow it to fix Alloy models with more than one faulty line or expression. Additionally, BeAFix does not require tests as a patch acceptance criterion. Although BeAFix supports tests as oracles, our tool is also able to leverage property-based oracles, which are more commonly found in Alloy models in the form of predicate satisfiability and assertion validity checks.A video demonstration of BeAFix can be found at https://youtu.be/5RG40SmlFXQ. The tool’s binaries and further details about its usage, can all be found at https://sites.google.com/view/beafixevaluation/beafix. The tool is also available in a public archive at https://doi.org/10.5281/zenodo.5296466.

Fault localization can help developers identify buggy statements or expressions in programs. Existing fault localization techniques are often designed for imperative programs (e.g., C and Java) and rely on tests to compare correct and incorrect execution traces to identify suspicious statements. In this demo paper, we present FLACK, a tool to automatically locate faults for models written in Alloy, a declarative language where the models are not executed but instead converted into a logical formula and solved using a SAT solver. FLACK takes as input an Alloy model that violates some assertions and returns a ranked list of suspicious expressions contributing to the violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion and instances that do satisfy the assertion to find suspicious expressions in the input model. An experiment with 157 Alloy models with various bugs shows the efficiency and accuracy of FLACK in localizing the causes of these bugs. FLACK and its evaluation benchmark and results can be downloaded from https://github.com/guolong-zheng/flack. The video demonstration is available at https://youtu.be/FKa2ohqIUms.

Various approaches to software analysis (e.g. test input generation, software model checking) require engineers to (manually) identify a subset of a module’s methods in order to drive the analysis. Given a module to be analyzed, engineers typically select a subset of its methods to be considered as object builders to define a so-called driver , that will be used to automatically build objects for analysis, e.g., combining them non-deterministically, randomly, etc. This requires a careful inspection of the module and its API, since both the relative exhaustiveness of the analysis (leaving important methods out may systematically avoid generating different objects), as well as its efficiency (the different bounded combinations of methods grows exponentially as the number of methods increases), are affected by the selection. We propose an approach for automatically selecting a set of builders from a module’s API, based on an evolutionary algorithm that favors sets of methods whose combinations lead to producing larger sets of objects. The algorithm also takes into account other characteristics of these sets of methods, trying to prioritize the selection of methods with less and simpler parameters. As the implementation of this evolutionary mechanism requires in principle handling and comparing large sets of objects, and this grows very quickly both in terms of space and running times, we employ an abstraction of sets of objects, called field extensions, that involves using the field values of the objects in the set instead of the actual objects, and enables us to effectively implement our mechanism. An experimental assessment on a benchmark of stateful classes shows that our approach can automatically identify sets of builders that are sufficient (can be used to create any instance of the module) and minimal (do not contain superfluous methods), in a reasonable time.

peer reviewed

Field-exhaustive testing is a testing criterion suitable for object-oriented code over complex, heap-allocated, data structures. It requires test suites to contain enough test inputs to cover all feasible values for the object's fields within a certain scope (input-size bound). While previous work shows that field-exhaustive suites can be automatically generated, the generation technique required a formal specification of the inputs that can be subject to SAT-based analysis. Moreover, the restriction of producing all feasible values for inputs' fields makes test generation costly. In this paper, we deal with field coverage as testing criteria that measure the quality of a test suite in terms of coverage and mutation score, by examining to what extent the values of inputs' fields are covered. In particular, we consider field coverage in combination with test generation based on symbolic execution to produce underapproximations of field-exhaustive suites, using the Symbolic Pathfinder tool. To underapproximate these suites we use tranScoping, a technique that estimates characteristics of yet to be run analyses for large scopes, based on data obtained from analyses performed in small scopes. This provides us with a suitable condition to prematurely stop the symbolic execution. As we show, tranScoping different metrics regarding field coverage allows us to produce significantly smaller suites using a fraction of the generation time. All this while retaining the effectiveness of field exhaustive suites in terms of test suite quality.

In goal-oriented requirements engineering approaches, conflict analysis has been proposed as an abstraction for risk analysis. Intuitively, given a set of expected goals to be achieved by the system-to-be, a conflict represents a subtle situation that makes goals diverge, i.e., not be satisfiable as a whole. Conflict analysis is typically driven by the identify-assess-control cycle, aimed at identifying, assessing and resolving conflicts that may obstruct the satisfaction of the expected goals. In particular, the assessment step is concerned with evaluating how likely the identified conflicts are, and how likely and severe are their consequences.

Summary Formal requirements specifications, eg, software cost reduction (SCR) specifications, are challenging to analyse using automated techniques such as model checking. Since such specifications are meant to capturerequirements, they tend to refer to real‐world magnitudes often characterized through variables over large domains. At the same time, they feature a high degree of nondeterminism, as opposed to other analysis contexts such as (sequential) program verification. This makes model checking of SCR specifications difficult even for symbolic approaches. Moreover, automated abstraction refinement techniques such as counterexample guided abstraction refinement fail in many cases in this context, since the concrete state space is typically large, and reaching specific states of interest may require complex executions involving many different states, causing these approaches to perform many abstraction refinements, and making them ineffective in practice. In this paper, an approach to tackle the above situation, through a 2‐stage abstraction, is presented. The specification is first relaxed, by disregarding the constraints imposed in the specification by physical laws or by the environment, before being fed to a counterexample guided abstraction refinement procedure, tailored to SCR. By relaxing the original specification, shorter spurious counterexamples are produced, favouring the abstraction refinement through the introduction of fewer abstraction predicates. Then, when a counterexample is concretizable with respect to the relaxed (concrete) specification but it is spurious with respect to the original specification, an efficient though incomplete refinement step is applied to the constraints, to cause the removal of the spurious case. This approach is experimentally assessed, comparing it with related techniques in the verification of properties and in automated test case generation, using various SCR specifications drawn from the literature as case studies. The experiments show that this new approach runs faster and scales better to larger, more complex specifications than related techniques.

We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy.

It is so inconceivable to debug a program without testing it that these two words are used nearly interchangeably. Yet we argue that using the concept of relative correctness we can indeed remove a fault from a program and prove that the fault has been removed, by proving that the new program is more correct than the original. This is a departure from the traditional roles of proving and testing methods, whereby static proof methods are applied to a correct program to prove its correctness, and dynamic testing methods are applied to an incorrect program to expose its faults.

We present a testing approach for object oriented programs, which encompasses a testing criterion and an automated test generation technique. The criterion, that we call field-exhaustive testing, requires a user-provided limit n on the size of data domains, and is based on the idea of considering enough inputs so as to exhaustively cover the extension of class fields, within the limit n. Intuitively, the extension of a field f is the binary relation established between objects and their corresponding values for field f, in valid instances. Thus, a suite S is field-exhaustive if whenever a field f relates an object o with a value v (i.e., o.f = v) within a valid instance I of size bounded by n, then S contains at least one input I' covering such relationship, i.e., o must also be part of I', and o.f = v must hold in I'. Our test generation technique uses incremental SAT solving to produce small field-exhaustive suites: field-exhaustiveness can be achieved with a suite containing at most # F x n2 inputs, where # F is the number of fields in the class under test.

Lazy Initialization (LI) allows symbolic execution to effectively deal with heap-allocated data structures, thanks to a significant reduction in spurious and redundant symbolic structures. Bounded lazy initialization (BLI) improves on LI by taking advantage of precomputed relational bounds on the interpretation of class fields in order to reduce the number of spurious structures even further. In this paper we present bounded lazy initialization with SAT support (BLISS), a novel technique that refines the search for valid structures during the symbolic execution process. BLISS builds upon BLI, extending it with field bound refinement and satisfiability checks. Field bounds are refined while a symbolic structure is concretized, avoiding cases that, due to the concrete part of the heap and the field bounds, can be deemed redundant. Satisfiability checks on refined symbolic heaps allow us to prune these heaps as soon as they are identified as infeasible, i.e., as soon as it can be confirmed that they cannot be extended to any valid concrete heap. Compared to LI and BLI, BLISS reduces the time required by LI by up to four orders of magnitude for the most complex data structures. Moreover, the number of partially symbolic structures obtained by exploring program paths is reduced by BLISS by over 50 percent, with reductions of over 90 percent in some cases (compared to LI). BLISS uses less memory than LI and BLI, which enables the exploration of states unreachable by previous techniques.

We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes.

SUMMARY While the effectiveness of bounded exhaustive test suites increases as one increases the scope for the bounded exhaustive generation, both the time for test generation and the time for test execution grow exponentially with respect to the scope. In this article, a set of techniques for reducing the time for bounded exhaustive testing, by either reducing the generation time or reducing the obtained bounded exhaustive suites, is proposed. The representation invariant of the software under test's input, implemented as a repOK routine, is exploited for these reductions in two ways: (i) to factor out separate representation invariants for disjoint structures of the inputs; and (ii) to partition valid inputs into equivalence classes, according to how these exercise the repOK code. The first is used in order to split the test input generation process, as disjoint substructures can be independently generated. The second is used in order to reduce the size of a bounded exhaustive test suite, by removing from the suite those tests that are equivalent to some tests already present in the suite. Copyright © 2014 John Wiley & Sons, Ltd.

Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. Dynamite is an extension of PVS that embeds a complete calculus for Alloy. It also includes extensions to PVS that allow one to improve the proof effort by, for instance, automatically analyzing new hypotheses with the aid of the Alloy Analyzer. Since PVS sequents may get cluttered with unnecessary formulas, we use the Alloy unsat-core extraction feature in order to refine proof sequents. An internalization of Alloy's syntax as an Alloy specification allows us to use the Alloy Analyzer for producing witnesses for proving existentially quantified formulas. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer for early error detection, sequent refinement, and witness generation.

We present a novel and general technique for automated test generation that combines tight bounds with incremental SAT solving. The proposed technique uses incremental SAT to build test suites targeting a specific testing criterion, amongst various black-box and white-box criteria. As our experimental results show, the combination of tight bounds with incremental SAT, and the testing criterion driven approach implemented in our prototype tool FAJITA, enable us to effectively generate test suites for container classes with rich contracts, more efficiently than other state-of-the-art tools.

In this article we present a novel technique for automated parallel bug-finding based on the sequential analysis tool TACO. TACO is a tool based on SAT-solving for efficient bug-finding in Java code with rich class invariants. It prunes the SAT-solver's search space by introducing precise symmetry-breaking predicates and bounding the relational semantics of Java class fields. The bounds computed by TACO generally include a substantial amount of nondeterminism; its reduction allows us to split the original analysis into disjoint subproblems. We discuss the soundness and completeness of the decomposition. Furthermore, we present experimental results showing that MUCHO-TACO, our tool which implements this technique, yields significant speed-ups over TACO on commodity cluster hardware.

We present a novel approach for parallel analysis of models written in Alloy, a declarative extension of first-order logic based on relations. The Alloy language is supported by the fully automatic Alloy Analyzer, which translates models into propositional formulas and uses off-the-shelf SAT technology to solve them. Our key insight is that the underlying constraint satisfaction problem can be split into subproblems of lesser complexity by using ranges of candidate solutions, which partition the space of all candidate solutions. Conceptually, we define a total ordering among the candidate solutions, split this space of candidates into ranges, and let independent SAT searches take place within these ranges' endpoints. Our tool, Ranger, embodies our insight. Experimental evaluation shows that Ranger provides substantial speedups (in several cases, superlinear ones) for a variety of hard-to-solve Alloy models, and that adding more hardware reduces analysis costs almost linearly.

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present Translation of Annotated COde (TACO), a prototype tool which implements a novel, general, and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models and, on the other hand, allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to an improvement of the efficiency of the analysis of orders of magnitude, compared to the noninstrumented SAT--based analysis. We show that in some cases our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking, or SMT-solving.

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques.

DynAlloy is an extension of Alloy to support the definition of actions and the specification of assertions regarding execution traces. In this article we show how we can extend the Alloy tool so that DynAlloy specifications can be automatically analyzed in an efficient way. We also demonstrate that DynAlloy's semantics allows for a sound technique that we call program atomization , which improves the analyzability of properties regarding execution traces by considering certain programs as atomic steps in a trace. We present the foundations, case studies, and empirical results indicating that the analysis of DynAlloy specifications can be performed efficiently.

We present DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems using actions. Actions allow us to appropriately specify dynamic properties, particularly, properties regarding execution traces, in the style of dynamic logic specifications.We extend Alloy's syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra's weakest liberal precondition. These assertions, defined in terms of actions, allow us to easily express properties regarding executions, favoring the separation of concerns between the static and dynamic aspects of a system specification.We also extend the Alloy tool in such a way that DynAlloy specifications are also automatically analyzable, as standard Alloy specifications. We present the foundations, two case-studies, and empirical results evidencing that the analysis of DynAlloy specifications can be performed efficiently.

We introduce a strategy for the verification of relational specifications based on the analysis of monotonicity of variables within formulas. By comparing with the Alloy Analyzer, we show that for a relevant class of problems this technique drastically outperforms analysis of the same problems using SAT-solvers, while consuming a fraction of the memory SAT-solvers require.

We study a number of restrictions associated with the first-order relational specification language Alloy. The main shortcomings we address are:---the lack of a complete calculus for deduction in Alloy's underlying formalism, the so called relational logic,---the inappropriateness of the Alloy language for describing (and analyzing) properties regarding execution traces.The first of these points was not regarded as an important issue during the genesis of Alloy, and therefore has not been taken into account in the design of the relational logic. The second point is a consequence of the static nature of Alloy specifications, and has been partly solved by the developers of Alloy; however, their proposed solution requires a complicated and unstructured characterization of executions.We propose to overcome the first problem by translating relational logic to the equational calculus of fork algebras . Fork algebras provide a purely relational formalism close to Alloy, which possesses a complete equational deductive calculus. Regarding the second problem, we propose to extend Alloy by adding actions . These actions, unlike Alloy functions, do modify the state. Much the same as programs in dynamic logic, actions can be sequentially composed and iterated, allowing them to state properties of execution traces at an appropriate level of abstraction.Since automatic analysis is one of Alloy's main features, and this article aims to provide a deductive calculus for Alloy, we show that:---the extension hereby proposed does not sacrifice the possibility of using SAT solving techniques for automated analysis,---the complete calculus for the relational logic is straightforwardly extended to a complete calculus for the extension of Alloy.

The relational calculus MU/sub 2/, presented in de Roever's dissertation as a framework for describing and proving properties of programs, was conjectured by David Park to be complete. In this paper we confirm Park's conjecture.

Since the main themes at the Helena Rasiowa memorial were algebra, logic and computer science, we will present a survey of results on fork algebras from these points of view. In this paper we study fork algebras from the points of view of their algebraic and logical properties and applications. These results will prove to be essential, in a future work, for the definition of a wide-spectrum calculus for program construction.