Pietro Braione

dblp:07/4464 · DBLP profile ↗
← Back
14ranked-venue papers
9as first author
4since 2021 · last 2026
0000-0001-9307-6781ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 11 · 7 first-author · 4 since 2021Computer networks · 1 · 1 first-authorHuman-computer interaction and ubiquitous computing · 1
YearPublicationVenuePosition
2026 Path-Optimal Symbolic Execution of Heap-Manipulating Programs
Pietro Braione, Giovanni Denaro, Luca Guglielmo
SANER1
2025 Automated Test Generation for Integration Testing
abstract
Integration testing is a fundamental step of the software development process. Due to the high costs, testers may like to automatically generate the test cases, but unfortunately current test generators are designed for unit testing or system testing, while they are generally ill-suited for integration testing. In this paper, we discuss the challenges of generating test cases for integration testing, and the limitations of current test generators thereby. We elaborate on a novel approach to automatically generating test cases for integration testing, and report initial evidence in support of our approach.
Elson Kurian, Giovanni Denaro, Pietro Braione, Luca Guglielmo
AST3
2023 Automatically generating test cases for safety-critical software via symbolic execution
Elson Kurian, Daniela Briola, Pietro Braione, Giovanni Denaro
J. Syst. Softw.3
2022 About the special issue on: "Distributed Complex Systems: Governance, Engineering, and Maintenance"
abstract
Abstract The volume at hand presents the Special Issue on “Distributed Complex Systems: Governance, Engineering, and Maintenance”. The Special Issue has been originally conceived within the context of the 2nd International Workshop on Governing Adaptive and Unplanned Systems of Systems (GAUSS 2020), one of the co‐located events of the 31st International Symposium on Software Reliability Engineering (ISSRE 2020). The authors of the best papers at GAUSS 2020 have been invited to submit an extended version of their previous work. In addition, the editors opened the submission also to all the other researches working on technical and managerial solution for governing Distributed Complex Systems. Ultimate objective of the editors with this Special Issue is to promote discussions focusing on anticipating, mitigating, or reacting to scenarios that were unplanned or under‐specified at design time.
Pietro Braione, Daniela Briola, Guglielmo De Angelis, Francesco Gallo, Francesco Poggi, Giovanni Quattrocchi
J. Softw. Evol. Process.1
2020 Facilitating program performance profiling via evolutionary symbolic execution
abstract
Summary Performance profiling can benefit from test cases that hit high‐cost executions of programs. In this paper, we investigate the problem of automatically generating test cases that trigger the worst‐case execution of programs and propose a novel technique that solves this problem with an unprecedented combination of symbolic execution and evolutionary algorithms. Our technique, which we refer to as ‘Evolutionary Symbolic Execution’, embraces the execution cost of the program paths as the fitness function to pursue the worst execution. It defines an original set of evolutionary operators, based on symbolic execution, which suitably sample the possible program paths to make the search process effective. Specifically, our technique defines a memetic algorithm that (i) incrementally evolves by steering symbolic execution to traverse new program paths that comply with execution conditions combined and refined from the currently collected worse program paths and (ii) periodically applies local optimizations to the execution conditions of the worst currently identified program path to further speed up the identification of the worst path. We report on a set of initial experiments indicating that our technique succeeds in generating good worst‐case test cases for programs with which existing approaches cannot cope. Also, we show that, as far as the problem of generating worst‐case test cases is concerned, the distinguishing evolutionary operators based on symbolic execution that we define in this paper are more effective than traditional operators that directly manipulate the program inputs.
Andrea Aquino, Pietro Braione, Giovanni Denaro, Pasquale Salza
Softw. Test. Verification Reliab.2
2017 Combining symbolic execution and search-based testing for programs with complex heap inputs
abstract
Despite the recent improvements in automatic test case generation, handling complex data structures as test inputs is still an open problem. Search-based approaches can generate sequences of method calls that instantiate structured inputs to exercise a relevant portion of the code, but fall short in building inputs to execute program elements whose reachability is determined by the structural features of the input structures themselves. Symbolic execution techniques can effectively handle structured inputs, but do not identify the sequences of method calls that instantiate the input structures through legal interfaces. In this paper, we propose a new approach to automatically generate test cases for programs with complex data structures as inputs. We use symbolic execution to generate path conditions that characterise the dependencies between the program paths and the input structures, and convert the path conditions to optimisation problems that we solve with search-based techniques to produce sequences of method calls that instantiate those inputs. Our preliminary results show that the approach is indeed effective in generating test cases for programs with complex data structures as inputs, thus opening a promising research direction.
Pietro Braione, Giovanni Denaro, Andrea Mattavelli, Mauro Pezzè
ISSTA1
2016 JBSE: a symbolic executor for Java programs with complex heap inputs
abstract
We present the Java Bytecode Symbolic Executor (JBSE), a symbolic executor for Java programs that operates on complex heap inputs. JBSE implements both the novel Heap EXploration Logic (HEX), a symbolic execution approach to deal with heap inputs, and the main state-of-the-art approaches that handle data structure constraints expressed as either executable programs (repOk methods) or declarative specifications. JBSE is the first symbolic executor specifically designed to deal with programs that operate on complex heap inputs, to experiment with the main state-of-the-art approaches, and to combine different decision procedures to explore possible synergies among approaches for handling symbolic data structures.
Pietro Braione, Giovanni Denaro, Mauro Pezzè
SIGSOFT FSE1
2015 Symbolic execution of programs with heap inputs
abstract
Symbolic analysis is a core component of many automatic test generation and program verication approaches. To verify complex software systems, test and analysis techniques shall deal with the many aspects of the target systems at different granularity levels. In particular, testing software programs that make extensive use of heap data structures at unit and integration levels requires generating suitable input data structures in the heap. This is a main challenge for symbolic testing and analysis techniques that work well when dealing with numeric inputs, but do not satisfactorily cope with heap data structures yet. In this paper we propose a language HEX to specify invariants of partially initialized data structures, and a decision procedure that supports the incremental evaluation of structural properties in HEX. Used in combination with the symbolic execution of heap manipulating programs, HEX prevents the exploration of invalid states, thus improving the eefficiency of program testing and analysis, and avoiding false alarms that negatively impact on verication activities. The experimental data conrm that HEX is an effective and efficient solution to the problem of testing and analyzing heap manipulating programs, and outperforms the alternative approaches that have been proposed so far.
Pietro Braione, Giovanni Denaro, Mauro Pezzè
ESEC/SIGSOFT FSE1
2014 Software testing with code-based test generators: data and lessons learned from a case study with an industrial software component
Pietro Braione, Giovanni Denaro, Andrea Mattavelli, Mattia Vivanti
Softw. Qual. J.1
2013 Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization
abstract
Symbolic execution suffers from problems when analyzing programs that handle complex data structures as their inputs and take decisions over non-linear expressions. For these programs, symbolic execution may incur invalid inputs or unidentified infeasible traces, and may raise large amounts of false alarms. Some symbolic executors tackle these problems by introducing executable preconditions to exclude invalid inputs, and some solvers exploit rewrite rules to address non linear problems. In this paper, we discuss the core limitations of executable preconditions, and address these limitations by proposing invariants specifically designed to harmonize with the lazy initialization algorithm. We exploit rewrite rules applied within the symbolic executor, to address simplifications of inverse relationships fostered from either program-specific calculations or the logic of the verification tasks. We present a symbolic executor that integrates the two techniques, and validate our approach against the verification of a relevant set of properties of the Tactical Separation Assisted Flight Environment. The empirical data show that the integrated approach can improve the effectiveness of symbolic execution.
Pietro Braione, Giovanni Denaro, Mauro Pezzè
ESEC/SIGSOFT FSE1
2011 Enhancing structural software coverage by incrementally computing branch executability
Mauro Baluda, Pietro Braione, Giovanni Denaro, Mauro Pezzè
Softw. Qual. J.2
2006 Classification methods and inductive learning rules: what we may learn from theory
abstract
Inductive learning methods allow the system designer to infer a model of the relevant phenomena of an unknown process by extracting information from experimental data. A wide range of inductive learning methods is nowadays available, potentially ensuring different levels of accuracy on different problem domains. In this critical review of theoretic results gained in the last decade, we address the problem of designing an inductive classification system with optimal accuracy when domain knowledge is limited and the number of available experiments is-possibly-small. By analyzing the formal properties of consistent learning methods and of accuracy estimators, we wish to convey to the reader the message that the common practice of aggressively pursuing error minimization with different training algorithms and classification families is unjustified
Cesare Alippi, Pietro Braione
IEEE Trans. Syst. Man Cybern. Syst.2
2004 On Calculi for Context-Aware Coordination
Pietro Braione, Gian Pietro Picco
COORDINATION1
2002 A Semantical and Implementative Comparison of File Sharing Peer-to-Peer Applications
abstract
In this paper some representative peer-to-peer file sharing applications are compared against two sets of features. The first set describes the semantics of the relevant primitive operations over the shared data space. The second set describes the algorithmic and architectural solutions to implement these primitives. The obtained classification points out the mutual relationships between the expressive power and the degree of abstraction over low-level issues offered by each application.
Pietro Braione
Peer-to-Peer Computing1