| 研究実績の概要 |
During the last year, I published four papers in the international conferences or workshops, in which two papers are first authored. One is published in the top conference of the formal verification area, that is, CAV'19, Core A* rank. This work proposes a novel approach of handling Boolean connectives in falsification by introducing the multi-armed bandit (MAB) model. Boolean connectives are important in industry; however, they suffer from the scale problem that diminishes the falsification performance. Our approach employ the MAB model: we treat sub-formulas as bandit machines, and apply MAB algorithms to govern the optimization. We experimentally show the effectiveness of our approach with a comparison to the existing one, and conclude that the proposed approach does not suffer from the scale problem.
The other one is published in a premier formal verification venue, NFM'20. We study the problem of input constraints. Although existing falsification techniques are effective, as they do not consider input constraints, the results they produce are usually meaningless. We bridge this gap by proposing the penalty-based approaches: once the input does not satisfy the constraint, we add a penalty to the objective function. Experiments show that the proposed approaches solve the problem and are able to produce meaningful results.
I participated in a work published in QEST'19, in which a novel sampling method is proposed for falsification. I participated in the ARCH friendly competition, and as a member authored a report of the competition results.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
My research work is going on smoothly. This is not only reflected by the publications over the last year, but also by many ideas that will be implemented in the coming year. The work published in CAV'19 implements the idea that I proposed in the research plan last year. This is a big improvement to the existing falsification framework, and will also be a starting point to some future works. Individually, I also strengthen myself a lot through this work. I experienced the entire research process, starting with raising a problem and proposing ideas, and ending with formally presenting it. Technically, the proposed two-layered framework is a powerful tool that can be generalized to solve many other problems. I will try to apply this idea again in the future work.
I also find many future directions of research. I realize that the practical usage is of great significance to a falsification technique, so my research is also guided by that goal. The work published in NFM'20 is an outcome of that direction. It considers the input constraint problem, which is not included in the existing framework but is important for industrial applications. In my future research, I will continue considering requirements from industry, so that my work aims to give falsification technique more practical values.
In conclusion, I grow up as a researcher smoothly, and I am confident to contribute more to the scientific community.
|
| 今後の研究の推進方策 |
I will continue my research plan, and contribute more to the falsification community. Firstly, I will keep on the research in falsification methodology, especially paying attention to some weaknesses of the existing work. The search algorithm is the core issue in falsification, however, it suffers from many problems, such as local optimum trap, etc. We will develop new techniques to further improve its effectiveness. At the same time, I will also aim to make falsification able to handle scenarios of better diversity. For example, scenarios in the presence of noises, input signals including discrete variables, etc. Our goal is to build up a more effective and efficient falsification framework.
Secondly, I will take efforts to make the falsification techniques more suited for practical use. This gives rise to many problems. For example, a problem we are very interested in is that, in the case that falsification does not return a counterexample, how likely there exists no counterexample in the search space. Although in general this problem is not decidable, we are considering approaches via heuristics, such as Gaussian process regression. Besides that, we will continue focusing on the input constraint problem, and aim to develop better techniques other than penalty-based approaches.
Thirdly, I will collaborate with my colleagues. One ongoing collaboration is with an intern student in our lab. Our topic is about white-box methods for falsification, which has not been investigated before. Another collaboration is with University of Waterloo on testing automated driving systems.
|
