Publications | José Miguel Rojas

2025

ASE

Software Testing for Extended Reality Applications: A Systematic Mapping Study

Ruizhen Gu, José Miguel Rojas, and Donghwan Shin

Automated Software Engineering (ASE), 2025

DOI
ICST

Can test generation and program repair inform automated assessment of programming projects?

Ruizhen Gu, José Miguel Rojas, and Donghwan Shin

In IEEE International Conference on Software Testing, Verification and Validation (ICST), 2025

DOI

2024

NLBSE

What’s in a Display Name? An Empirical Study on the Use of Display Names in Open-Source JUnit Tests

Yining Qiao and José Miguel Rojas

In Proceedings of the Third ACM/IEEE International Workshop on NL-Based Software Engineering, 2024

DOI
ICSME

Private-Keep Out? Understanding How Developers Account for Code Visibility in Unit Testing

Muhammad Firhard Roslan, José Miguel Rojas, and Phil McMinn

In 2024 IEEE International Conference on Software Maintenance and Evolution (ICSME), 2024

DOI
ICSME

Viscount: A Direct Method Call Coverage Tool for Java

Muhammad Firhard Roslan, José Miguel Rojas, and Phil McMinn

In 2024 IEEE International Conference on Software Maintenance and Evolution (ICSME), 2024

DOI
FSE

Bounding Random Test Set Size with Computational Learning Theory

Neil Walkinshaw, Michael Foster, José Miguel Rojas, and 1 more author

Proc. ACM Softw. Eng., 2024

DOI

2023

An Empirical Study on the Adoption of Scripted GUI Testing for Android Apps

Ruizhen Gu and José Miguel Rojas

In 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023 - Workshops, 2023

2022

SSBSE

An Empirical Comparison of EvoSuite and DSpot for Improving Developer-Written Test Suites with Respect to Mutation Score

Muhammad Firhard Roslan, José Miguel Rojas, and Phil McMinn

In Search-Based Software Engineering - 14th International Symposium, SSBSE 2022, 2022
AST

On the feasibility and challenges of synthesizing executable Espresso tests

Iván Arcuschin Moreno, Juan Pablo Galeotti, Christian Ciccaroni, and 1 more author

In IEEE/ACM International Conference on Automation of Software Test, AST@ICSE 2022, 2022

DOI

2020

ICSTW

Teaching Software Testing with the Code Defenders Testing Game: Experiences and Improvements

Gordon Fraser, Alessio Gambi, and José Miguel Rojas

In 13th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2020, Porto, Portugal, October 24-28, 2020, 2020

DOI

2019

SIGCSE

Gamifying a Software Testing Course with Code Defenders

Gordon Fraser, Alessio Gambi, Marvin Kreis, and 1 more author

In ACM Technical Symposium on Computer Science Education, (SIGCSE), 2019
Software Testing

Gordon Fraser and José Miguel Rojas

In Handbook of Software Engineering, 2019

PDF

2018

A Preliminary Report on Gamifying a Software Testing Course with the Code Defenders Testing Game

Gordon Fraser, Alessio Gambi, and José Miguel Rojas

In European Conference of Software Engineering Education (ECSEE), 2018

DOI
SBST

EvoSuite at the SBST 2018 tool competition

Gordon Fraser, José Miguel Rojas, and Andrea Arcuri

In Int. Workshop on Search-Based Software Testing (SBST), 2018

DOI
STVR

Random or Evolutionary Search for Object-Oriented Test Suite Generation?

Sina Shamshiri, José Miguel Rojas, Luca Gazzola, and 4 more authors

Software Testing, Verification and Reliability (STVR), 2018

Abs DOI

An important aim in software testing is constructing a test suite with high structural code coverage, that is, ensuring that most if not all of the code under test have been executed by the test cases comprising the test suite. Several search-based techniques have proved successful at automatically generating tests that achieve high coverage. However, despite the well-established arguments behind using evolutionary search algorithms (eg, genetic algorithms) in preference to random search, it remains an open question whether the benefits can actually be observed in practice when generating unit test suites for object-oriented classes. In this paper, we report an empirical study on the effects of using evolutionary algorithms (including a genetic algorithm and chemical reaction optimization) to generate test suites, compared with generating test suites incrementally with random search. We apply the EVOSUITE unit test suite generator to 1000 classes randomly selected from the SF110 corpus of open-source projects. Surprisingly, the results show that the difference is much smaller than one might expect: While evolutionary search covers more branches of the type where standard fitness functions provide guidance, we observed that, in practice, the vast majority of branches do not provide any guidance to the search. These results suggest that, although evolutionary algorithms are more effective at covering complex branches, a random search may suffice to achieve high coverage of most object-oriented classes.
ICST

