EDBT 2026 Demo / reviewers in the wild / expert
Wontae Choi
dblp:70/7540
· DBLP profile ↗
8ranked-venue papers
4as first author
0since 2021 · last 2020
0000-0003-4745-5363ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 7 · 4 first-authorSecurity and privacy · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
5 papers |
Software testing · 59% Program analysis · 24% Programming languages and type systems · 17% |
Topics — the 16 heaviest of 17, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Software testing
GUI testing |
0.5 | 2 | 2018 | DetReduce: minimizing Android GUI test suites for regression testing · ICSE 2018 Guided GUI testing of android apps with minimal restart and approximate learning · OOPSLA 2013 |
Software testing › GUI testing
Android GUI testing |
0.3 | 1 | 2018 | DetReduce: minimizing Android GUI test suites for regression testing · ICSE 2018 |
Software testing
regression testing |
0.3 | 1 | 2018 | DetReduce: minimizing Android GUI test suites for regression testing · ICSE 2018 |
Software testing › regression testing
test suite reduction |
0.3 | 1 | 2018 | DetReduce: minimizing Android GUI test suites for regression testing · ICSE 2018 |
Software testing
test input generation |
0.2 | 2 | 2015 | Guided GUI testing of android apps with minimal restart and approximate learning · OOPSLA 2013 MultiSE: multi-path symbolic execution using value summaries · ESEC/SIGSOFT FSE 2015 |
Program analysis › symbolic execution
dynamic symbolic execution |
0.2 | 1 | 2015 | MultiSE: multi-path symbolic execution using value summaries · ESEC/SIGSOFT FSE 2015 |
Program analysis › symbolic execution
state merging |
0.2 | 1 | 2015 | MultiSE: multi-path symbolic execution using value summaries · ESEC/SIGSOFT FSE 2015 |
Program analysis
symbolic execution |
0.2 | 1 | 2015 | MultiSE: multi-path symbolic execution using value summaries · ESEC/SIGSOFT FSE 2015 |
Software testing › mobile application testing
android app testing |
0.2 | 1 | 2013 | Guided GUI testing of android apps with minimal restart and approximate learning · OOPSLA 2013 |
Software testing
model-based testing |
0.2 | 1 | 2013 | Guided GUI testing of android apps with minimal restart and approximate learning · OOPSLA 2013 |
Programming languages and type systems › programming paradigms
generic programming |
0.1 | 1 | 2012 | The implicit calculus: a new foundation for generic programming · PLDI 2012 |
Programming languages and type systems › type systems › polymorphism
type classes |
0.1 | 1 | 2012 | The implicit calculus: a new foundation for generic programming · PLDI 2012 |
Programming languages and type systems
type systems |
0.1 | 1 | 2012 | The implicit calculus: a new foundation for generic programming · PLDI 2012 |
Programming languages and type systems › metaprogramming
multi-stage programming |
0.1 | 1 | 2011 | Static analysis of multi-staged programs via unstaging translation · POPL 2011 |
Program analysis
static analysis |
0.1 | 1 | 2011 | Static analysis of multi-staged programs via unstaging translation · POPL 2011 |
Program analysis › symbolic execution
path exploration |
0.1 | 1 | 2015 | MultiSE: multi-path symbolic execution using value summaries · ESEC/SIGSOFT FSE 2015 |
Methods — techniques the papers use, named apart from their topics
value summaries · 0.2constraint solving · 0.2machine learning · 0.2approximate learning · 0.2type theory · 0.1unstaging translation · 0.1semantic-preserving translation · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2020 | Guide Me to Exploit: Assisted ROP Exploit Generation for ActionScript Virtual MachineabstractAutomatic exploit generation (AEG) is the challenge of determining the exploitability of a given vulnerability by exploring all possible execution paths that can result from triggering the vulnerability. Since typical AEG implementations might need to explore an unbounded number of execution paths, they usually utilize a fuzz tester and a symbolic execution tool to facilitate this task. However, in the case of language virtual machines, such as the ActionScript Virtual Machine (AVM), AEG implementations cannot leverage fuzz testers or symbolic execution tools for generating the exploit script, because of two reasons: (1) fuzz testers cannot efficiently generate grammatically correct executables for the AVM due to the improbability of randomly generating highly-structured executables that follow the complex grammar rules and (2) symbolic execution tools encounter the well-known program-state-explosion problem due to the enormous number of control paths in early processing stages of a language virtual machine (e.g., lexing and parsing). Fadi Yilmaz, Meera Sridhar, Wontae Choi |
ACSAC | 3 |
| 2018 | DetReduce: minimizing Android GUI test suites for regression testingabstractIn recent years, several automated GUI testing techniques for Android apps have been proposed. These tools have been shown to be effective in achieving good test coverage and in finding bugs without human intervention. Being automated, these tools typically run for a long time (say, for several hours), either until they saturate test coverage or until a testing time budget expires. Thus, these automated tools are not good at generating concise regression test suites that could be used for testing in incremental development of the apps and in regression testing. Wontae Choi, Koushik Sen, George C. Necula |
ICSE | 1 |
| 2015 | SJS: A Type System for JavaScript with Fixed Object Layout
Wontae Choi, Satish Chandra 0001, George C. Necula, Koushik Sen |
SAS | 1 |
| 2015 | MultiSE: multi-path symbolic execution using value summariesabstractDynamic symbolic execution (DSE) has been proposed to effectively generate test inputs for real-world programs. Unfortunately, DSE techniques do not scale well for large realistic programs, because often the number of feasible execution paths of a program increases exponentially with the increase in the length of an execution path. In this paper, we propose MultiSE, a new technique for merging states incrementally during symbolic execution, without using auxiliary variables. The key idea of MultiSE is based on an alternative representation of the state, where we map each variable, including the program counter, to a set of guarded symbolic expressions called a value summary. MultiSE has several advantages over conventional DSE and conventional state merging techniques: value summaries enable sharing of symbolic expressions and path constraints along multiple paths and thus avoid redundant execution. MultiSE does not introduce auxiliary symbolic variables, which enables it to 1) make progress even when merging values not supported by the constraint solver, 2) avoid expensive constraint solver calls when resolving function calls and jumps, and 3) carry out most operations concretely. Moreover, MultiSE updates value summaries incrementally at every assignment instruction, which makes it unnecessary to identify the join points and to keep track of variables to merge at join points. We have implemented MultiSE for JavaScript programs in a publicly available open-source tool. Our evaluation of MultiSE on several programs shows that 1) value summaries are an eective technique to take advantage of the sharing of value along multiple execution path, that 2) MultiSE can run significantly faster than traditional dynamic symbolic execution and, 3) MultiSE saves a substantial number of state merges compared to conventional state-merging techniques. Koushik Sen, George C. Necula, Wontae Choi |
ESEC/SIGSOFT FSE | 4 |
| 2013 | Guided GUI testing of android apps with minimal restart and approximate learningabstractSmartphones and tablets with rich graphical user interfaces (GUI) are becoming increasingly popular. Hundreds of thousands of specialized applications, called apps, are available for such mobile platforms. Manual testing is the most popular technique for testing graphical user interfaces of such apps. Manual testing is often tedious and error-prone. In this paper, we propose an automated technique, called Swift-Hand, for generating sequences of test inputs for Android apps. The technique uses machine learning to learn a model of the app during testing, uses the learned model to generate user inputs that visit unexplored states of the app, and uses the execution of the app on the generated inputs to refine the model. A key feature of the testing algorithm is that it avoids restarting the app, which is a significantly more expensive operation than executing the app on a sequence of inputs. An important insight behind our testing algorithm is that we do not need to learn a precise model of an app, which is often computationally intensive, if our goal is to simply guide test execution into unexplored parts of the state space. We have implemented our testing algorithm in a publicly available tool for Android apps written in Java. Our experimental results show that we can achieve significantly better coverage than traditional random testing and L*-based testing in a given time budget. Our algorithm also reaches peak coverage faster than both random and L*-based testing. Wontae Choi, George C. Necula, Koushik Sen |
OOPSLA | 1 |
| 2012 | The implicit calculus: a new foundation for generic programmingabstractGeneric programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces; and 2) implicit instantiation of implementations of those interfaces. Bruno C. d. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, Kwangkeun Yi |
PLDI | 3 |
| 2011 | Static analysis of multi-staged programs via unstaging translationabstractStatic analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report. Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta |
POPL | 1 |
| 2009 | Abstract parsing for two-staged languages with concatenationabstractThis article, based on Doh, Kim, and Schmidt’s “abstract parsing” technique, presents an abstract interpretation for statically check-ing the syntax of generated code in two-staged programs. Ab-stract parsing is a static analysis technique for checking the syntax of generated strings. We adopt this technique for two-staged pro-gramming languages and formulate it in the abstract interpretation framework. We parameterize our analysis with the abstract domain so that one can choose the abstract domain as long as it satisfies the domain, namely an abstract parse stack and its widening with k-cutting. Soonho Kong, Wontae Choi, Kwangkeun Yi |
GPCE | 2 |