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.
The theory of institutions, introduced by Goguen and Burstall in 1984, can be thought of as an abstract formulation of model theory. This theory has been shown to be particularly useful in computer ...science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, José Meseguer among them, who, in 1989, presented General Logics, wherein the model theoretical view of institutions is complemented by providing (categorical) structures supporting the proof theory of any given logic. In other words, Meseguer introduced the notion of proof calculus as a formalisation of syntactical deduction, thus “implementing” the entailment relation of a given logic. In this paper we follow the approach initiated by Goguen and introduce the concept of Satisfiability Calculus. This concept can be regarded as the semantical counterpart of Meseguer’s notion of proof calculus, as it provides the formal foundations for those proof systems that resort to model construction techniques to prove or disprove a given formula, thus “implementing” the satisfiability relation of an institution. These kinds of semantic proof methods have gained a great amount of interest in computer science over the years, as they provide the basic means for many automated theorem proving techniques.
Goal oriented methods have been successfully employed for eliciting and elaborating software requirements. When goals are assigned to an agent, they have to be operationalised: the agent’s operations ...have to be refined, by equipping them with appropriate enabling and triggering conditions, so that the goals are fulfilled. Goal operationalisation generally demands a significant effort of the engineer. Although there exist approaches that tackle this problem, they are either informal or at most semi automated, requiring the engineer to assist in the process. In this paper, we present an approach for goal operationalisation that automatically computes required preconditions and required triggering conditions for operations, so that the resulting operations establish the goals. The process is iterative, is able to deal with safety goals and particular kinds of liveness goals, and is based on the use of interpolation and SAT solving.
Fuzzing class specifications Molina, Facundo; d'Amorim, Marcelo; Aguirre, Nazareno
2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE),
05/2022
Conference Proceeding
Odprti dostop
Expressing class specifications via executable constraints is important for various software engineering tasks such as test generation, bug finding and automated debugging, but developers rarely ...write them. Techniques that infer specifications from code exist to fill this gap, but they are designed to support specific kinds of assertions and are difficult to adapt to support different assertion languages, e.g., to add support for quantification, or additional comparison operators, such as membership or containment.
To address the above issue, we present SpecFuzzer, a novel technique that combines grammar-based fuzzing, dynamic invariant detection, and mutation analysis, to automatically produce class specifications. SpecFuzzer uses: (i) a fuzzer as a generator of candidate assertions derived from a grammar that is automatically obtained from the class definition; (ii) a dynamic invariant detector -Daikon- to filter out assertions invalidated by a test suite; and (iii) a mutation-based mechanism to cluster and rank assertions, so that similar constraints are grouped and then the stronger prioritized. Grammar-based fuzzing enables SpecFuzzer to be straightforwardly adapted to support different specification languages, by manipulating the fuzzing grammar, e.g., to include additional operators.
We evaluate our technique on a benchmark of 43 Java methods employed in the evaluation of the state-of-the-art techniques GAssert and EvoSpex. Our results show that SpecFuzzer can easily support a more expressive assertion language, over which is more effective than GAssert and EvoSpex in inferring specifications, according to standard performance metrics.
In object-oriented design, class specifications are primarily used to express properties describing the intended behavior of the class methods and constraints on class' objects. Although the presence ...of these specifications is important for various software engineering tasks such as test generation, bug finding and automated debugging, developers rarely write them. In this tool demo we present the details of SPEcFuzZER, a tool that aims at alleviating the problem of writing class specifications by using a combination of grammar-based fuzzing, dynamic invariant detection and mutation analysis to auto-maticallyautomatically infer specifications for Java classes. Given a class under analysis, SPEcFuzZER uses (i) a generator of candidate assertions derived from a grammar automatically extracted from the class; (ii) a dynamic invariant detector -Daikon- in order to discard the assertions invalidated by a test suite; and (iii) a mutation-based mechanism to cluster and rank assertions, so that similar constraints are grouped together and the stronger assertions are prioritized. The tool is available on GitHub at https://github.com/facumolina/specfuzzer, and the demo video can be found on YouTube: https://youtu.be/IfakNCbzOUg.
Bounded exhaustive testing is a very effective technique for bug finding, which proposes to test a given program under all valid bounded inputs, for a bound provided by the developer. Existing ...bounded exhaustive testing techniques require the developer to provide a precise specification of the valid inputs. Such specifications are rarely present as part of the software under test, and writing them can be costly and challenging.
To address this situation we propose BEAPI, a tool that given a Java class under test, generates a bounded exhaustive set of objects of the class solely employing the methods of the class, without the need for a specification. BEAPI creates sequences of calls to methods from the class' public API, and executes them to generate inputs. BEAPI implements very effective pruning techniques that allow it to generate inputs efficiently.
We experimentally assessed BEAPI in several case studies from the literature, and showed that it performs comparably to the best existing specification-based bounded exhaustive generation tool (Korat), without requiring a specification of the valid inputs.
Alloy is 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 both static and dynamic properties 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 to Alloy that incorporate elements for the specification of properties of executions. These are DynAlloy , whose syntax and semantics are inspired by dynamic logic, and Electrum , based on linear-time temporal logic and inspired by languages such as TLA+ . 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 of Alloy specifications that are taken from the literature and demand dynamic behavior analysis, including an Alloy model of the Chord ring-maintenance protocol, that drives our qualitative comparison of the notations.
EvoSpex Molina, Facundo; Ponzio, Pablo; Aguirre, Nazareno ...
2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE),
05/2021
Conference Proceeding
Odprti dostop
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.
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.
Efficient Analysis of DynAlloy Specifications Frias, Marcelo F.; Lopez Pombo, Carlos G.; Galeotti, Juan P. ...
ACM transactions on software engineering and methodology,
12/2007, Letnik:
17, Številka:
1
Journal Article
Recenzirano
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.
PDF