Automated Accessibility Testing of Mobile Apps

Yan Ge Marcelo Medeiros Eler and Gordon Fraser

In IEEE Int. Conference on Software Testing, Verification and Validation (ICST), 2018

AWARD Abs DOI

Facebook Testing and Verification Research Award 2018

It is important to make mobile apps accessible, so as not to exclude users with common disabilities such as blindness, low vision, or color blindness. Even when developers are aware of these accessibility needs, the lack of tool support makes the development and assessment of accessible apps challenging. Some accessibility properties can be checked statically, but user interface widgets are often created dynamically and are not amenable to static checking. Some accessibility checking frameworks analyze accessibility properties at runtime, but have to rely on existing thorough test suites. In this paper, we introduce the idea of using automated test generation to explore the accessibility of mobile apps. We present the MATE tool (Mobile Accessibility Testing), which automatically explores apps while applying different checks for accessibility issues related to visual impairment. For each issue, MATE generates a detailed report that supports the developer in fixing the issue. Experiments on a sample of 73 apps demonstrate that MATE detects more basic accessibility problems than static analysis, and many additional types of accessibility problems that cannot be detected statically at all. Comparison with existing accessibility testing frameworks demonstrates that the independence of an existing test suite leads to the identification of many more accessibility problems. Even when enabling Android’s assistive features like contrast enhancement, MATE can still find many accessibility issues.
ICST

How Do Automatically Generated Unit Tests Influence Software Maintenance?

Sina Shamshiri, José Miguel Rojas, Juan Pablo Galeotti, and 2 more authors

In IEEE Int. Conference on Software Testing, Verification and Validation (ICST), 2018

Abs DOI

Generating unit tests automatically saves time over writing tests manually and can lead to higher code coverage. However, automatically generated tests are usually not based on realistic scenarios, and are therefore generally considered to be less readable. This places a question mark over their practical value: Every time a test fails, a developer has to decide whether this failure has revealed a regression fault in the program under test, or whether the test itself needs to be updated. Does the fact that automatically generated tests are harder to read outweigh the time-savings gained by their automated generation, and render them more of a hindrance than a help for software maintenance? In order to answer this question, we performed an empirical study in which participants were presented with an automatically generated or manually written failing test, and were asked to identify and fix the cause of the failure. Our experiment and two replications resulted in a total of 150 data points based on 75 participants. Whilst maintenance activities take longer when working with automatically generated tests, we found developers to be equally effective with manually written and automatically generated tests. This has implications on how automated test generation is best used in practice, and it indicates a need for research into the generation of more realistic tests.

2017

ISSTA

Generating Unit Tests with Descriptive Names Or: Would You Name Your Children Thing1 and Thing2?

Ermira Daka, José Miguel Rojas, and Gordon Fraser

In ACM Int. Symposium on Software Testing and Analysis (ISSTA), 2017

Abs DOI

The name of a unit test helps developers to understand the purpose and scenario of the test, and test names support developers when navigating amongst sets of unit tests. When unit tests are generated automatically, however, they tend to be given non-descriptive names such as “test0”, which provide none of the benefits a descriptive name can give a test. The underlying challenge is that automatically generated tests typically do not represent real scenarios and have no clear purpose other than covering code, which makes naming them difficult. In this paper, we present an automated approach which generates descriptive names for automatically generated unit tests by summarizing API-level coverage goals. The tests are optimized to be short, descriptive of the test, have a clear relation to the covered code under test, and allow developers to uniquely distinguish tests in a test suite. An empirical evaluation with 47 participants shows that developers agree with the synthesized names, and the synthesized names are equally descriptive as manually written names. Study participants were even more accurate and faster at matching code and tests with synthesized names compared to manually derived names.
SBST

EvoSuite at the SBST 2017 Tool Competition

Gordon Fraser, José Miguel Rojas, Jose Campos, and 1 more author

In Int. Workshop on Search-Based Software Testing (SBST), 2017

Abs DOI

EvoSuite is a search-based tool that automatically generates unit tests for Java code. This paper summarises the results and experiences of EvoSuite’s participation at the fifth unit testing competition at SBST 2017, where EvoSuite achieved the highest overall score.
SBST

