VLDB 2026 Research / reviewers in the wild / expert
Jooyong Yi
dblp:121/2697 · also Jooyong Lee
· DBLP profile ↗
26ranked-venue papers
6as first author
10since 2021 · last 2025
0000-0002-7215-0855ORCID · conflict
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 26 · 6 first-author · 10 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Lightweight Concolic Testing via Path-Condition Synthesis for Deep Learning LibrariesabstractMany techniques have been recently developed for testing deep learning (DL) libraries. Although these techniques have effectively improved API and code coverage and detected unknown bugs, they rely on blackbox fuzzing for input generation. Concolic testing (also known as dynamic symbolic execution) can be more effective in exploring diverse execution paths, but applying it to DL libraries is extremely challenging due to their inherent complexity. In this paper, we introduce the first concolic testing technique for DL libraries. Our technique offers a lightweight approach that significantly reduces the heavy overhead associated with traditional concolic testing. While symbolic execution maintains symbolic expressions for every variable with non-concrete values to build a path condition, our technique computes approximate path conditions by inferring branch conditions via inductive program synthesis. Despite potential imprecision from approximation, our method's light overhead allows for effective exploration of diverse execution paths within the complex implementations of DL libraries. We have implemented our tool, Pathfinder, and evaluated it on PyTorch and TensorFlow. Our results show that Pathfinder outperforms existing API-level DL library fuzzers by achieving 67% more branch coverage on average; up to 63% higher than TitanFuzz and 120% higher than FreeFuzz. Pathfinder is also effective in bug detection, uncovering 61 crash bugs, 59 of which were confirmed by developers as previously unknown, with 32 already fixed. Yonghyeon Kim, Dahyeon Park, Yuseok Jeon, Jooyong Yi, Mijung Kim |
ICSE | 5 |
| 2025 | Proactive Debugging of Memory Leakage Bugs in Single Page Web ApplicationsabstractDeveloping modern web applications often relies on web-based application frameworks such as React, Vue.js, and Angular. Although the frameworks accelerate the development of web applications with several useful and predefined components, they are inevitably vulnerable to unmanaged memory consumption as the frameworks often produce monolithic web pages, socalled, Single Page Applications (SPAs), in which no page refresh actions are made during navigation.Web applications can be alive for hours and days with behavior loops, in such cases, even a single memory leak in an SPA can cause performance degradation on the client side. However, recent debugging techniques for web applications focus on memory leak detection, which requires manual tasks and produces imprecise results, rather than proactively repairing memory leaks.We propose LEAKPAIR, a technique to proactively repair memory leaks in SPAs rather than following a classical and reactive debugging process. Given the insight that memory leaks are mostly non-functional bugs and fixing them might not change the behavior of an application, the technique is designed to proactively generate patches to fix memory leaks, without leak detection, which is often heavy and tedious. Thus, the proactive technique can significantly reduce the time and effort necessary to fix the memory leaks. To generate effective patches, LEAKPAIR follows the idea of pattern-based program repair since the automated repair strategy shows successful results in many recent studies. We extensively evaluate the technique on 60 open-source projects without using explicit leak detection. The patches generated by our technique are also submitted to the projects as pull requests (PRs). The results of PRs show that LEAKPAIR can generate effective patches to reduce memory consumption that are acceptable to developers. In addition, we execute the test suites given by the projects after applying the patches, and it turns out that the patches do not cause any functionality breakage; this might imply that LEAKPAIR can generate non-intrusive patches for memory leaks. Furthermore, we compare the performance of LEAKPAIR with that of GPT-4 as recent studies show that large language models are successful with program repair tasks. Our results show that our technique outperforms the language model. Arooba Shahoor, Satbek Abdyldayev, Hyeongi Hong, Jooyong Yi, Dongsun Kim 0001 |
IEEE Trans. Software Eng. | 4 |
| 2024 | Preserving Reactiveness: Understanding and Improving the Debugging Practice of Blocking-Call BugsabstractReactive programming reacts to data items as they occur, rather than waiting for them to complete. This programming paradigm is widely used in asynchronous and event-driven scenarios, such as web applications, microservices, real-time data processing, IoT, interactive UIs, and big data. When done right, it can offer greater responsiveness without extra resource usage. However, this also requires a thorough understanding of asynchronous and non-blocking coding, posing a learning curve for developers new to this style of programming. In this work, we analyze issues reported in reactive applications and explore their corresponding fixes. Our investigation results reveal that (1) developers often do not fix or ignore reactiveness bugs as compared to other bug types, and (2) this tendency is most pronounced for blocking-call bugs -- bugs that block the execution of the program to wait for the operations (typically I/O operations) to finish, wasting CPU and memory resources. To improve the debugging practice of such blocking bugs, we develop a pattern-based proactive program repair technique and obtain 30 patches, which we submit to the developers. In addition, we hypothesize that the low patch acceptance rate for reactiveness bugs is due to the difficulty of assessing the patches. This is in contrast to functionality bugs, where the correctness of the patches can be assessed by running test cases. To assess our hypothesis, we split our patches into two groups: one with performance improvement evidence and the other without. It turns out that the patches are more likely to be accepted when submitted with performance improvement evidence. Arooba Shahoor, Jooyong Yi, Dongsun Kim 0001 |
ISSTA | 2 |
| 2024 | Enhancing the Efficiency of Automated Program Repair via Greybox AnalysisabstractIn this paper, we pay attention to the efficiency of automated program repair (APR). Recently, an efficient patch scheduling algorithm, Casino, has been proposed to improve APR efficiency. Inspired by fuzzing, Casino adaptively chooses the next patch candidate to evaluate based on the results of previous evaluations. However, we observe that Casino utilizes only the test results, treating the patched program as a black box. Inspired by greybox fuzzing, we propose a novel patch-scheduling algorithm, Gresino, which leverages the internal state of the program to further enhance APR efficiency. Specifically, Gresino monitors the hit counts of branches observed during the execution of the program and uses them to guide the search for a valid patch. Our experimental evaluation on the Defects4J benchmark and eight APR tools demonstrates the efficacy of our approach. Yechan Park, Seungheon Han, Jooyong Yi |
ASE | 4 |
| 2024 | Poracle: Testing Patches under Preservation Conditions to Combat the Overfitting Problem of Program RepairabstractTo date, the users of test-driven program repair tools suffer from the overfitting problem; a generated patch may pass all available tests without being correct. In the existing work, users are treated as merely passive consumers of the tests. However, what if they are willing to modify the test to better assess the patches obtained from a repair tool? In this work, we propose a novel semi-automatic patch-classification methodology named Poracle . Our key contributions are three-fold. First, we design a novel lightweight specification method that reuses the existing test. Specifically, the users extend the existing failing test with a preservation condition —the condition under which the patched and pre-patched versions should produce the same output. Second, we develop a fuzzer that performs differential fuzzing with a test containing a preservation condition. Once we find an input that satisfies a specified preservation condition but produces different outputs between the patched and pre-patched versions, we classify the patch as incorrect with high confidence. We show that our approach is more effective than the four state-of-the-art patch classification approaches. Last, we show through a user study that the users find our semi-automatic patch assessment method more effective and preferable than the manual assessment. Elkhan Ismayilzada, Md Mazba Ur Rahman, Dongsun Kim 0001, Jooyong Yi |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2023 | Automated Program Repair from Fuzzing PerspectiveabstractIn this work, we present a novel approach that connects two closely-related topics: fuzzing and automated program repair (APR). The paper is divided into two parts. In the first part, we describe the similarities between fuzzing and APR both of which can be viewed as a search problem. In the second part, we introduce a new patch-scheduling algorithm called Casino, which is designed from a fuzzing perspective to enhance search efficiency. Our experiments demonstrate that Casino outperforms existing algorithms. We also promote open science by sharing SimAPR, a simulation tool that can be used to evaluate new patch-scheduling algorithms. Seungheon Han, Askar Yeltayuly Khamit, Jooyong Yi |
ISSTA | 4 |
| 2023 | BUGSC++: A Highly Usable Real World Defect Benchmark for C/C++abstractAs software systems grow larger and more complex, debugging takes up an increasingly significant portion of developers' time and efforts during software maintenance. To aid software engineers in debugging, many automated debugging and repair techniques have been proposed. Both the development and evaluation of these automated techniques depend on benchmarks of bugs. While many different defect benchmarks have been developed, only a few benchmarks are widely used due to the origin of the collected bugs as well as the usability of the benchmarks themselves, risking a biased research landscape. This paper presents BUGSC++, a new benchmark that contains 209 real-world bugs collected from 22 open-source C/C++ projects. BugsC++ aims to provide high usability by providing a similar user interface to the widely used Defects4J. Further, BugsC++ ensures the replicability of the bugs in its collection by encapsulating each buggy program in a Docker container. By providing a highly usable real-world defect benchmark for C/C++, we hope to promote debugging research for C/C++. Gabin An, Minhyuk Kwon, Kyunghwa Choi, Jooyong Yi, Shin Yoo |
ASE | 4 |
| 2023 | Leakpair: Proactive Repairing of Memory Leaks in Single Page Web ApplicationsabstractModern web applications often resort to application development frameworks such as React, Vue.js, and Angular. While the frameworks facilitate the development of web applications with several useful components, they are inevitably vulnerable to unmanaged memory consumption since the frameworks often produce Single Page Applications (SPAs). Web applications can be alive for hours and days with behavior loops, in such cases, even a single memory leak in a SPA app can cause performance degradation on the client side. However, recent debugging techniques for web applications still focus on memory leak detection, which requires manual tasks and produces imprecise results. We propose Leakpair,a technique to repair memory leaks in single page applications. Given the insight that memory leaks are mostly non-functional bugs and fixing them might not change the behavior of an application, the technique is designed to proactively generate patches to fix memory leaks, without leak detection, which is often heavy and tedious. To generate effective patches, Leakpairfollows the idea of pattern-based program repair since the automated repair strategy shows successful results in many recent studies. We evaluate the technique on more than 20 open-source projects without using explicit leak detection. The patches generated by our technique are also submitted to the projects as pull requests. The results show that Leakpaircan generate effective patches to reduce memory consumption that are acceptable to developers. In addition, we execute the test suites given by the projects after applying the patches, and it turns out that the patches do not cause any functionality breakage; this might imply that Leakpaircan generate non-intrusive patches for memory leaks. Arooba Shahoor, Askar Yeltayuly Khamit, Jooyong Yi, Dongsun Kim 0001 |
ASE | 3 |
| 2022 | Speeding up constraint-based program repair using a search-based technique
Jooyong Yi, Elkhan Ismayilzada |
Inf. Softw. Technol. | 1 |
| 2022 | Verifix: Verified Repair of Programming AssignmentsabstractAutomated feedback generation for introductory programming assignments is useful for programming education. Most works try to generate feedback to correct a student program by comparing its behavior with an instructor’s reference program on selected tests. In this work, our aim is to generate verifiably correct program repairs as student feedback. A student-submitted program is aligned and composed with a reference solution in terms of control flow, and the variables of the two programs are automatically aligned via predicates describing the relationship between the variables. When verification attempt for the obtained aligned program fails, we turn a verification problem into a MaxSMT problem whose solution leads to a minimal repair. We have conducted experiments on student assignments curated from a widely deployed intelligent tutoring system. Our results show that generating verified repair without sacrificing the overall repair rate is possible. In fact, our implementation, Verifix, is shown to outperform Clara, a state-of-the-art tool, in terms of repair rate. This shows the promise of using verified repair to generate high confidence feedback in programming pedagogy settings. Umair Z. Ahmed, Zhiyu Fan, Jooyong Yi, Omar I. Al-Bataineh, Abhik Roychoudhury |
ACM Trans. Softw. Eng. Methodol. | 3 |
| 2018 | Toward a Better Understanding of How to Develop Software Under Stress - Drafting the Lines for Future ResearchabstractThe software is often produced under significant time constraints. Our idea is to understand the effects of various software development practices on the performance of developers working in stressful environments, and identify the best operating conditions for software developed under stressful conditions collecting data through questionnaires, non-invasive software measurement tools that can collect measurable data about software engineers and the software they develop, without intervening their activities, and biophysical sensors and then try to recreated also in different processes or key development practices such conditions. Joseph Alexander Brown, Vladimir Ivanov 0001, Alan Rogers, Giancarlo Succi, Alexander Tormasov, Jooyong Yi |
ENASE | 6 |
| 2018 | A correlation study between automated program repair and test-suite metricsabstractAutomated program repair has attracted attention due to its potential to reduce debugging cost. Prior works show the feasibility of automated repair, and the research focus is gradually shifting towards the quality of generated patches. One promising direction is to control the quality of generated patches by controlling the quality of test-suites used. In this paper, 1we investigate the question: "Can traditional test-suite metrics used in software testing be used for automated program repair?". We empirically investigate the effectiveness of test-suite metrics (statement / branch coverage and mutation score) in controlling the reliability of repairs (the likelihood that repairs cause regressions). We conduct the largest-scale experiments to date with real-world software, and perform the first correlation study between test-suite metrics and the reliability of generated repairs. Our results show that by increasing test-suite metrics, the reliability of repairs tend to increase. Particularly, such trend is most strongly observed in statement coverage. This implies that traditional test-suite metrics used in software testing can also be used to improve the reliability of repairs in program repair. Jooyong Yi, Shin Hwei Tan, Sergey Mechtaev, Marcel Böhme, Abhik Roychoudhury |
ICSE | 1 |
| 2018 | Design and validation of precooked developer dashboardsabstractDespite increasing popularity of developer dashboards, the effectiveness of dashboards is still in question. In order to design a dashboard that is effective and useful for developers, it is important to know (a) what information developers need to see in a dashboard, and (b) how developers want to use a dashboard with that necessary information. To answer these questions, we conducted two series of face-to-face individual interviews with developers. In the first step we analyzed answers, build a Goal-Question-Metric model and designed a precooked developer dashboard. Then, during the second separate series of interviews, we validated the GQM and derived feedback on the designed dashboard. Given that the cost of dashboard customization prevents developers from utilizing dashboards, we believe that our findings can provide a solid starting point to build precooked developer dashboards that can be readily utilized by software companies. Vladimir Ivanov 0001, Vladislav Pischulin, Alan Rogers, Giancarlo Succi, Jooyong Yi, Vasilii Zorin |
ESEC/SIGSOFT FSE | 5 |
| 2018 | A correlation study between automated program repair and test-suite metrics
Jooyong Yi, Shin Hwei Tan, Sergey Mechtaev, Marcel Böhme, Abhik Roychoudhury |
Empir. Softw. Eng. | 1 |
| 2017 | What do software engineers care about? gaps between research and practiceabstractIt is a cliche to say that there is a gap between research and practice. As the interest and importance in the practical impact of research has been growing, the gap between research and practice is expected to be narrowing. However, our study reveals that there still seems to be a wide gap. We survey so ware engineers about what they care about when developing so ware. We then compare our survey results with the research topics of the papers published in ICSE/FSE recently. We found the following discrepancy: while so ware engineers care more about so ware development productivity than the quality of so ware, papers on research areas closely related to so ware productivity--such as so ware development process management and so ware development techniques--are significantly less published than papers on so ware verification and validation that account for more than half of publications. We also found that so ware engineers are in great need for techniques for accurate effort estimation, and they are not necessarily knowledgable about techniques they can use to meet their needs. Vladimir Ivanov 0001, Alan Rogers, Giancarlo Succi, Jooyong Yi, Vasilii Zorin |
ESEC/SIGSOFT FSE | 4 |
| 2017 | A feasibility study of using automated program repair for introductory programming assignmentsabstractDespite the fact an intelligent tutoring system for programming (ITSP) education has long attracted interest, its widespread use has been hindered by the difficulty of generating personalized feedback automatically. Meanwhile, automated program repair (APR) is an emerging new technology that automatically fixes software bugs, and it has been shown that APR can fix the bugs of large real-world software. In this paper, we study the feasibility of marrying intelligent programming tutoring and APR. We perform our feasibility study with four state-of-the-art APR tools (GenProg, AE, Angelix, and Prophet), and 661 programs written by the students taking an introductory programming course. We found that when APR tools are used out of the box, only about 30% of the programs in our dataset are repaired. This low repair rate is largely due to the student programs often being significantly incorrect - in contrast, professional software for which APR was successfully applied typically fails only a small portion of tests. To bridge this gap, we adopt in APR a new repair policy akin to the hint generation policy employed in the existing ITSP. This new repair policy admits partial repairs that address part of failing tests, which results in 84% improvement of repair rate. We also performed a user study with 263 novice students and 37 graders, and identified an understudied problem; while novice students do not seem to know how to effectively make use of generated repairs as hints, the graders do seem to gain benefits from repairs. Jooyong Yi, Umair Z. Ahmed, Amey Karkare, Shin Hwei Tan, Abhik Roychoudhury |
ESEC/SIGSOFT FSE | 1 |
| 2016 | Angelix: scalable multiline program patch synthesis via symbolic analysisabstractSince debugging is a time-consuming activity, automated program repair tools such as GenProg have garnered interest. A recent study revealed that the majority of GenProg repairs avoid bugs simply by deleting functionality. We found that SPR, a state-of-the-art repair tool proposed in 2015, still deletes functionality in their many "plausible" repairs. Unlike generate-and-validate systems such as GenProg and SPR, semantic analysis based repair techniques synthesize a repair based on semantic information of the program. While such semantics-based repair methods show promise in terms of quality of generated repairs, their scalability has been a concern so far. In this paper, we present Angelix, a novel semantics-based repair method that scales up to programs of similar size as are handled by search-based repair tools such as GenProg and SPR. This shows that Angelix is more scalable than previously proposed semantics based repair methods such as SemFix and DirectFix. Furthermore, our repair method can repair multiple buggy locations that are dependent on each other. Such repairs are hard to achieve using SPR and GenProg. In our experiments, Angelix generated repairs from large-scale real-world software such as wireshark and php, and these generated repairs include multi-location repairs. We also report our experience in automatically repairing the well-known Heartbleed vulnerability. Sergey Mechtaev, Jooyong Yi, Abhik Roychoudhury |
ICSE | 2 |
| 2015 | DirectFix: Looking for Simple Program RepairsabstractRecent advances in program repair techniques have raised the possibility of patching bugs automatically. For an automatically generated patch to be accepted by developers, it should not only resolve the bug but also satisfy certain human-related factors including readability and comprehensibility. In this paper, we focus on the simplicity of patches (the size of changes). We present a novel semantics-based repair method that generates the simplest patch such that the program structure of the buggy program is maximally preserved. To take into account the simplicity of repairs in an efficient way (i.e., Without explicitly enumerating each repair candidate for each fault location), our method fuses fault localization and repair generation into one step. We do so by leveraging partial Max SAT constraint solving and component-based program synthesis. We compare our prototype implementation, Direct Fix, with the state-of-the-art semantics-based repair tool Sem Fix, that performs fault localization before repair generation. In our experiments with SIR programs and GNU Coreutils, Direct Fix generates repairs that are simpler than those generated by Sem Fix. Since both Direct Fix and Sem Fix are test-driven repair tools, they can introduce regressions for other tests which do not drive the repair. We found that Direct Fix causes substantially less regression errors than Sem Fix. Sergey Mechtaev, Jooyong Yi, Abhik Roychoudhury |
ICSE (1) | 2 |
| 2015 | Software Change ContractsabstractSoftware errors often originate from incorrect changes, including incorrect program fixes, incorrect feature updates, and so on. Capturing the intended program behavior explicitly via contracts is thus an attractive proposition. In our recent work, we had espoused the notion of “change contracts” to express the intended program behavior changes across program versions. Change contracts differ from program contracts in that they do not require the programmer to describe the intended behavior of those program features which are unchanged across program versions. In this work, we present the formal semantics of our change contract language built on top of the Java modeling language (JML). Our change contract language can describe behavioral as well as structural changes. We evaluate the expressivity of the change contract language via a survey given to final-year undergraduate students. The survey results enable to understand the usability of our change contract language for purposes of writing contracts, comprehending written contracts, and modifying programs according to given change contracts. Finally, we develop both dynamic and static checkers for change contracts, and show how they can be used in maintaining software changes. We use our dynamic checker to automatically suggest tests that manifest violations of change contracts. Meanwhile, we use our static checker to verify that a program is changed as specified in its change contract. Apart from verification, our static checker also performs various other software engineering tasks, such as localizing the buggy method, detecting/debugging regression errors, and classifying the cause for a test failure as either error in production code or error in test code. Jooyong Yi, Dawei Qi, Shin Hwei Tan, Abhik Roychoudhury |
ACM Trans. Softw. Eng. Methodol. | 1 |
| 2014 | Dynamic Inference of Change ContractsabstractSoftware evolves and thus developers frequently make changes to systems that are logged in version control systems. These changes are often poorly documented -- often commit logs are empty or only contain minimal information. Thus, it is often a challenge to understand why certain changes are made especially if they were introduced many months or even years ago. Understanding these changes is important when pertinent questions are raised during future bug fixing or software evolution efforts. Thus, there is a need for an automated approach that can help developers better document changes with little or minimal effort. To address this need, we propose a dynamic inference framework that automatically infers change contracts. Recently, change contract is proposed as a formalism to capture the semantics of changes. Different from standard program contract, change contract focuses in expressing the changed behavior between two versions of software systems. Our system infers candidate contracts based on actual changes and developers can further modify these contracts to reflect intended changes. We have performed a preliminary evaluation of our dynamic inference framework on a set of 15 real bug fixing changes from AspectJ with promising results. Tien-Duy B. Le, Jooyong Yi, David Lo 0001, Ferdian Thung, Abhik Roychoudhury |
ICSME | 2 |
| 2013 | Expressing and checking intended changes via software change contractsabstractSoftware errors often originate from incorrect changes, including incorrect program fixes, incorrect feature updates and so on. Capturing the intended program behavior explicitly via contracts is thus an attractive proposition. In our recent work, we had espoused the notion of "change contracts" to express the intended program behavior changes across program versions. Change contracts differ from program contracts in that they do not require the programmer to describe the intended behavior of program features which are unchanged across program versions. In this work, we present the formal semantics of our change contract language built on top of the Java Modeling Language (JML). Our change contract language can describe behavioral as well as structural changes. We evaluate the expressivity of the change contract language via a survey given to final year undergraduate students. The survey results enable us to understand the usability of our change contract language for purposes of writing contracts, comprehending written contracts, and modifying programs according to given change contracts. Finally, we discuss the tool support developed for our change contract language. The tool support enables (i) test generation to witness contract violation, as well as (ii) automated repair of certain tests which are broken due to program changes. Jooyong Yi, Dawei Qi, Shin Hwei Tan, Abhik Roychoudhury |
ISSTA | 1 |
| 2012 | Software change contractsabstractIncorrect program changes including regression bugs, incorrect bug-fixes, incorrect feature updates are pervasive in software. These incorrect program changes affect software quality and are difficult to detect/correct. In this paper, we propose the notion of "change contracts" to avoid incorrect program changes. Change contracts formally specify the intended effect of program changes. Incorrect program changes are detected when they are checked with respect to the change contracts. We design a change contract language for Java programs and a dynamic checking system for our change contract language. We conduct a preliminary user study to check the expressiveness of our change contract language and find that the language is expressive enough to capture a wide variety of real-life changes in three large software projects (i.e., Ant, JMeter, log4j). Finally, our contract checking system detects several real-life incorrect changes in these three software projects via runtime checking of the change contracts. Dawei Qi, Jooyong Yi, Abhik Roychoudhury |
SIGSOFT FSE | 2 |
| 2012 | Efficient and formal generalized symbolic execution
Xianghua Deng, Jooyong Yi, Robby |
Autom. Softw. Eng. | 2 |
| 2010 | Filtering false alarms of buffer overflow analysis using SMT solvers
Youil Kim, Jooyong Yi, Hwansoo Han, Kwang-Moo Choe |
Inf. Softw. Technol. | 2 |
| 2010 | Towards an industrial grade IVE for Java and next generation research platform for JML
Patrice Chalin, Robby, Perry R. James, Jooyong Yi, George Karabotsos |
Int. J. Softw. Tools Technol. Transf. | 4 |
| 2006 | Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open SystemsabstractThis paper presents Kiasan, a bounded technique to reason about open systems based on a path sensitive, relatively sound and complete symbolic execution instead of the usual compositional reasoning through weakest precondition calculation that summarizes all execution paths. Kiasan is able to check strong heap properties, and it is fully automatic and flexible in terms of its cost and the guarantees it provides. It allows a user-adjustable mixed compositional/non-compositional reasoning and naturally produces error traces as fault evidence. We implemented Kiasan using the Bogor model checking framework and observed that its performance is comparable to ESC/Java on similar scales of problems and behavioral coverage, while providing the ability to check much stronger specifications Xianghua Deng, Jooyong Yi, Robby |
ASE | 2 |