Marcelo d'Amorim

dblp:16/608 · DBLP profile ↗
← Back
61ranked-venue papers
5as first author
28since 2021 · last 2026
0000-0002-1323-8769ORCID · verified

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

Software engineering, systems software and programming languages · 57 · 5 first-author · 26 since 2021Databases, data management, data science and information retrieval · 4 · 3 since 2021Applied, interdisciplinary, general and emerging computing · 3 · 1 since 2021Artificial intelligence and machine learning · 2Graphics, computer vision, multimedia, augmented reality and games · 1Theory of computation · 1 · 1 first-author
YearPublicationVenuePosition
2026 Improving Deep Learning Library Testing with Machine Learning
abstract
Deep Learning (DL) libraries like TensorFlow and Pytorch simplify machine learning (ML) model development but are prone to bugs due to their complex design. Bug-finding techniques exist, but without precise API specifications, they produce many false alarms. Existing methods to mine API specifications lack accuracy.
Facundo Molina, M. M. Abid Naziri, Feiran (Alex) Qin, Alessandra Gorla, Marcelo d'Amorim
AST5
2026 How Effective Is Coverage-Guided Fuzzing to Test Deep Learning Library APIs?
Feiran Alex Qin, M. M. Abid Naziri, Hengyu Ai, Saikat Dutta 0001, Marcelo d'Amorim
ICST5
2026 Learning Compiler Fuzzing Mutators from Historical Bugs
abstract
Bugs in compilers, which are critical infrastructure today, can have outsized negative impacts. Mutational fuzzers aid compiler bug detection by systematically mutating compiler inputs, i.e., programs. Their effectiveness depends on the quality of the mutators used. Yet, no prior work used compiler bug histories as a source of mutators.
Lingjun Liu, Feiran (Alex) Qin, Owolabi Legunsen, Marcelo d'Amorim
MSR4
2026 An Empirical Analysis of Cross-OS Portability Issues in Python Projects
abstract
While Python is designed as a cross-platform language, real-world applications encounter portability failures when deployed across different operating systems. We present the first large-scale empirical study of cross-OS portability issues in Python, analyzing 2,042 open-source repositories using two complementary approaches: systematic cross-OS test re-execution and manual analysis of GitHub issues. Our cross-platform testing of 500 projects reveals that 11.2% exhibit OS-dependent test failures. Through systematic analysis of 240 GitHub issues, we confirm 102 genuine portability problems spanning 95 additional projects. We develop a comprehensive taxonomy identifying 7 primary failure categories—with file/directory operations, process management, and library dependencies being most prevalent—along with 24 distinct sub-categories, 15 diagnostic signatures, and 4 systematic repair patterns. Our evaluation reveals that existing static analysis tools provide minimal support for portability detection, while large language models achieve 40–79% accuracy in identifying issues and 50–77% success in generating fixes when provided with structured guidance. Through 33 contributed pull requests, we demonstrate practical applicability and developer acceptance (17 merged, zero rejected) of our findings.
Denini Silva, MohamadAli Farahat, Marcelo d'Amorim
MSR3
2026 XMutant: XAI-based fuzzing for deep learning systems
abstract
Semantic-based test generators are widely used to produce failure-inducing inputs for Deep Learning (DL) systems. They typically generate challenging test inputs by applying random perturbations to input semantic concepts until a failure is found or a timeout is reached. However, such randomness may hinder them from efficiently achieving their goal. This paper proposes XMutant, a technique that leverages explainable artificial intelligence (XAI) techniques to generate challenging test inputs. XMutant uses the local explanation of the input to inform the fuzz testing process and effectively guide it toward failures of the DL system under test. We evaluated different configurations of XMutant in triggering failures for different DL systems both for model-level (sentiment analysis, digit recognition) and system-level testing (advanced driving assistance). Our studies showed that XMutant enables more effective and efficient test generation by focusing on the most impactful parts of the input. XMutant generates up to $$125\%$$ more failure-inducing inputs compared to an existing baseline, up to 7 $$\times$$ faster. We also assessed the validity of these inputs, maintaining a validation rate above $$89\%$$ , according to automated and human validators.
Xingcheng Chen, Matteo Biagiola, Vincenzo Riccio, Marcelo d'Amorim, Andrea Stocco 0001
Empir. Softw. Eng.4
2026 Configuration Defects in Kubernetes
abstract
Kubernetes is a tool that facilitates rapid deployment of software. Unfortunately, configuring Kubernetes is prone to errors. Configuration defects are not uncommon and can result in serious consequences. This paper reports an empirical study about configuration defects in Kubernetes with the goal of helping practitioners detect and prevent these defects. We study 719 defects that we extract from 2,260 Kubernetes configuration scripts using open source repositories. Using qualitative analysis, we identify 15 categories of defects, of which 7 have not been reported in previously-studied software systems. We find 8 publicly available static analysis tools to be capable of detecting 8 of the 15 defect categories. We find that the highest precision and recall of those tools are for defects related to data fields. We develop a linter to detect two categories of defects that cause serious consequences, which none of the studied tools are able to detect. Our linter revealed 26 previously-unknown defects that have been confirmed by practitioners, 19 of which have already been fixed. We conclude our paper by providing recommendations on how defect detection and repair techniques can be used for Kubernetes configuration scripts. The datasets and source code used for the paper are publicly available online.
Yue Zhang 0051, Uchswas Paul, Marcelo d'Amorim, Akond Ashfaque Ur Rahman
IEEE Trans. Software Eng.3
2025 Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
abstract
Runtime verification (RV) monitors program executions for conformance with formal specifications (specs). This paper concerns Monitoring-Oriented Programming (MOP), the only RV approach shown to scale to thousands of open-source GitHub projects when simultaneously monitoring passing unit tests against dozens of specs. Explicitly storing traces—sequences of spec-related program events—can make it easier to debug spec violations or to monitor tests against hyperproperties, which requires reasoning about sets of traces. But, most online MOP algorithms are implicit trace , i.e. they work event by event to avoid the time and space costs of storing traces. Yet, T race MOP, the only explicit-trace online MOP algorithm, is often too slow and often fails. We propose L azy MOP, a faster explicit-trace online MOP algorithm for RV of tests that is enabled by three simple optimizations. First, whereas all existing online MOP algorithms eagerly monitor all events as they occur, L azy MOP lazily stores only unique traces at runtime and monitors them just before the test run ends. Lazy monitoring is inspired by a recent finding: 99.87% of traces during RV of tests are duplicates. Second, to speed up trace storage, L azy MOP encodes events and their locations as integers, and amortizes the cost of looking up locations across events. Lastly, L azy MOP only synchronizes accesses to its trace store after detecting multi-threading, unlike T race MOP’s eager and wasteful synchronization of all accesses. On 179 Java open-source projects, L azy MOP is up to 4.9 x faster and uses 4.8 x less memory than T race MOP, finding the same traces (modulo test non-determinism) and violations. We show L azy MOP’s usefulness in the context of software evolution, where tests are re-run after each code change. L azy MOP e optimizes L azy MOP in this context by generating fewer duplicate traces. Using unique traces from one code version, L azy MOP e finds all pairs of method m and spec s , where all traces for s in m are identical. Then, in a future version, L azy MOP e generates and monitors only one trace of s in m . L azy MOP e is up to 3.9 x faster than L azy MOP and it speeds up two recent techniques that speed up RV during evolution by up to 4.6 x with no loss in violations.
Kevin Guan, Marcelo d'Amorim, Owolabi Legunsen
Proc. ACM Program. Lang.2
2025 Test Oracle Automation in the Era of LLMs
abstract
The effectiveness of a test suite in detecting faults highly depends on the quality of its test oracles. Large Language Models (LLMs) have demonstrated remarkable proficiency in tackling diverse software testing tasks. This article aims to present a roadmap for future research on the use of LLMs for test oracle automation. We discuss the progress made in the field of test oracle automation before the introduction of LLMs, identifying the main limitations and weaknesses of existing techniques. Additionally, we discuss recent studies on the use of LLMs for this task, highlighting the main challenges that arise from their use, e.g., how to assess quality and usefulness of the generated oracles. We conclude with a discussion about the directions and opportunities for future research on LLM-based oracle automation.
Facundo Molina, Alessandra Gorla, Marcelo d'Amorim
ACM Trans. Softw. Eng. Methodol.3
2025 ChatAssert: LLM-Based Test Oracle Generation With External Tools Assistance
abstract
Test oracle generation is an important and challenging problem. Neural-based solutions have been recently proposed for oracle generation but they are still inaccurate. For example, the accuracy of the state-of-the-art techniquetecois only 27.5% on its dataset including 3,540 test cases. We proposeChatAssert, a prompt engineering framework designed for oracle generation that uses dynamic and static information to iteratively refine prompts for querying large language models (LLMs).ChatAssertuses code summaries and examples to assist an LLM in generating candidate test oracles, uses a lightweight static analysis to assist the LLM in repairing generated oracles that fail to compile, and uses dynamic information obtained from test runs to help the LLM in repairing oracles that compile but do not pass. Experimental results using an independent publicly-available dataset show thatChatAssertimproves the state-of-the-art technique,teco, on key evaluation metrics. For example, it improvesAcc@1by 15%. Overall, results provide initial yet strong evidence that using external tools in the formulation of prompts is an important aid in LLM-based oracle generation.
Ishrak Hayet, Adam Scott, Marcelo d'Amorim
IEEE Trans. Software Eng.3
2024 Feedback-Directed Partial Execution
abstract
Partial code execution is the problem of executing code with missing definitions. The problem has gained recent traction as solutions to the problem could enable various downstream analyses. We propose feedback-directed partial execution, a technique supported by a tool, named Incompleter, that uses the error feedback from executions to enable partial code execution. Incompleter builds on the observation that errors observed during the execution of incomplete snippets often follow similar error patterns. Incompleter takes an incomplete snippet as input and applies rules (e.g., add class, add field, add file, etc.) to resolve the successive dynamic errors it encounters during execution of the snippet. Incompleter stops when the snippet successfully executes or when it reaches certain bounds. Our results indicate that Incompleter outperforms LExecutor, the state-of-the-art in partial execution. For example, considering a dataset of 4.7K incomplete StackOverflow snippets, Incompleter enables the execution of 10% more code snippets compared to LExecutor and covers 23% more statements. We also show that Incompleter’s type inference significantly improves over LExecutor’s type inference, with a 37% higher F1 score.
Ishrak Hayet, Adam Scott, Marcelo d'Amorim
ISSTA3
2024 The Effects of Computational Resources on Flaky Tests
abstract
Flaky tests are tests that non-deterministically pass and fail in unchanged code. These tests can be detrimental to developers’ productivity. Particularly when tests run in continuous integration environments, the tests may be competing for access to limited computational resources (CPUs, memory etc.), and we hypothesize that resource (un)-availability may be a significant factor in the failure rate of flaky tests. We present the first assessment of the impact that computational resources have on flaky tests, including a total of 52 projects written in Java, JavaScript and Python, and 27 different resource configurations. Using a rigorous statistical methodology, we determine which tests are RAFTs (Resource-Affected Flaky Tests). We find that 46.5% of the flaky tests in our dataset are RAFTs, indicating that a substantial proportion of flaky-test failures happen depending on the resources available when running tests. We report RAFTs and configurations to avoid them to developers, and received interest to either fix the RAFTs or to improve the specifications of the projects so that tests would be run only in configurations that are unlikely to encounter RAFT failures. Although most test suites in our dataset are executed quite quickly (under one minute) in a baseline configuration, our results highlight the possibility of using this methodology to detect RAFT to reduce the cost of cloud infrastructure for reliably running larger test suites.
Denini Silva, Martin Gruber, Satyajit Gokhale, Ellen Arteca, Alexi Turcotte, Marcelo d'Amorim, Wing Lam, Stefan Winter 0001, Jonathan Bell 0001
IEEE Trans. Software Eng.6
2023 SpecFuzzer: A Tool for Inferring Class Specifications via Grammar-Based Fuzzing
abstract
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.
Facundo Molina, Marcelo d'Amorim, Nazareno Aguirre
ASE2
2023 Test Flakiness Across Programming Languages
abstract
Regression Testing (RT) is a quality-assurance practice commonly adopted in the software industry to check if functionality remains intact after code changes. Test flakiness is a serious problem for RT. A test is said to be flaky when it non-deterministically passes or fails on a fixed environment. Prior work studied test flakiness primarily on Java programs. It is unclear, however, how problematic is test flakiness for software written in other programming languages. This paper reports on a study focusing on three central aspects of test flakiness: concentration, similarity, and cost. Considering concentration, our results show that, for any given programming language that we studied (C, Go, Java, JS, and Python), most issues could be explained by a small fraction of root causes (5/13 root causes cover 78.07% of the issues) and could be fixed by a relatively small fraction of fix strategies (10/23 fix strategies cover 85.20% of the issues). Considering similarity, although there were commonalities in root causes and fixes across languages (e.g., concurrency and async wait are common causes of flakiness in most languages), we also found important differences (e.g., flakiness due to improper release of resources are more common in C), suggesting that there is opportunity to fine tuning analysis tools. Considering cost, we found that issues related to flaky tests are resolved either very early once they are posted ($< $10 days), suggesting relevance, or very late ($>$100 days), suggesting irrelevance.
Keila Barbosa Costa, Ronivaldo Ferreira, Gustavo Pinto 0001, Marcelo d'Amorim, Breno Miranda
IEEE Trans. Software Eng.4
2023 NCQ: Code Reuse Support for Node.js Developers
abstract
Code reuse is an important part of software development. The adoption of code reuse practices is especially common among Node.js developers. The Node.js package manager, NPM, indexes over 1 Million packages and developers often seek out packages to solve programming tasks. Due to the vast number of packages, selecting the right package is difficult and time consuming. With the goal of improving productivity of developers that heavily reuse code through third-party packages, we presentNode Code Query(NCQ), a Read-Eval-Print-Loop environment that allows developers to 1) search for NPM packages using natural language queries, 2) search for code snippets related to those packages, 3) automatically correct errors in these code snippets, 4) quickly setup new environments for testing those snippets, and 5) transition between search and editing modes. In two user studies with a total of 20 participants, we find that participants begin programming faster and conclude tasks faster with NCQ than with baseline approaches, and that they like, among other features, the search for code snippets and packages. Our results suggest that NCQ makes Node.js developers more efficient in reusing code.
Brittany Reid, Marcelo d'Amorim, Markus Wagner 0007, Christoph Treude
IEEE Trans. Software Eng.2
2023 Runtime Verification of Crypto APIs: An Empirical Study
abstract
Misuse of cryptographic (crypto) APIs is a noteworthy cause of security vulnerabilities. For this reason, static analyzers were recently proposed for detecting crypto API misuses. They differ in strengths and weaknesses, and they might miss bugs. Motivated by the inherent limitations of static analyzers, this article reports on a study of runtime verification (RV) as a dynamic-analysis-based alternative for crypto API misuse detection. RV monitors program runs against formal specifications; it was shown to be effective and efficient for amplifying the bug-finding ability of software tests. We focus on the popular JCA crypto API and write 22 RV specifications based on expert-validated rules in a static analyzer. We monitor these specifications while running tests in five benchmarks. Lastly, we compare the accuracy of our RV-based approach, RVSec, with those of three state-of-the-art crypto API misuses detectors: CogniCrypt, CryptoGuard, and CryLogger. Results show that RVSec has higher accuracy in four benchmarks and is on par with CryptoGuard in the fifth. Overall, RVSec achieves an average${\boldsymbol{F}}_{1}$measure of 95%, compared with 83%, 78%, and 86% for CogniCrypt, CryptoGuard, and CryLogger, respectively. We highlight the strengths and limitations of these tools and show that RV is effective for detecting crypto API misuses. We also discuss how static and dynamic analysis can complement each other for detecting crypto API misuses.
Adriano Torres, Pedro Henrique Teixeira Costa, Luis Henrique Vieira Amaral, Jonata Pastro, Rodrigo Bonifácio, Marcelo d'Amorim, Owolabi Legunsen, Eric Bodden, Edna Dias Canedo
IEEE Trans. Software Eng.6
2022 Fuzzing Class Specifications
abstract
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.
Facundo Molina, Marcelo d'Amorim, Nazareno Aguirre
ICSE2
2022 ThirdEye: Attention Maps for Safe Autonomous Driving Systems
abstract
Automated online recognition of unexpected conditions is an indispensable component of autonomous vehicles to ensure safety even in unknown and uncertain situations. In this paper we propose a runtime monitoring technique rooted in the attention maps computed by explainable artificial intelligence techniques. Our approach, implemented in a tool called ThirdEye, turns attention maps into confidence scores that are used to discriminate safe from unsafe driving behaviours. The intuition is that uncommon attention maps are associated with unexpected runtime conditions.
Andrea Stocco 0001, Paulo J. Nunes, Marcelo d'Amorim, Paolo Tonella
ASE3
2022 Leveraging Practitioners' Feedback to Improve a Security Linter
abstract
Infrastructure-as-Code (IaC) is a technology that enables the management and distribution of infrastructure through code instead of manual processes. In 2020, Palo Alto Network’s Unit 42 announced the discovery of over 199K vulnerable IaC templates through their “Cloud Threat” Report. This report highlights the importance of tools to prevent vulnerabilities from reaching production. Unfortunately, we observed through a comprehensive study that a security linter for IaC scripts is not reliable yet—high false positive rates. Our approach to tackling this problem was to leverage community expertise to improve the precision of this tool. More precisely, we interviewed professional developers to collect their feedback on the root causes of imprecision of the state-of-the-art security linter for Puppet. From that feedback, we developed a linter adjusting 7 rules of an existing linter ruleset and adding 3 new rules. We conducted a new study with 131 practitioners, which helped us improve the tool’s precision significantly and achieve a final precision of . An important takeaway from this paper is that obtaining professional feedback is fundamental to improving the rules’ precision and extending the rulesets, which is critical for the usefulness and adoption of lightweight tools, such as IaC security linters.
Sofia Reis, Rui Abreu 0001, Marcelo d'Amorim, Daniel Fortunato
ASE3
2022 RVprio: A tool for prioritizing runtime verification violations
abstract
Summary Runtime verification (RV) helps to find software bugs by monitoring formally specified properties during testing. A key problem in using RV during testing is how to reduce the manual inspection effort for checking whether property violations are true bugs. To date, there was no automated approach for determining the likelihood that property violations were true bugs to reduce tedious and time‐consuming manual inspection. We present RVprio, the first automated approach for prioritizing RV violations in order of likelihood of being true bugs. RVprio uses machine learning classifiers to prioritize violations. For training, we used a labelled dataset of 1170 violations from 110 projects. On that dataset, (1) RVprio reached 90% of the effectiveness of a theoretically optimal prioritizer that ranks all true bugs at the top of the ranked list, and (2) 88.1% of true bugs were in the top 25% of RVprio‐ranked violations; 32.7% of true bugs were in the top 10%. RVprio was also effective when we applied it to new unlabelled violations, from which we found previously unknown bugs—54 bugs in 8 open‐source projects. Our dataset is publicly available online.
Lucas Cabral 0002, Breno Miranda, Igor Lima, Marcelo d'Amorim
Softw. Test. Verification Reliab.4
2022 Syrius: Synthesis of Rules for Intrusion Detectors
abstract
Network intrusion detection systems (NIDS) are popular tools to defend local networks against attacks. These systems monitor the network traffic and flag suspicious behavior. Rule-based NIDS do that by checking the network traffic against a set of rules, which become obsolete as attackers learn new strategies to circumvent existing defenses. This article proposessynthesis of suricata rules(Syrius), a novel approach to synthesize rules for rule-based NIDS.Syriusleverages malicious (positive) and benign (negative) traffic to create rules for new attacks.Syriusis organized as a pipeline of three components to 1) create an overspecified seed rule, 2) derive plausible rules from the seed, and 3) rank plausible rules. We evaluatedSyriusagainst a set of 21 network attacks with various characteristics.Syriuswas capable of generating the correct rule among the top-3 and top-1 rules of the ranking, respectively, in 80.1% and 47.6% of the cases.
Lucas A. M. De Alcantara, Guilherme Padilha, Rui Abreu 0001, Marcelo d'Amorim
IEEE Trans. Reliab.4
2021 A comparative study on methods and tools for handwritten mathematical expression recognition
abstract
Handwritten mathematical expression recognition (HMER) is a challenging task due to factors such as ambiguity, variety of writing styles, and complexity of two-dimensional writing. In this paper, we identify challenges in HMER applications through experiments that simulate real scenarios that go far beyond the usual cases found in literature: variations on luminance; different stroke width, inclination and color; different background pattern; and partially shaded images. The results of state-of-the-art methods (as TAP and Dense-WAP) and a commercial tool (MathPix) are analyzed, using the CROHME 2016 database. We proved that, although the area has had a lot of improvement in recent years, there are still issues to overcome.
Daniela S. Costa, Carlos A. B. Mello, Marcelo d'Amorim
DocEng3
2021 Shipwright: A Human-in-the-Loop System for Dockerfile Repair
Jordan Henkel, Denini Silva, Leopoldo Teixeira, Marcelo d'Amorim, Thomas W. Reps
ICSE4
2021 Soundy Automated Parallelization of Test Execution
abstract
Regression Testing is an important quality assurance practice widely adopted today. Optimizing regression testing is important. Test parallelization has the potential to leverage the power of multi-core architectures to accelerate regression testing. Unfortunately, it is not possible to directly use parallelization options available in build systems and testing frameworks without introducing test flakiness. Tests can fail because of data races or broken test dependencies. Although it is possible to safely circumvent those problems with the assistance of an automated tool to collect test dependencies (e.g., PRADET), the cost of that solution is prohibitive, defeating the purpose of test parallelization. This paper proposes PASTE an approach to automatically parallelize the execution of test suites. PASTE alternates parallel and sequential execution of test cases and test classes to circumvent provoked test failures. PASTE does not provide the safety guarantee that flakiness will not be manifested, but our results indicate that the strategy is sufficient to avoid them. We evaluated PASTE on 25 projects mined from GitHub using an objective selection criteria. Results show that (i) PASTE could circumvent flakiness introduced with parallelization in all projects that manifested them and (ii) 52% of the projects benefited from test-parallelization with a median speedup of 1.59x (best: 2.28x, average: 1.47x, worst: 0.93x).
Shouvick Mondal, Denini Silva, Marcelo d'Amorim
ICSME3
2021 Demystifying the Challenges of Formally Specifying API Properties for Runtime Verification
abstract
Runtime Verification (RV) is a technique to monitor formally-specified properties of the software during its execution. RV has shown to be very effective for bug finding. Unfortunately, RV typically relies on formal specification languages and learning those languages be costly for developers. This paper reports on a study to assess the challenges to specify API properties for the purpose of RV. To that end, we wrote SIESTA, a minimalist specification language, extending Java with two features (the ability to catch calls to specified methods and the ability to access the event history of a given object), and asked inexperienced developers (students) to write specifications in that language for certain parts of the Java API. Among our findings, we observed that 40% of the specifications written by the students matched the ground truth perfectly. The main messages of this work are that 1) it is feasible to use a simple imperative language for specifying properties without significant loss of generality; and that 2) developers are capable of writing specifications in the (programming) language they feel comfortable.
Leopoldo Teixeira, Breno Miranda, Henrique Rebêlo, Marcelo d'Amorim
ICST4
2021 Shaker: a Tool for Detecting More Flaky Tests Faster
abstract
A test case that intermittently passes or fails when performed under the same version of source code and test code is said to be flaky. The presence of flaky tests wastes testing time and effort. The most popular approach in industry to detect flakiness is ReRun. The idea behind ReRun is very simple: failing test cases are re-executed many times looking for inconsistencies in the output. Despite its simplicity, the ReRun strategy is very expensive both in terms of time and in terms of computational resources. This is particularly true for contexts where thousands of test cases are performed on a daily basis. Reducing the rerunning overhead is, thus, of utmost importance. This paper presents SHAKER, an open-source tool for detecting flakiness in time-constrained tests by adding noise in the execution environment. The main idea behind SHAKER is to add stressing tasks that compete with the test execution for the use of resources (CPU or memory). SHAKER is available as a GitHub Actions workflow that can be seamlessly integrated with any GitHub project. Alternatively, SHAKER can also be used via its provided Command Line Interface. In our evaluation, SHAKER was able to discover more flaky tests than ReRun and in a faster way (less re-executions); besides, our approach revealed tens of new flaky tests that went undetected by ReRun even after 50 re-executions. Thanks to its flexibility and ease of use, we believe that SHAKER can be useful for both practitioners and researchers.Demo video: https://youtu.be/7-aiQwOb4rAShaker website: https://star-rg.github.io/shaker
Marcello Cordeiro, Denini Silva, Leopoldo Teixeira, Breno Miranda, Marcelo d'Amorim
ASE5
2021 Identifying method-level mutation subsumption relations using Z3
Rohit Gheyi, Márcio Ribeiro 0001, Beatriz Souza, Marcio Augusto Guimarães, Leonardo Fernandes, Marcelo d'Amorim, Vander Alves, Leopoldo Teixeira, Baldoino Fonseca dos Santos Neto
Inf. Softw. Technol.6
2021 Exposing bugs in JavaScript engines through test transplantation and differential testing
Igor Lima, Jefferson Silva, Breno Miranda, Gustavo Pinto 0001, Marcelo d'Amorim
Softw. Qual. J.5
2021 Using Docker to Assist Q&A Forum Users
abstract
Q&A forums are today a valuable tool to assist developers in programming tasks. Unfortunately, contributions to these forums are often unclear and incomplete. Docker is a container solution that enables software developers to encapsulate an operating environment and could help address reproducibility issues. This artile reports on a feasibility study to evaluate if Docker can help improve reproducibility in Stack Overflow. We started surveying Stack Overflow users to understand their perceptions on the proposal of using Docker to reproduce Stack Overflow posts. Participants were critical and mentioned two important aspects: cost and need. To validate their criticism, we conducted an exploratory study focused on understanding how costly the task of creating containers for posts is for developers. Overall, results indicate that the cost of creating containers is not high, especially due to the fact that dockerfiles are highly similar and small. Based on these findings we developed a tool, dubbedFrisk, to assist developers in creating containers for those posts. We then conducted a user study to evaluate interest of Stack Overflow developers on the tool. We found that, on average, users spent nearly ten minutes interacting withFriskand that 45.3% of the 563Frisksessions we created for existing posts resulted in a successful access to the corresponding web service by the owners of the post. Overall, this artile provides early evidence that the use of Docker in Q&A forums should be encouraged for configuration-related posts.
Luis Melo, Igor Scaliante Wiese, Marcelo d'Amorim
IEEE Trans. Software Eng.3
2020 Shake It! Detecting Flaky Tests Caused by Concurrency with Shaker
abstract
A test is said to be flaky when it non-deterministically passes or fails. Test flakiness negatively affects the effectiveness of regression testing and, consequently, impacts software evolution. Detecting test flakiness is an important and challenging problem. ReRun is the most popular approach in industry to detect test flakiness. It re-executes a test suite on a fixed code version multiple times, looking for inconsistent outputs across executions. Unfortunately, ReRun is costly and unreliable. This paper proposes SHAKER, a lightweight technique to improve the ability of ReRun to detect flaky tests. SHAKER adds noise in the execution environment (e.g., it adds stressor tasks to compete for the CPU or memory). It builds on the observations that concurrency is an important source of flakiness and that adding noise in the environment can interfere in the ordering of events and, consequently, influence on the test outputs. We conducted experiments on a data set with 11 Android apps. Results are very encouraging. SHAKER discovered many more flaky tests than ReRun (95% and 37.5% of the total, respectively) and discovered these flaky tests much faster. In addition, SHAKER was able to reveal 61 new flaky tests that went undetected in 50 re-executions with ReRun.
Denini Silva, Leopoldo Teixeira, Marcelo d'Amorim
ICSME3
2020 Optimizing Mutation Testing by Discovering Dynamic Mutant Subsumption Relations
abstract
One recent promising direction on reducing costs of mutation analysis is to identify redundant mutations, i.e., mutations that are subsumed by some other mutations. Previous works found out redundant mutants manually through the truth table. Although the idea is promising, it can only be applied for logical and relational operators. In this paper, we propose an approach to discover redundancy in mutations through dynamic subsumption relations among mutants. We focus on subsumption relations among mutations of an expression or statement, named here as “mutation target:” By focusing on targets and relying on automatic test generation tools, we define subsumption relations for dozens of mutation targets in which the MUJAVA tool can apply mutations. We then implemented these relations in a tool, named MUJAVA-M, that generates a reduced set of mutants for each target, avoiding redundant mutants. We evaluated MUJAVA and MUJAVA-M using classes of five open-source projects. As results, we analyze 2,341 occurrences of 32 mutation targets in 168 classes. MUJAVA-M generates less mutants (on average 64.43% less) with 100% of effectiveness in 20 out of 32 targets and more than 95% in 29 out of 32 mutation targets. MUJAVA- M also reduced the time to execute the test suites against the mutants in 52.53% on average, considering the full mutation analysis process.
Marcio Augusto Guimarães, Leonardo Fernandes, Márcio Ribeiro 0001, Marcelo d'Amorim, Rohit Gheyi
ICST4
2020 Prioritizing Runtime Verification Violations
abstract
Runtime Verification (RV) can help find software bugs by monitoring formally specified properties during testing. A key problem when using RV during testing is how to reduce the manual inspection effort for checking whether property violations are true bugs. To date, there was no automated approach for determining the likelihood that property violations were true bugs to reduce tedious and time-consuming manual inspection.We present RVPRIO, the first automated approach for prioritizing RV violations in order of likelihood of being true bugs. RVPRIO uses machine learning classifiers to prioritize violations. For training, we used a labeled dataset of 1,170 violations from 110 projects. On that dataset, (1) RVPRIO reached 90% of the effectiveness of a theoretically optimal prioritizer that ranks all true bugs at the top of the ranked list, and (2) 88.1% of true bugs were in the top 25% of RVPRIO-ranked violations; 32.7% of true bugs were in the top 10%. RVPRIO was also effective when we applied it to new unlabeled violations, from which we found previously unknown bugs-29 bugs in 7 projects and two bugs in two properties. Our dataset is publicly available online.
Breno Miranda, Igor Lima, Owolabi Legunsen, Marcelo d'Amorim
ICST4
2020 What is the Vocabulary of Flaky Tests?
abstract
Flaky tests are tests whose outcomes are non-deterministic. Despite the recent research activity on this topic, no effort has been made on understanding the vocabulary of flaky tests. This work proposes to automatically classify tests as flaky or not based on their vocabulary. Static classification of flaky tests is important, for example, to detect the introduction of flaky tests and to search for flaky tests after they are introduced in regression test suites.
Gustavo Pinto 0001, Breno Miranda, Supun Dissanayake, Marcelo d'Amorim, Christoph Treude, Antonia Bertolino
MSR4
2020 Practical detection of CMS plugin conflicts in large plugin sets
Igor Lima, Jeanderson Cândido, Marcelo d'Amorim
Inf. Softw. Technol.3
2019 Intent-Preserving Test Repair
abstract
Repairing broken tests in evolving software systems is an expensive and challenging task. One of the main challenges for test repair, in particular, is preserving the intent of the original tests in the repaired ones. To address this challenge, we propose a technique for test repair that models and considers the intent of a test when repairing it. Our technique first uses a search-based approach to generate repair candidates for the broken test. It then computes, for each candidate, its likelihood of preserving the original test intent. To do so, the technique characterizes such intent using the path conditions generated during a dynamic symbolic execution of the tests. Finally, the technique reports the best candidates to the developer as repair recommendations. We implemented and evaluated our technique on a benchmark of 91 broken tests in 4 open-source programs. Our results are promising, in that the technique was able to generate intentpreserving repair candidates for over 79% of those broken tests and rank the intent-preserving candidates as the first choice of repair recommendations for almost 70% of the broken tests.
Xiangyu Li 0001, Marcelo d'Amorim, Alessandro Orso
ICST2
2019 Demystifying the Combination of Dynamic Slicing and Spectrum-based Fault Localization
abstract
Several approaches have been proposed to reduce debugging costs through automated software fault diagnosis. Dynamic Slicing (DS) and Spectrum-based Fault Localization (SFL) are popular fault diagnosis techniques and normally seen as complementary. This paper reports on a comprehensive study to reassess the effects of combining DS with SFL. With this combination, components that are often involved in failing but seldom in passing test runs could be located and their suspiciousness reduced. Results show that the DS-SFL combination, coined as Tandem-FL, improves the diagnostic accuracy up to 73.7% (13.4% on average). Furthermore, results indicate that the risk of missing faulty statements, which is a DS?s key limitation, is not high ? DS misses faulty statements in 9% of the 260 cases. To sum up, we found that the DS-SFL combination was practical and effective and encourage new SFL techniques to be evaluated against that optimization.
Sofia Reis, Rui Abreu 0001, Marcelo d'Amorim
IJCAI3
2018 Enlightened debugging
abstract
Numerous automated techniques have been proposed to reduce the cost of software debugging, a notoriously time-consuming and human-intensive activity. Among these techniques, Statistical Fault Localization (SFL) is particularly popular. One issue with SFL is that it is based on strong, often unrealistic assumptions on how developers behave when debugging. To address this problem, we propose Enlighten, an interactive, feedback-driven fault localization technique. Given a failing test, Enlighten (1) leverages SFL and dynamic dependence analysis to identify suspicious method invocations and corresponding data values, (2) presents the developer with a query about the most suspicious invocation expressed in terms of inputs and outputs, (3) encodes the developer feedback on the correctness of individual data values as extra program specifications, and (4) repeats these steps until the fault is found. We evaluated Enlighten in two ways. First, we applied Enlighten to 1,807 real and seeded faults in 3 open source programs using an automated oracle as a simulated user; for over 96% of these faults, Enlighten required less than 10 interactions with the simulated user to localize the fault, and a sensitivity analysis showed that the results were robust to erroneous responses. Second, we performed an actual user study on 4 faults with 24 participants and found that participants who used Enlighten performed significantly better than those not using our tool, in terms of both number of faults localized and time needed to localize the faults.
Xiangyu Li 0001, Shaowei Zhu 0001, Marcelo d'Amorim, Alessandro Orso
ICSE3
2018 Automatically translating bug reports into test cases for mobile apps
abstract
When users experience a software failure, they have the option of submitting a bug report and provide information about the failure and how it happened. If the bug report contains enough information, developers can then try to recreate the issue and investigate it, so as to eliminate its causes. Unfortunately, the number of bug reports filed by users is typically large, and the tasks of analyzing bug reports and reproducing the issues described therein can be extremely time consuming. To help make this process more efficient, in this paper we propose Yakusu, a technique that uses a combination of program analysis and natural language processing techniques to generate executable test cases from bug reports. We implemented Yakusu for Android apps and performed an empirical evaluation on a set of over 60 real bug reports for different real-world apps. Overall, our technique was successful in 59.7% of the cases; that is, for a majority of the bug reports, developers would not have to study the report to reproduce the issue described and could simply use the test cases automatically generated by Yakusu. Furthermore, in many of the remaining cases, Yakusu was unsuccessful due to limitations that can be addressed in future work.
Mattia Fazzini, Martin Prammer, Marcelo d'Amorim, Alessandro Orso
ISSTA3
2018 Time-space efficient regression testing for configurable systems
Sabrina Souto, Marcelo d'Amorim
J. Syst. Softw.2
2017 Balancing soundness and efficiency for practical testing of configurable systems
abstract
Testing configurable systems is important and challenging due to the enormous space of configurations where errors can hide. Existing approaches to test these systems are often costly or unreliable. This paper proposes S-SPLat, a technique that combines heuristic sampling with symbolic search to obtain both breadth and depth in the exploration of the configuration space. S-SPLat builds on SPLat, our previously developed technique, that explores all reachable configurations from tests. In contrast to its predecessor, S-SPLat sacrifices soundness in favor of efficiency. We evaluated our technique on eight software product lines of various sizes and on a large configurable system - GCC. Considering the results for GCC, S-SPLat was able to reproduce all five bugs that we previously found in a previous study with SPLat but much faster and it was able to find two new bugs in a recent release of GCC. Results suggest that it is preferable to use a combination of simple heuristics to drive the symbolic search as opposed to a single heuristic. S-SPLat and our experimental infrastructure are publicly available.
Sabrina Souto, Marcelo d'Amorim, Rohit Gheyi
ICSE2
2017 Prevalence of Single-Fault Fixes and Its Impact on Fault Localization
abstract
Several fault predictors were proposed in the context of Spectrum-based Fault Localization approaches to rank software components in order of suspiciousness of being the root-cause of observed failures. Previous work has also shown that some of the fault predictors (near-)optimally rank software components, provided that there is one fault in the system. Despite this, further work is being spent on creating more complex, computationally expensive, model-based techniques that can handle multiple-faulted scenarios accurately. However, our hypothesis is that when software is being developed, bugs arise one-at-a-time and therefore can be considered as single-faulted scenarios. We describe an approach to mine repositories, find bug-fixes, and catalog them according to the number of faults they fix, to assess the prevalence of single-fault fixes. Our empirical study using 279 open-source projects reveals that there is a prevalence of single-fault fixes, with over 82% of all fixes only eliminating one bug from the system, enabling the use of simpler, (near-)optimal, fault predictors. Moreover, we draw on the practical implications of our findings to influence and set direction for future research.
Alexandre Perez, Rui Abreu 0001, Marcelo d'Amorim
ICST3
2017 Test suite parallelization in open-source projects: a study on its usage and impact
abstract
Dealing with high testing costs remains an important problem in Software Engineering. Test suite parallelization is an important approach to address this problem. This paper reports our findings on the usage and impact of test suite parallelization in open-source projects. It provides recommendations to practitioners and tool developers to speed up test execution. Considering a set of 468 popular Java projects we analyzed, we found that 24% of the projects contain costly test suites but parallelization features still seem underutilized in practice - only 19.1% of costly projects use parallelization. The main reported reason for adoption resistance was the concern to deal with concurrency issues. Results suggest that, on average, developers prefer high predictability than high performance in running tests.
Jeanderson Cândido, Luis Melo, Marcelo d'Amorim
ASE3
2017 Preface
Tao Xie 0001, Yuanfang Cai, Xuanzhe Liu, Xiaoyin Wang, Mithun Acharya, Marcelo d'Amorim, Xiaoxing Ma
J. Comput. Sci. Technol.6
2015 Static Analysis of Implicit Control Flow: Resolving Java Reflection and Android Intents (T)
abstract
Implicit or indirect control flow is a transfer of control between procedures using some mechanism other than an explicit procedure call. Implicit control flow is a staple design pattern that adds flexibility to system design. However, it is challenging for a static analysis to compute or verify properties about a system that uses implicit control flow. This paper presents static analyses for two types of implicit control flow that frequently appear in Android apps: Java reflection and Android intents. Our analyses help to resolve where control flows and what data is passed. This information improves the precision of downstream analyses, which no longer need to make conservative assumptions about implicit control flow. We have implemented our techniques for Java. We enhanced an existing security analysis with a more precise treatment of reflection and intents. In a case study involving ten real-world Android apps that use both intents and reflection, the precision of the security analysis was increased on average by two orders of magnitude. The precision of two other downstream analyses was also improved.
Paulo Barros, René Just, Suzanne Millstein, Paul Vines, Werner Dietl, Marcelo d'Amorim, Michael D. Ernst
ASE6
2015 Iterative distribution-aware sampling for probabilistic symbolic execution
abstract
Probabilistic symbolic execution aims at quantifying the probability of reaching program events of interest assuming that program inputs follow given probabilistic distributions. The technique collects constraints on the inputs that lead to the target events and analyzes them to quantify how likely it is for an input to satisfy the constraints. Current techniques either handle only linear constraints or only support continuous distributions using a “discretization” of the input domain, leading to imprecise and costly results. We propose an iterative distribution-aware sampling approach to support probabilistic symbolic execution for arbitrarily complex mathematical constraints and continuous input distributions. We follow a compositional approach, where the symbolic constraints are decomposed into sub-problems whose solution can be solved independently. At each iteration the convergence rate of the com- putation is increased by automatically refocusing the analysis on estimating the sub-problems that mostly affect the accuracy of the results, as guided by three different ranking strategies. Experiments on publicly available benchmarks show that the proposed technique improves on previous approaches in terms of scalability and accuracy of the results.
Mateus Borges, Antonio Filieri, Marcelo d'Amorim, Corina Pasareanu
ESEC/SIGSOFT FSE3
2015 Faster bug detection for software product lines with incomplete feature models
abstract
A software product line (SPL) is a family of programs that are differentiated by features --- increments in functionality. Systematically testing an SPL is challenging because it requires running each test of a test suite against a combinatorial number of programs. Feature models capture dependencies among features and can (1) reduce the space of programs to test and (2) enable accurate categorization of failing tests as failures of programs or the tests themselves, not as failures due to illegal combinations of features. In practice, sadly, feature models are not always available.
Sabrina Souto, Divya Gopinath, Marcelo d'Amorim, Darko Marinov, Sarfraz Khurshid, Don S. Batory
SPLC3
2014 Compositional solution space quantification for probabilistic software analysis
abstract
Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time.
Mateus Borges, Antonio Filieri, Marcelo d'Amorim, Corina Pasareanu, Willem Visser
PLDI3
2014 Quantifying information leaks using reliability analysis
abstract
We report on our work-in-progress into the use of reliability analysis to quantify information leaks. In recent work we have proposed a software reliability analysis technique that uses symbolic execution and model counting to quantify the probability of reaching designated program states, e.g. assert violations, under uncertainty conditions in the environment. The technique has many applications beyond reliability analysis, ranging from program understanding and debugging to analysis of cyber-physical systems. In this paper we report on a novel application of the technique, namely Quantitative Information Flow analysis (QIF). The goal of QIF is to measure information leakage of a program by using information-theoretic metrics such as Shannon entropy or Renyi entropy. We exploit the model counting engine of the reliability analyzer over symbolic program paths, to compute an upper bound of the maximum leakage over all possible distributions of the confidential data.
Quoc-Sang Phan, Pasquale Malacaria, Corina Pasareanu, Marcelo d'Amorim
SPIN4
2014 Efficient static checker for tainted variable attacks
Andrei Rimsa, Marcelo d'Amorim, Fernando Magno Quintão Pereira, Roberto da Silva Bigonha
Sci. Comput. Program.2
2013 Entropy-based test generation for improved fault localization
abstract
Spectrum-based Bayesian reasoning can effectively rank candidate fault locations based on passing/failing test cases, but the diagnostic quality highly depends on the size and diversity of the underlying test suite. As test suites in practice often do not exhibit the necessary properties, we present a technique to extend existing test suites with new test cases that optimize the diagnostic quality. We apply probability theory concepts to guide test case generation using entropy, such that the amount of uncertainty in the diagnostic ranking is minimized. Our ENTBUG prototype extends the search-based test generation tool EVOSUITE to use entropy in the fitness function of its underlying genetic algorithm, and we applied it to seven real faults. Empirical results show that our approach reduces the entropy of the diagnostic ranking by 49% on average (compared to using the original test suite), leading to a 91% average reduction of diagnosis candidates needed to inspect to find the true faulty one.
José Campos 0001, Rui Abreu 0001, Gordon Fraser 0001, Marcelo d'Amorim
ASE4
2013 SPLat: lightweight dynamic analysis for reducing combinatorics in testing configurable systems
abstract
Many programs can be configured through dynamic and/or static selection of configuration variables. A software product line (SPL), for example, specifies a family of programs where each program is defined by a unique combination of features. Systematically testing SPL programs is expensive as it can require running each test against a combinatorial number of configurations. Fortunately, a test is often independent of many configuration variables and need not be run against every combination. Configurations that are not required for a test can be pruned from execution. This paper presents SPLat, a new way to dynamically prune irrelevant configurations: the configurations to run for a test can be determined during test execution by monitoring accesses to configuration variables. SPLat achieves an optimal reduction in the number of configurations and is lightweight compared to prior work that used static analysis and heavyweight dynamic execution. Experimental results on 10 SPLs written in Java show that SPLat substantially reduces the total test execution time in many cases. Moreover, we demonstrate the scalability of SPLat by applying it to a large industrial code base written in Ruby on Rails.
Chang Hwan Peter Kim, Darko Marinov, Sarfraz Khurshid, Don S. Batory, Sabrina Souto, Paulo Barros, Marcelo d'Amorim
ESEC/SIGSOFT FSE7
2012 Symbolic Execution with Interval Solving and Meta-heuristic Search
abstract
A challenging problem in symbolic execution is to solve complex mathematical constraints such as constraints that include floating-point variables and transcendental functions. The inability to solve such constraints limit the application scope of symbolic execution. In this paper, we present a new method to solve such complex math constraints. Our method combines two existing: meta-heuristic search and interval solving. Conceptually, the combination explores the synergy of the individual methods to improve constraint solving. We implemented the new method in the CORAL constraint-solving infrastructure, and evaluated its effectiveness on a set of publicly-available software from the aerospace domain. Results indicate that the new method can solve significantly more complex mathematical constraints than previous techniques.
Mateus Borges, Marcelo d'Amorim, Saswat Anand, David H. Bushnell, Corina Pasareanu
ICST2
2011 Tainted Flow Analysis on e-SSA-Form Programs
Andrei Rimsa, Marcelo d'Amorim, Fernando Magno Quintão Pereira
CC2
2011 Fault-localization using dynamic slicing and change impact analysis
abstract
Spectrum-based fault-localization tools, such as Tarantula, have been developed to help guide developers towards faulty statements in a system under test. These tools report statements ranked in order of suspiciousness. Unfortunately, the reported statements can often be unrelated to the error. This paper evaluates the impact of several approaches to ignoring such unrelated statements in order to improve the effectiveness of fault-localization tools.
Elton Alves, Milos Gligoric 0001, Vilas Jagannath, Marcelo d'Amorim
ASE4
2009 An Empirical Evaluation of Automated Black Box Testing Techniques for Crashing GUIs
abstract
This paper reports an empirical evaluation of four black-box testing techniques for crashing programs through their GUI interface: SH, AF, DH, and BxT. The techniques vary in their level of automation and the results they offer. The experiments we conducted quantify execution time and the capability of finding a crash for each technique on 8 different cellular phone configurations with historical (real) errors. The results show that AF and BxT offered better precision (i.e., the fraction of runs that end in a crash out of the total number of runs) than SH and DH (AF and BxT found crashes in all 8 configurations), and BxT crashes the application the fastest more often (5 out of 8 cases). The experiments reveal that the selection of the random seed to AF and BxT results in a high variance of execution time (i.e., the time the technique takes to either crash the application or timeout in 40h): the mean (across 8 phone configurations) of the standard deviation of execution times (for 10 runs per each phone configuration) is 7.79h for AF and 5.21h for BxT. Despite this fact, AF and BxT could crash the application consistently: the mean of the precision (fraction of the 10 runs that results in a crash) is 74% for AF and 69% for BxT.
Cristiano Bertolini, Glaucia Peres, Marcelo d'Amorim, Alexandre Mota 0001
ICST3
2008 State extensions for java pathfinder
abstract
Java PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison. This paper summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.
Tihomir Gvero, Milos Gligoric 0001, Steven Lauterburg, Marcelo d'Amorim, Darko Marinov, Sarfraz Khurshid
ICSE4
2008 Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs
abstract
We present Delta execution, a technique that speeds up state-space exploration of object-oriented programs. State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular the heap. We exploit the fact that many execution paths in state-space exploration partially overlap. Delta execution simultaneously operates on several states/heaps and shares the common parts across the executions, separately executing only the "deltas" where the executions differ. We implemented Delta execution in two model checkers: JPF, a popular general-purpose model checker for Java programs, and BOX, a specialized model checker that we developed for efficient exploration of sequential Java programs. The results for bounded-exhaustive exploration of ten basic subject programs and one larger case study show that Delta execution reduces exploration time from 1.06x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX. The results for a non-exhaustive exploration in JPF show that Delta execution reduces exploration time from 0.92x to 6.28x (with median 4.52x).
Marcelo d'Amorim, Steven Lauterburg, Darko Marinov
IEEE Trans. Software Eng.1
2007 Delta execution for efficient state-space exploration of object-oriented programs
abstract
State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular the heap. Previous research has focused on standard program execution that operates on one state/heap. We present Delta Execution, a technique that simultaneously operates on several states/heaps. It exploits the fact that many execution paths in state-space exploration partially overlap and speeds up the exploration by sharing the common parts across the executions and separately executing only the "deltas" where the executions differ.
Marcelo d'Amorim, Steven Lauterburg, Darko Marinov
ISSTA1
2006 Optimized Execution of Deterministic Blocks in Java PathFinder
Marcelo d'Amorim, Ahmed Sobeih, Darko Marinov
ICFEM1
2006 An Empirical Comparison of Automated Generation and Classification Techniques for Object-Oriented Unit Testing
abstract
Testing involves two major activities: generating test inputs and determining whether they reveal faults. Automated test generation techniques include random generation and symbolic execution. Automated test classification techniques include ones based on uncaught exceptions and violations of operational models inferred from manually provided tests. Previous research on unit testing for object-oriented programs developed three pairs of these techniques: model-based random testing, exception-based random testing, and exception-based symbolic testing. We develop a novel pair, model-based symbolic testing. We also empirically compare all four pairs of these generation and classification techniques. The results show that the pairs are complementary (i.e., reveal faults differently), with their respective strengths and weaknesses
Marcelo d'Amorim, Carlos Pacheco, Tao Xie 0001, Darko Marinov, Michael D. Ernst
ASE1
2005 Efficient Monitoring of omega-Languages
Marcelo d'Amorim, Grigore Rosu
CAV1
2004 A Formal Monitoring-Based Framework for Software Development and Analysis
Feng Chen 0006, Marcelo d'Amorim, Grigore Rosu
ICFEM2