Is Search-based Test Generation Research Stuck in a Local Optimum?

José Miguel Rojas and Gordon Fraser

In Int. Workshop on Search-Based Software Testing (SBST), 2017

Abs DOI

Research in search-based unit test generation has seen steady development in recent years. New techniques and tools have been developed, and empirical evidence has been collected on the wide-ranging capabilities of search-based algorithms for unit test generation, and for many related software engineering practices. But why are developers not generating all their tests automatically yet in practice? In this paper, we argue that there may be deceiving local optima in the research landscape on search-based unit test generation, and we outline specific challenges and opportunities to escape these local optima.
ICSE

Teaching Software Testing Concepts Using a Mutation Testing Game

Benjamin Clegg, José Miguel Rojas, and Gordon Fraser

In Int. Conference on Software Engineering (ICSE)(SEET), 2017

Abs DOI

Software testing is a core aspect of software development, but testing programs systematically is not always a core aspect of software engineering education. As a result, software developers often treat testing as a liability, and overall software quality suffers. One of the reasons for this is that standard testing techniques are often perceived as boring and difficult when compared to creative programming and design activities, which dominate education. To make software testing education more enjoyable, we recently introduced the Code Defenders game, in which players engage with testing activities in a fun and competitive way. In this short paper, we explore the idea of using Code Defenders to systematically teach software testing concepts. We present a mapping of core developer testing concepts, such as statement or branch coverage, to categories of puzzles in the framework of the game. As players progress through levels of this game, they incrementally learn and practice testing concepts. By presenting software testing as an enjoyable activity, we hope that learners will not only acquire better testing skills, but will in the long term become better software engineers.
ICSE

Code Defenders: Crowdsourcing Effective Tests and Subtle Mutants with a Mutation Testing Game

José Miguel Rojas, Thomas White, Benjamin Clegg, and 1 more author

In Int. Conference on Software Engineering (ICSE), 2017

AWARD Abs DOI

ACM Distinguished Paper Award

Writing good software tests is difficult and not every developer’s favorite occupation. Mutation testing aims to help by seeding artificial faults (mutants) that good tests should identify, and test generation tools help by providing automatically generated tests. However, mutation tools tend to produce huge numbers of mutants, many of which are trivial, redundant, or semantically equivalent to the original program; automated test generation tools tend to produce tests that achieve good code coverage, but are otherwise weak and have no clear purpose. In this paper, we present an approach based on gamification and crowdsourcing to produce better software tests and mutants: The Code Defenders web-based game lets teams of players compete over a program, where attackers try to create subtle mutants, which the defenders try to counter by writing strong tests. Experiments in controlled and crowdsourced scenarios reveal that writing tests as part of the game is more enjoyable, and that playing Code Defenders results in stronger test suites and mutants than those produced by automated tools.

2016

Teaching Software Testing with a Mutation Testing Game

José Miguel Rojas and Gordon Fraser

In Psychology of Programming Interest Group 2016 (PPIG), 2016

No formal proceedings.

Abs

Software testing is crucially important in a world dominated by software. Software testing is also inherently difficult and requires theoretical expertise and practical experience. However, standard testing techniques are often perceived as boring and difficult, and thus do not feature as prominently in programming education as they maybe should. In order to address this problem, we aim to make testing education more interesting with gamification. The Code Defenders game uses gameplay elements to engage students in the testing process in a competitive and fun way. Our hope is that if students perceive writing tests as a fun activity, they will later become better software engineers, with better testing skills, and with more inclination to apply thorough testing. In this work-in-progress paper we describe our initial experiences with Code Defenders, as well as open challenges on the way to making testing education fun.
Teaching Mutation Testing using Gamification

José Miguel Rojas and Gordon Fraser

In European Conference of Software Engineering Education (ECSEE), 2016

Abs

Software quality and testing are at the heart of software engineering, but they are not always at the heart of software engineering education. As a consequence, advanced techniques such as \emphmutation testing are often neglected and do not become part of the standard repertoire of a graduate software engineer. We propose the use of gamification to teach mutation testing and to strengthen testing skills. We introduce Code Defenders, a mutation testing game, which can assist educators in delivering complex mutation testing concepts and is intended to make the learning experience more enjoyable and fruitful for students.
Code Defenders: A Mutation Testing Game

José Miguel Rojas and Gordon Fraser

