The imbalanced problem indicates that the data set is unevenly distributed, resulting in sub-optimal classifiers to recognize the minority class. Traditional solutions try to design new classifiers to solve this problem or balance the skewed data sets, the former is too costly while the latter has an uncertain effect on different combinations of classifiers and measurements. In this paper, we propose a reinforcement learning-based oversampling method, which can directly produce targeted samples according to the downstream classifiers and measurements. During training, our learning procedure introduces the classification information to the generation process. Moreover, as opposed to oversampling approaches, we have no assumption of the downstream classifiers and performance metrics, and the proposed has a wider application. We carry out experiments on 17 UCI and KEEL data sets, experimental results demonstrate the superior performance of our proposed method.

Memory is a constrained resource for software, and memory consumption is an essential factor to evaluate a program's performance. Therefore, there are existing works which concentrated on the inference of programs' memory usage. However, previous works mainly exploited type systems to infer programs' memory consumption, which were weak at handling aliasing information for heap manipulating programs. In this work, we propose an automated inference system for programs' memory usage based on the framework of Nguyen et al. The system can capture both the maximum requirement and the net usage of memory. We employ a separation logic based forward analysis to track the program's execution symbolically, and use symbolic Presburger arithmetic expressions to express the effect of allocation and deallocation in heap memory. Our approach is sound, and is also expected to provide more precision and scalability than previous works.

Memory usage analysis is an important problem for resource-constrained mobile devices, especially under mission- or safety-critical circumstances. Program codes running on or being downloaded into such devices are often available in low-level bytecode forms. We propose in this paper a formal heap model for Java bytecode language, on top of which we can then provide separation logic support for further memory usage verification. Our low-level heap model for Java bytecode would allow us to reason about the size and alignment properties of primitive values stored in the heap. To support type-related reasoning such as guaranteeing type and alignment safety, this model is also lifted with both base types and user-defined classes. Based on such model, we have also defined a separation logic proof system whose assertions are interpreted using the lifted heap with types. We envision, with further extension, the system would provide good support for memory usage analysis and verification for mobile devices.

The WS-BPEL language has become a de facto standard for modeling Web-based business processes. One of its essential features is the fully programmable compensation mechanism. To understand it better, many works have mainly focused on formal semantic models for WS-BPEL. In this paper, we make one step forward by investigating the verification problem for business processes written in BPEL-like languages. We propose a set of proof rules in Hoare-logic style as an axiomatic verification system for a BPEL-like core language containing key features such as data states, fault and compensation handling. We also propose a big-step operational semantics which incorporates all these key features. Our verification rules are proven sound with respect to this underlying semantics. The application of the verification rules is illustrated via the proof search process for a nontrivial example.