VLDB 2026 Research / reviewers in the wild / expert
Juliano Iyoda
dblp:72/4526 · also Juliano Manabu Iyoda
· DBLP profile ↗
16ranked-venue papers
0as first author
4since 2021 · last 2026
0000-0001-7137-8287ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 12 · 4 since 2021Theory of computation · 4Databases, data management, data science and information retrieval · 2
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Toward a non-invasive robotic-supported approach for data loss detection in android applicationsabstractContext: Maintaining data consistency in mobile applications is essential, as activity restarts—such as those triggered by screen rotations—can lead to user data loss. Existing automated approaches, including DLD and R-DLD, rely on semi-invasive testing methods that require system-level access through debugging tools like ADB or app instrumentation. These dependencies limit their applicability to specific devices and reduce realism in user interaction. Objective: This work aims to overcome the limitations of semi-invasive data loss detection by introducing a fully non-invasive, hardware-based framework for Android applications. The goal is to preserve the authenticity of user interaction while maintaining detection accuracy comparable to existing approaches. Method: We present a new version of R-DLD, which leverages an industrial robotic arm to reproduce realistic user interactions such as touch gestures, scrolling, and device rotations without system-level access. The oracle was completely redesigned, using an external camera and computer vision techniques that apply similarity and dissimilarity metrics to identify data loss after double rotation events. Results: Experimental evaluation on thirty benchmark Android applications showed that the new R-DLD detected 100% of known data loss cases, matching R-DLD’s performance while operating entirely non-invasively. The results also demonstrate the robustness of the visual oracle against environmental lighting variations. Conclusion: The new R-DLD represents a significant advancement in realistic, non-invasive testing for mobile applications. By eliminating the need for ADB or instrumentation, it broadens the applicability of automated data loss detection and establishes a foundation for future research in vision-based, robotics-supported testing. Davi Freitas, Breno Miranda, Juliano Iyoda |
Inf. Softw. Technol. | 3 |
| 2024 | The effect of distance metrics in a general purpose synthesizer of imperative programs: A second empirical study using enlarged search spacesabstractAbstract Context Program synthesis is the task of automatically finding a program that satisfies the user intention. In previous work, we developed APS‐GA, a program synthesizer based on a genetic algorithm. As genetic algorithms depend on a fitness function, so does APS‐GA. Researchers argue that different distance metrics for a fitness function may reveal behavioral differences in the genetic algorithm. More recently, we presented initial evidence that APS‐GA was not affected by different distance metrics for its fitness function. However, that study was carried out on a medium‐sized scale. Objective In order to investigate our previous study on a larger scale, we extended our experiment to replicate it on a search space that is up to 6500 times larger than our previous work, and we ran it with a synthesis time that was at least 20 times longer. We have chosen the same five distance metrics as fitness functions to check whether they affect the synthesis task of five integer domain imperative toy programs. Method A hypothesis test was proposed and experiments were conducted to observe the number of calls to the fitness function () and to measure the synthesis time (). Results By considering a confidence level of 95% (with ), we found out that there were no significant differences in both and . Conclusion With these results, our extended replication study suggests that the discrete distance metric constitutes the best choice for APS‐GA as it guides the search with the same effectiveness as the other metrics, and is cheaper to compute. Alexandre R. S. Correia, Juliano Iyoda, Alexandre Mota 0001 |
Softw. Pract. Exp. | 2 |
| 2022 | The effect of distance metrics in a general purpose synthesizer: An empirical study on integer domain imperative programsabstractAbstract Context Program synthesis is the task of automatically finding a program that satisfies the user intention. In previous work, we have developed a program synthesizer that integrates genetic algorithm with model finder. A genetic algorithm uses a fitness function to calculate how “distant to a solution” a given candidate program is. Researchers argue that different distance metrics for a fitness function may reveal behavioral differences in the genetic algorithm. Objective We have chosen five distance metrics as fitness functions to check whether they affect the synthesis task of five different integer domain imperative toy‐programs which read/write integer values using fundamental syntactic constructs, such as while, if‐then‐else, and so forth. We have used input/output examples and sketches to constrain the search space of the candidate programs. Method A hypothesis test was proposed and experiments were conducted to observe the number of calls to the fitness function (x) and to measure the synthesis time ( ). Results Regarding x, the synthesizer found a solution for all five subjects after calling the fitness function the same amount of times. For , a one‐way ANOVA was performed with a significance level of 5% ( ). No significant differences were observed in both x and . Conclusion With these preliminary results, this study suggests that the discrete distance metric is the best choice, because it guides the search with the same effectiveness as the others and is not time consuming, and so forth. However, future experimentation with a larger search space will confirm or not this initial impression. Alexandre R. S. Correia, Juliano Iyoda, Alexandre Mota 0001 |
Softw. Pract. Exp. | 2 |
| 2021 | A family of multi-concept program synthesisers in Alloy⁎
Alexandre R. S. Correia, Juliano Iyoda, Alexandre Mota 0001 |
Sci. Comput. Program. | 2 |
| 2020 | Combining model finder and genetic programming into a general purpose automatic program synthesizer
Alexandre R. S. Correia, Juliano Iyoda, Alexandre Mota 0001 |
Inf. Process. Lett. | 2 |
| 2019 | Test case generation, selection and coverage from natural language
Sidney C. Nogueira, Hugo Leonardo da Silva Araujo, Renata B. S. Araujo, Juliano Iyoda, Augusto Sampaio 0001 |
Sci. Comput. Program. | 4 |
| 2017 | Towards Automated Deployment of Self-adaptive Applications on Hybrid Clouds (Short Paper)
Lom-Messan Hillah, Rodrigo Elia Assad, Antonia Bertolino, Márcio Eduardo Delamaro, Fabio De Rosa, Vinicius Cardoso Garcia, Francesca Lonetti, Ariele-Paolo Maesano, Libero Maesano, Eda Marchetti, Breno Miranda, Auri M. R. Vincenzi, Juliano Iyoda |
SEFM | 13 |
| 2017 | An integrated semantics for reasoning about SysML design models using refinement
Lucas Lima 0001, Alvaro Miyazawa, Ana Cavalcanti 0001, Márcio Cornélio, Juliano Iyoda, Augusto Sampaio 0001, Ralph Hains, Adrian Larkham, Vaughan Lewis |
Softw. Syst. Model. | 5 |
| 2016 | Program synthesis by model finding
Alexandre Mota 0001, Juliano Iyoda, Heitor Maranhão |
Inf. Process. Lett. | 2 |
| 2015 | Selected papers from the Brazilian Symposiums on Formal Methods (SBMF 2012 and 2013)
Rohit Gheyi, Juliano Iyoda |
Sci. Comput. Program. | 2 |
| 2014 | A Formal Semantics for Sequence Diagrams and a Strategy for System AnalysisabstractWe propose a semantics for Sequence Diagrams based on the COMPASS Modelling Language (CML): a formal specification language to model systems of systems. A distinguishing feature of our semantics is that it is defined as part of a larger effort to define the semantics of several diagrams of SysML, a UML profile for systems engineering. We have defined a fairly comprehensive semantics for Sequence Diagrams, which comprises sequential and parallel constructors, loops, breaks, alternatives, synchronous and asynchronous messages. We illustrate our semantics with a scenario of a case study of a system of systems. We also discuss an analysis strategy which involves an integrated view of several diagrams. Lucas Lima 0001, Juliano Iyoda, Augusto Sampaio 0001 |
MODELSWARD | 2 |
| 2014 | Compositionality and correctness of fault tolerant patterns in HOL4
Diego Machado Dias, Juliano Iyoda |
Sci. Comput. Program. | 2 |
| 2012 | Recommender systems for manual testing: deciding how to assign tests in a test teamabstractBACKGROUND: Software testing can be an arduous and expensive activity. A typical activity to maximise testing productivity is to allocate test cases according to the testers' profile. However, optimising the allocation of manual test cases is not a trivial task: in big companies, test managers are responsible for allocating hundreds of test cases among several testers. OBJECTIVE: In this paper we propose and evaluate 2 assignment algorithms for test case allocation and 3 tester profiles based on recommender systems. Each assignment algorithm can be combined with 3 tester profiles, which results in six possible allocation systems. METHOD: We run a controlled experiment that uses 100 test suites, each one with at least 50 test cases, from a real industrial setting in order to compare our allocation systems to the manager's allocation in terms of precision, recall and unassignment (percentage of test cases the algorithm could not allocate). RESULTS: In our experiment, the statistical analysis shows that one of the systems outperforms the others with respect to the precision and recall metrics. For unassignment, three of our six allocation systems achieved zero (best value) for the unassignment rate. CONCLUSION: The results of our experiment suggest that, in similar environments, test managers can use our allocation systems to reduce the amount of time spent in the test case allocation task. In the real industrial setting in which our work was developed, managers spend from 16 to 30 working days a year on test case allocation. Our algorithms can help them do it faster and better. Breno Miranda, Eduardo Aranha, Juliano Iyoda |
ESEM | 3 |
| 2011 | Correct hardware synthesis - An algebraic approach
Juan Ignacio Perna, Jim Woodcock 0001, Augusto Sampaio 0001, Juliano Iyoda |
Acta Informatica | 4 |
| 2009 | Test case prioritization based on data reuse an experimental studyabstractThe order in which tests are executed can significantly impact the total test execution time. In this paper, we evaluate two test prioritization techniques (manual and automatic) in the context of mobile phone testing. The manual technique produces test sequences created by test experts, while the automatic one generates sequences mechanically based on the permutation of the tests. Both techniques take into account a data reuse: the more the data is reused among tests, the faster the sequence is executed. In order to evaluate the benefits of these two techniques, we carried out an experiment with 8 testers and 2 test suites arranged in a 2times2 Latin square design replicated four times. The automatic technique reduced approximately 25% of the data generation time and 13.5% of the execution time. The automatic technique is clearly better than the manual one with respect to the generation of sequences. Our experiment showed that the automatic technique also generates sequences whose execution is faster than those created manually by test experts. Lucas Lima 0001, Juliano Iyoda, Augusto Sampaio 0001, Eduardo Aranha |
ESEM | 2 |
| 2007 | Proof producing synthesis of arithmetic and cryptographic hardwareabstractAbstract A compiler from a synthesisable subset of higher order logic to clocked synchronous hardware is described. It is being used to create coprocessors for cryptographic and arithmetic applications. The compiler automatically translates a functionfdefined in higher order logic (typically using recursion) into a device that computesfvia a four-phase handshake circuit. Compilation is by fully automatic proof in the HOL4 system, and generates a correctness theorem for each compiled function. Synthesised circuits can be directly translated to Verilog, and then input to design automation tools. A fully-expansive ‘LCF methodology’ allows users to safely modify and extend the compiler’s theorem proving scripts to add optimisations or to enlarge the synthesisable subset of higher order logic. Konrad Slind, Scott Owens, Juliano Iyoda, Michael J. C. Gordon |
Formal Aspects Comput. | 3 |