In Int. Conference on Software Testing, Verification and Validation Workshops (MUTATION ICSTW), 2016

Abs DOI

Mutation testing is endorsed by software testing researchers for its unique capability of providing pragmatic estimates of a test suite’s fault detection capability, and for guiding testers in improving their test suites. In practice, however, wide-spread adoption of mutation testing is hampered because any non-trivial program results in huge numbers of mutants, many of which are either trivial or equivalent, and thus useless. Trivial mutants reduce the motivation of developers in trusting and using the technique, while equivalent mutants are frustratingly difficult to handle. These problems are exacerbated by insufficient education on testing, which often means that mutation testing is not well understood in practice. These are examples of the types of problems that \emphgamification aims to overcome by making such tedious activities competitive and entertaining. In this paper, we introduce the first steps towards building Code Defenders, a mutation testing game where players take the role of an \emphattacker, who aims to create the most subtle non-equivalent mutants, or a \emphdefender, who aims to create strong tests to kill these mutants. The benefits of such an approach are manifold: The game can serve an educational role by engaging learners in mutation testing activities in a fun way. Experienced players will produce strong test suites, capable of detecting even the most subtle bugs that other players can conceive. Equivalent mutants are handled by making them a special part of the gameplay, where points are at stake in duels between attackers and defenders.
STVR

Seeding strategies in search-based unit test generation

José Miguel Rojas, Gordon Fraser, and Andrea Arcuri

Software Testing, Verification and Reliability (STVR), 2016

Abs DOI

Search-based techniques have been applied successfully to the task of generating unit tests for object-oriented software. However, as for any meta-heuristic search, the efficiency heavily depends on many factors; \emphseeding, which refers to the use of previous related knowledge to help solve the testing problem at hand, is one such factor that may strongly influence this efficiency. This paper investigates different seeding strategies for unit test generation, in particular seeding of numerical and string constants derived statically and dynamically, seeding of type information, and seeding of previously generated tests. To understand the effects of these seeding strategies, the results of a large empirical analysis carried out on a large collection of open source projects from the SF110 corpus and the Apache Commons repository are reported. These experiments show with strong statistical confidence that, even for a testing tool already able to achieve high coverage, the use of appropriate seeding strategies can further improve performance.
EMSE

A detailed investigation of the effectiveness of whole test suite generation

José Miguel Rojas, Mattia Vivanti, Andrea Arcuri, and 1 more author

Empirical Software Engineering (EMSE), 2016

Abs DOI

A common application of search-based software testing is to generate test cases for all goals defined by a coverage criterion (e.g., lines, branches, mutants). Rather than generating one test case at a time for each of these goals individually, whole test suite generation optimizes entire test suites towards satisfying all goals at the same time. There is evidence that the overall coverage achieved with this approach is superior to that of targeting individual coverage goals. Nevertheless, there remains some uncertainty on (a) whether the results generalize beyond branch coverage, (b) whether the whole test suite approach might be inferior to a more focused search for some particular coverage goals, and (c) whether generating whole test suites could be optimized by only targeting coverage goals not already covered. In this paper, we perform an in-depth analysis to study these questions. An empirical study on 100 Java classes using three different coverage criteria reveals that indeed there are some testing goals that are only covered by the traditional approach, although their number is only very small in comparison with those which are exclusively covered by the whole test suite approach. We find that keeping an archive of already covered goals along with the tests covering them and focusing the search on uncovered goals overcomes this small drawback on larger classes, leading to an improved overall effectiveness of whole test suite generation.

2015

ASE

Do Automatically Generated Unit Tests Find Real Faults? An Empirical Study of Effectiveness and Challenges

Sina Shamshiri, René Just, José Miguel Rojas, and 3 more authors

In IEEE/ACM Int. Conference on Automated Software Engineering (ASE), 2015

AWARD Abs

ACM SIGSOFT Distinguished Paper Award

Rather than tediously writing unit tests manually, tools can be used to generate them automatically — sometimes even resulting in higher code coverage than manual testing. But how good are these tests at actually finding faults? To answer this question, we applied three state-of-the-art unit test generation tools for Java (Randoop, EvoSuite, and Agitar) to the 357 real faults in the Defects4J dataset and investigated how well the generated test suites perform at detecting these faults. Although the automatically generated test suites detected 55.7% of the faults overall, only 19.9% of all the individual test suites detected a fault. By studying the effectiveness and problems of the individual tools and the tests they generate, we derive insights to support the development of automated unit test generators that achieve a higher fault detection rate. These insights include 1) improving the obtained code coverage so that faulty statements are executed in the first instance, 2) improving the propagation of faulty program states to an observable output, coupled with the generation of more sensitive assertions, and 3) improving the simulation of the execution environment to detect faults that are dependent on external factors such as date and time.
GECCO

