We present Diver, a novel technique for effectively finding critical bugs in SMT solvers. Ensuring the correctness of SMT solvers is becoming increasingly important as many applications use solvers as a foundational basis. In response, several approaches for testing SMT solvers, which are classified into differential testing and oracle-guided approaches, have been proposed until recently. However, they are still unsatisfactory in that (1) differential testing approaches cannot validate unique yet important features of solvers, and (2) oracle-guided approaches cannot generate diverse tests due to their reliance on limited mutation rules. Diver aims to complement these shortcomings, particularly focusing on finding bugs that are missed by existing approaches. To this end, we present a new testing technique that performs oracle-guided yet unrestricted random mutations. We have used Diver to validate the most recent versions of three popular SMT solvers: CVC5, Z3 and dReal. In total, Diver found 25 new bugs, of which 21 are critical and directly affect the reliability of the solvers. We also empirically prove DIVER's own strength by showing that existing tools are unlikely to find the bugs discovered by Diver.

Rename Instance Method Refactoring (RiMr) is a behavior-preserving code transformation that changes the name of a non-static method declaration along with its references (i.e., method calls) while preserving all method bindings over an entire program. RiMr checks a set of preconditions to ensure that the original method bindings will be preserved after rename. Only when all preconditions are satisfied, are the method declaration and references transformed. A decade ago, however, it was found that RiMr offered by Java Integrated Development Environment (IDE) tools may change existing method bindings due to incorrect precondition checks, which consequently cause program behavior changes. Surprisingly, we found that none of the current Java IDEs have corrected those flaws in their RiMr preconditions.We created a Java RiMr tool (called KennyRiMr) as an Eclipse JDT plug-in that addresses the method rebinding issues in RiMr. We verified the correctness of KennyRiMr with thirteen nontrivial programs in terms of precondition checks and code transformations. Our experiments demonstrated that KennyRiMr fixed all known flaws in RiMr preconditions, requiring merely a few more seconds to process the additional precondition checks that we introduced. With KennyRiMr, correctness remains consistent regardless of program size.

Packing is the most common analysis avoidance technique for hiding malware. Also, packing can make it harder for the security researcher to identify the behaviour of malware and increase the analysis time. In order to analyze the packed malware, we need to perform unpacking first to release the packing. In this paper, we focus on unpacking and its related technologies to analyze the packed malware. Through extensive analysis on previous unpacking studies, we pay attention to four important drawbacks: no phase integration, no detection combination, no real-restoration, and no unpacking verification. To resolve these four drawbacks, in this paper, we present an all-in-one structure of the unpacking system that performs packing detection, unpacking (i.e., restoration), and verification phases in an integrated framework. For this, we first greatly increase the packing detection accuracy in the detection phase by combining four existing and new packing detection techniques. We then improve the unpacking phase by using the state-of-the-art static and dynamic unpacking techniques. We also present a verification algorithm evaluating the accuracy of unpacking results. Experimental results show that the proposed all-in-one unpacking system performs all of the three phases well in an integrated framework. In particular, the proposed hybrid detection method is superior to the existing methods, and the system performs unpacking very well up to 100% of restoration accuracy for most of the files except for a few packers.

Regression testing checks that recent project changes do not break previously working functionality. Although important, regression testing is costly when changes are frequent. Regression test selection (RTS) optimizes regression testing by running only tests whose results might be affected by a change. Traditionally, RTS collects dependencies (e.g., on files) for each test and skips the tests, at a new project revision, whose dependencies did not change. Existing RTS techniques do not differentiate behavior-preserving transformations (i.e., refactorings) from other code changes. As a result, tests are run more frequently than necessary.

Refactoring engines are standard tools in today's Integrated Development Environments (IDEs). They allow programmers to perform one refactoring at a time, but programmers need more. Most design patterns in the Gang-of-Four text can be written as a refactoring script -- a programmatic sequence of refactorings. In this paper, we present R3, a new Java refactoring engine that supports refactoring scripts. It builds a main-memory, non-persistent database to encode Java entity declarations (e.g., packages, classes, methods), their containment relationships, and language features such as inheritance and modifiers. Unlike classical refactoring engines that modify Abstract Syntax Trees (ASTs), R3 refactorings modify only the database; refactored code is produced only when pretty-printing ASTs that reference database changes. R3 performs comparable precondition checks to those of the Eclipse Java Development Tools (JDT) but R3's codebase is about half the size of the JDT refactoring engine and runs an order of magnitude faster. Further, a user study shows that R3 improved the success rate of retrofitting design patterns by 25% up to 50%.