Random or Genetic Algorithm Search for Object-Oriented Test Suite Generation?

Sina Shamshiri, José Miguel Rojas, Gordon Fraser, and 1 more author

In Genetic and Evolutionary Computation Conference (GECCO), 2015

AWARD Abs DOI

Best Paper Award (SBSE-SS Track)

Achieving high structural coverage is an important aim in software testing. Several search-based techniques have proved successful at automatically generating tests that achieve high coverage. However, despite the well-established arguments behind using evolutionary search algorithms (e.g., genetic algorithms) in preference to random search, it remains an open question whether the benefits can actually be observed in practice when generating unit test suites for object-oriented classes. In this paper, we report an empirical study on the effects of using a genetic algorithm (GA) to generate test suites over generating test suites incrementally with random search, by applying the EvoSuite unit test suite generator to 1,000 classes randomly selected from the SF110 corpus of open source projects. Surprisingly, the results show little difference between the coverage achieved by test suites generated with evolutionary search compared to those generated using random search. A detailed analysis reveals that the genetic algorithm covers more branches of the type where standard fitness functions provide guidance. In practice, however, we observed that the vast majority of branches in the analyzed projects provide no such guidance.
ISSTA

Automated unit test generation during software development: a controlled experiment and think-aloud observations

José Miguel Rojas, Gordon Fraser, and Andrea Arcuri

In ACM Int. Symposium on Software Testing and Analysis (ISSTA), 2015

Abs DOI

Automated unit test generation tools can produce tests that are superior to manually written ones in terms of code coverage, but are these tests helpful to developers \emphwhile they are writing code? A developer would first need to know when and how to apply such a tool, and would then need to understand the resulting tests in order to provide test oracles and to diagnose and fix any faults that the tests reveal. Considering all this, does automatically generating unit tests provide any benefit over simply writing unit tests manually? We empirically investigated the effects of using an automated unit test generation tool (EvoSuite) during development. A controlled experiment with 41 students shows that using EvoSuite leads to an average branch coverage increase of +13%, and 36% less time is spent on testing compared to writing unit tests manually. However, there is no clear effect on the quality of the implementations, as it depends on how the test generation tool and the generated tests are used. In-depth analysis, using five think-aloud observations with professional programmers, confirms the necessity to increase the \emphusability of automated unit test generation tools, to \emphintegrate them better during software development, and to \empheducate software developers on how to best use those tools.
SSBSE

Combining Multiple Coverage Criteria in Search-Based Unit Test Generation

José Miguel Rojas, José Campos, Mattia Vivanti, and 2 more authors

In Int. Symposium on Search Based Software Engineering (SSBSE), 2015

AWARD Abs DOI

Best Paper Award (Industry-relevant SBSE results)

Automated test generation techniques typically aim at maximising coverage of well-established structural criteria such as statement or branch coverage. In practice, generating tests only for one specific criterion may not be sufficient when testing object oriented classes, as standard structural coverage criteria do not fully capture the properties developers may desire of their unit test suites. For example, covering a large number of statements could be easily achieved by just calling the \tt main method of a class; yet, a good unit test suite would consist of smaller unit tests invoking individual methods, and checking return values and states with test assertions. There are several different properties that test suites should exhibit, and a search-based test generator could easily be extended with additional fitness functions to capture these properties. However, does search-based testing scale to combinations of multiple criteria, and what is the effect on the size and coverage of the resulting test suites? To answer these questions, we extended the EvoSuite unit test generation tool to support combinations of multiple test criteria, defined and implemented several different criteria, and applied combinations of criteria to a sample of 650 open source Java classes. Our experiments suggest that optimising for several criteria at the same time is feasible without increasing computational costs: When combining nine different criteria, we observed an average decrease of only 0.4% for the constituent coverage criteria, while the test suites may grow up to 70%.

2014

Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency

Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, and 1 more author

In 14th Int. School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM Advanced Lectures), 2014

Abs PDF

The focus of this tutorial is white-box test case generation (TCG) based on symbolic execution. Symbolic execution consists in executing a program with the contents of its input arguments being symbolic variables rather than concrete values. A symbolic execution tree characterizes the set of execution paths explored during the symbolic execution of a program. Test cases can be then obtained from the successful branches of the tree. The tutorial is split into three parts: (1) The first part overviews the basic techniques used in TCG to ensure termination, handling heap-manipulating programs, achieving compositionality in the process and guiding TCG towards interesting test cases. (2) In the second part, we focus on a particular implementation of the TCG framework in constraint logic programming (CLP). In essense, the imperative object-oriented program under test is automatically transformed into an equivalent executable CLP-translated program. The main advantage of CLP-based TCG is that the standard mechanism of CLP performs symbolic execution for free. The PET system is an open-source software that implements this approach. (3) Finally, in the last part, we study the extension of TCG to actor-based concurrent programs.

2013

Test Case Generation in Object-Oriented Programming

José Miguel Rojas

Universidad Politécnica de Madrid (Technical University of Madrid), Dec 2013

Abs

Testing is nowadays the most used technique to validate software and assess its quality. It is integrated into all practical software development methodologies and plays a crucial role towards the success of any software project. From the smallest units of code to the most complex components and their integration into a software system and later deployment; all pieces of a software product must be tested thoroughly before a software product can be released. The main limitation of software testing is that it remains a mostly manual task, representing a large fraction of the total development cost. In this scenario, test automation is paramount to alleviate such high costs. Test case generation (TCG) is the process of automatically generating test inputs that achieve high coverage of the system under test. Among a wide variety of approaches to TCG, this thesis focuses on structural (white-box) TCG, where one of the most successful enabling techniques is symbolic execution. In symbolic execution, the program under test is executed with its input arguments being symbolic expressions rather than concrete values. This thesis relies on a previously developed constraint-based TCG framework for imperative object-oriented programs (e.g., Java), in which the imperative program under test is first translated into an equivalent constraint logic program, and then such a translated program is symbolically executed by relying on standard evaluation mechanisms of Constraint Logic Programming (CLP), extended with special treatment for dynamically allocated data structures. Improving the scalability and efficiency of symbolic execution constitutes a major challenge. It is well known that symbolic execution quickly becomes impractical due to the large number of paths that must be explored and the size of the constraints that must be handled. Moreover, symbolic execution-based TCG tends to produce an unnecessarily large number of test cases when applied to medium or large programs. The contributions of this dissertation can be summarized as follows. \beginitemize \item[(1)] A compositional approach to CLP-based TCG is developed which overcomes the inter-procedural path explosion by separately analyzing each component (method) in a program under test, stowing the results as method summaries and incrementally reusing them to obtain whole-program results. A similar compositional strategy that relies on program specialization is also developed for the state-of-the-art symbolic execution tool Symbolic PathFinder (SPF). \item[(2)] Resource-driven TCG is proposed as a methodology to use resource consumption information to drive symbolic execution towards those parts of the program under test that comply with a user-provided resource policy, avoiding the exploration of those parts of the program that violate such policy. \item[(3)] A generic methodology to guide symbolic execution towards the most interesting parts of a program is proposed, which uses abstractions as oracles to steer symbolic execution through those parts of the program under test that interest the programmer/tester most. \item[(4)] A new heap-constraint solver is proposed, which efficiently handles heap-related constraints and aliasing of references during symbolic execution and greatly outperforms the state-of-the-art standard technique known as lazy initialization. \item[(5)] All techniques above have been implemented in the PET system (and some of them in the SPF tool). Experimental evaluation has confirmed that they significantly help towards a more scalable and efficient symbolic execution and TCG. \enditemize
ICLP

A CLP Heap Solver for Test Case Generation

Elvira Albert, María García Banda, Miguel Gómez-Zamalloa, and 2 more authors

Theory and Practice of Logic Programming (TPLP) (ICLP 2013 SI.), 2013

Abs PDF

One of the main challenges to software testing today is to efficiently handle heap-manipulating programs. These programs often build complex, dynamically allocated data structures during execution and, to ensure reliability, the testing process needs to consider all possible shapes these data structures can take. This creates scalability issues since high (often exponential) numbers of shapes may be built due to the \emphaliasing of references. This paper presents a novel \emphCLP heap solver for the test case generation of heap-manipulating programs that is more scalable than previous proposals, thanks to the treatment of reference aliasing by means of \emphdisjunction, and to the use of advanced \emphback-propagation of heap related constraints. In addition, the heap solver supports the use of \emphheap assumptions to avoid aliasing of data that, though legal, should not be provided as input.
Compositional Symbolic Execution through Program Specialization