Retrofitting design patterns into a program by hand is tedious and error-prone. A programmer must distinguish refactorings that are provided by an Integrated Development Environment (IDE) from those that must be realized manually, determine a precise sequence of refactorings to apply, and perform this sequence repetitively to a laborious degree. We designed, implemented, and evaluated Reflective Refactoring (R2), a Java package to automate the creation of classical design patterns (Visitor, Abstract Factory, etc.), their inverses, and variants. We encoded 18 out of 23 Gang-of-Four design patterns as R2scripts and explain why the remaining are inappropriate for refactoring engines. We evaluate the productivity and scalability of R2with a case study of 6 real-world applications. In one case, R2automatically created a Visitor with 276 visit methods by invoking 554 Eclipse refactorings in 10 minutes - an achievement that could not be done manually. R2also sheds light on why refactoring correctness, expressiveness, and speed are critical issues for scripting in next-generation refactoring engines.

The relationship between feature modules and feature interactions is not well-understood. To explain classic examples of feature interaction, we show that features are not only composed sequentially, but also by cross-product and interaction operations that heretofore were implicit in the literature. Using the Colored IDE (CIDE) tool as our starting point, we (a) present a formal model of these operations, (b) show how it connects and explains previously unrelated results in Feature Oriented Software Development (FOSD), and (c) describe a tool, based on our formalism, that demonstrates how changes in composed documents can be back-propagated to their original feature module definitions, thereby improving FOSD tooling.

Energy environment has been changing rapidly such as the fluctuation of oil prices and the effect on UNFCCC (United nations framework convention on climate change). Korea is easily affected by the change of oil prices due to poor natural resources and large dependence of consumed energy resources in Korea. Energy technology development is a crucial key considering Korea's national energy security and environments. In this study, we establish the criteria list and prioritize relative weights of criteria and sub-criteria for assessing and selecting strategic Big-sized R&D programs in the sector of energy technology development. A fuzzy AHP approach, which integrates fuzzy theory into analytic hierarchy process (AHP) approach, reflects the vagueness of human thoughts and perception as making pairwise comparisons of criteria and alternatives. The fundamental data of this research results will support R&D planning phase for policy makers as selecting strategic R&D programs for producing well focused R&D outcomes.

The advance of technology has given many alternatives of subscriber loop. Having many choices is a blessing and a curse at the same time for a newly established organization. A group of experts from Hanaro Telecom and Sejong University was formed to investigate techno-economic aspects of the many alternatives. In the course of several discussions, both parties agreed on the urgency to form a techno-economic model which can precisely describe the underlying technical nature of the subscriber loop and its business aspects. This paper presents the modeling, solution processes and related topics.

Stochastic Petri nets are strong tools to model discrete event dynamic systems. To describe the transient properties of the system, it is necessary to find the eigenvalues of the underlying Markov process. However, the state explosion problem, the stiffness problem appearing in many applications, and the intrinsic numerical instability hinder us from getting the complete eigenvalue set. In this paper, the location of the eigenvalues are obtained without generating the reachability set of the stochastic Petri net.

Stochastic Petri nets are widely used to get the steady state performance of a discrete event dynamic system. This is usually done with little concern about how fast the system reaches its steady state. The length of the transient state is known as the rise time in control theory or, the relaxation time in a Markov process. These are governed by the eigenvalue called the second dominant eigenvalues. Also, the separation of the most dominant and second dominant eigenvalue plays a role in the convergence of the numerical solution of the Markov process. A stochastic Petri net synthesis method which preserves the ergodicity and the irreducibility of the underlying Markov process, and gives the lower bound of the second dominant eigenvalue and the number of states is proposed.