José Miguel Rojas and Corina S. Păsăreanu

In BYTECODE 2013, 2013

Peer-reviewed workshop (co-located with ETAPS 2013) with no formal proceedings.

Abs

Scalability is a major challenge in symbolic execution. The large number of paths that need to be explored and the large size of the constraints that must be carried often compromise the effectiveness of symbolic execution for software testing in practice. Compositional symbolic execution aims to alleviate these scalability issues by executing the methods of a program separately, stowing their results in method summaries and using such summaries to incrementally execute the complete program. We present a novel compositional approach that leverages partial evaluation, a well-established technique that aims at automatically specializing a program with respect to some of its input. We report on its design and implementation in Symbolic PathFinder and on preliminary promising evaluation results.
In
LOPSTR

A Framework for Guided Test Case Generation in Constraint Logic Programming

José Miguel Rojas and Miguel Gómez-Zamalloa

In Int. Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2013

Abs DOI PDF

It is well known that performing test case generation by symbolic execution on large programs becomes quickly impracticable due to the path explosion phenomenon. This issue is considered a major challenge in the software testing arena. Another common limitation in the field is that test case generation by symbolic execution tends to produce an unnecessarily large number of test cases even for medium size programs. In this paper we propose a constraint logic programming approach to devise a generic framework to guide symbolic execution and thus test case generation. We show how the framework can help alleviate these scalability drawbacks that most symbolic execution-based test generation approaches endure.

2012

Automatic Inference of Bounds on Resource Consumption

Elvira Albert, Diego Esteban Alonso-Blas, Puri Arenas, and 9 more authors

In Int. Symposium on Formal Methods for Components and Objects (FMCO, Revised Lectures), 2012

Abs

In this tutorial paper, we overview the techniques that underlie the automatic inference of resource consumption bounds. We first explain the basic techniques on a Java-like sequential language. Then, we describe the extensions that are required to apply our method on concurrent ABS programs. Finally, we discuss some advanced issues in resource analysis, including the inference of non-cumulative resources and the treatment of shared mutable data.
\sc jms2abs: Automated Extraction of Abstract Behavioural Models from JMS Applications

Elvira Albert, Bjarte M. Østvold, and José Miguel Rojas

In Formal Methods for Industrial Critical Systems (FMICS), 2012

Abs

Distributed systems are hard to program, understand and analyze. Two key sources of complexity are the many possible behaviors of a system, arising from the parallel execution of its distributed nodes, and the handling of asynchronous messages exchanged between nodes. We show how to systematically construct \emphexecutable models of publish/subscribe systems based on the Java Messaging Service (JMS). These models, written in the Abstract Behavioural Specification (ABS) language, capture the essentials of the messaging behavior of the original Java systems, and eliminate details not related to distribution and messages. We report on \sc jms2abs, a tool that automatically extracts ABS models from the \emphbytecode of JMS systems. Since the extracted models are formal and executable, they allow us to reason about the modeled JMS systems by means of tools built specifically for the modeling language. For example, we have succeeded to apply simulation, termination and resource analysis tools developed for ABS to, respectively, execute, prove termination and infer the resource consumption of the original JMS applications.
LOPSTR

Resource-driven CLP-based Test Case Generation

Elvira Albert, Miguel Gómez-Zamalloa, and José Miguel Rojas

In Int. Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2012

Abs

Test Data Generation (TDG) aims at automatically obtaining test inputs which can then be used by a software testing tool to validate the functional behaviour of the program. In this paper, we propose \emphresource-aware TDG, whose purpose is to generate test cases (from which the test inputs are obtained) with associated resource consumptions. The framework is parametric w.r.t. the notion of resource (it can measure memory, steps, etc.) and allows using software testing to detect bugs related to non-functional aspects of the program. As a further step, we introduce \emphresource-driven TDG whose purpose is to guide the TDG process by taking resource consumption into account. Interestingly, given a \emphresource policy, TDG is guided to generate test cases that adhere to the policy and avoid the generation of test cases which violate it.
Resource Analysis in the COSTA System

Elvira Albert, Diego Esteban Alonso, Puri Arenas, and 9 more authors

Dec 2012

Newsletter

Abs PDF

Having information about the execution cost of programs, i.e., the amount of resources that the execution will require, is useful for many different purposes, including program optimization, verification and certification. Reasoning about execution cost is difficult and error-prone. Therefore, it is widely recognized that cost analysis, sometimes also referred to as resource analysis or automatic complexity analysis, is quite important. COSTA (\urlhttp://costa.ls.fi.upm.es) is a state-of-the-art cost and termination analyzer which automates this task. The system is able to infer upper and lower bounds on the resource consumption of a large class of programs. Given a program P, the analysis results allow bounding the cost of executing P on any input data \overlinex without having to actually run P(\overlinex). The first successful proposal for automatically computing the complexity of programs was the seminal work of Wegbreit. Since then, a number of cost analysis frameworks have been proposed, mostly in the context of declarative programming languages (functional programming and logic programming). Cost analysis of imperative programming languages has received significantly less attention. It is worth mentioning the pioneering work of Adachi et al. To the best of our knowledge, COSTA has been the first system which automatically infers bounds on cost for a large class of Java-like programs, getting meaningful results. The system is implemented in Prolog (it runs both on Ciao and SWI Prolog) and uses the Parma Polyhedra Library for manipulating linear constraints. More info on COSTA is available from its website, where it can be used from a web interface.

2011

Parallel Simulation of NEPs on Clusters

Carmen Navarrete, Marina Cruz, Eloy Anguiano, and 2 more authors

In IEEE/WIC/ACM Int. Conferences on Web Intelligence and Intelligent Agent Technology (WI-IAT), 2011

Abs DOI

This paper compares two different approaches, followed by our research group, to efficiently run NEPs on parallel platforms, as general and transparent as possible. The vague results of jNEP (our multithreaded Java simulator for multicore desktop computers) suggests the use of massively parallel platforms (clusters of computers). The good results obtained show the scalability and viability of this last approach.
LOPSTR

Compositional CLP-Based Test Data Generation for Imperative Languages

Elvira Albert, Miguel Gómez-Zamalloa, José Miguel Rojas, and 1 more author

In Int. Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), 2011

Abs PDF

Glass-box test data generation (TDG) is the process of automatically generating test input data for a program by considering its internal structure. This is generally accomplished by performing symbolic execution of the program where the contents of variables are expressions rather than concrete values. The main idea in CLP-based TDG is to translate imperative programs into equivalent CLP ones and then rely on the standard evaluation mechanism of CLP to symbolically execute the imperative program. Performing symbolic execution on large programs becomes quickly expensive due to the large number and the size of paths that need to be explored. In this paper, we propose \emphcompositional reasoning in CLP-based TDG where large programs can be handled by testing parts (such as components, modules, libraries, methods, etc.) separately and then by composing the test cases obtained for these parts to get the required information on the whole program. Importantly, compositional reasoning also gives us a practical solution to handle native code, which may be unavailable or written in a different programming language. Namely, we can model the behavior of a native method by means of test cases and compositional reasoning is able to use them.

2010

Towards the Automatic Programming of H Systems: jHsys, a Java H System Simulator

José Miguel Rojas, Marina Cruz Echeandı́a, and Alfonso Ortega Puente

In Int. Conference on Practical Applications of Agents and Multiagent Systems (PAAMS), 2010

Abs

The main goal of this paper is to describe how we consider that splicing systems (a family of abstract bio-inspired computing devices) can be automatically programmed (designed) in the future. One of the necessary steps is to formally de- scribe the computer being programmed (splicing systems). Some of the authors of this paper have previously solved this problem. Another necessary step is to develop a simulator for H systems. We propose applying Christiansen Grammar Evolution (an evolutionary automatic programming algorithm developed by the authors) to complete the process. This technique includes a fitness function that the simulator requires. This paper is devoted to describe jHSys, a Java simulator for splicing (H) systems.

2009

On the Solutions of NP-Complete Problems by Means of jNEP Run on Computers

Emilio Rosal, José Miguel Rojas, Rafael Núñez, and 2 more authors

In International Conference on Agents and Artificial Intelligence (ICAART), 2009

Abs

We have used jNEP (a JAVA simulator of a natural computing device named Networks of Evolutionary Processors) to solve some cases of well-known NP-complete problems. We have followed the most relevant papers in the literature. In this paper, we describe the difficulties found in this process and some conclusions about the design, the simulation and some useful tools for NEPs.