九州大学 研究者情報
論文一覧
佐藤 亮介(さとう りようすけ) データ更新日:2019.09.03

助教 /  システム情報科学研究院 情報知能工学部門 高度ソフトウェア工学講座


原著論文
1. Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno, Temporal verification of higher-order functional programs, ACM SIGPLAN Notices, 10.1145/2837614.2837667, 51, 1, 57-68, 2016.04, [URL], We present an automated approach to verifying arbitrary omega regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs..
2. Masayuki Hirose, Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato, Toward automatic program repair using knowledge extracted from stack overflow, Computer Software, 35, 4, 144-150, 2018.01, In this paper, we investigate the possibility and effectiveness of the approach to generating bug-fixing patterns extracted from Stack Overflow, which is a question and answer web site for programming. To do so, we collect 984,533 posts with the Android tag in Stack Overflow and extract top 10,000 ones related to the tag. Results show that (1) there are 28 posts that would be able to generate bug-fixing patterns, (2) there are 42 posts that are useful to fix bugs, and (3) those 42 posts include bug fixing patterns that are not supported by a previous study (PAR: Pattern-based Automatic program Repair)..
3. Daito Nakano, Yasutaka Kamei, Ryosuke Sato, Naoyasu Ubayashi, Shuichi Takayama, Takashi Iwasaki, An empirical study on weighting techniques for open source software assessment models, Computer Software, 35, 4, 136-143, 2018.01, It is desirable for software companies to assess the quality of open source software (OSS) in order to avoid degradation of product quality due to the quality of OSS. In this study, we conduct a questionnaire survey to understand which quality are required by developers for OSS in each development type and assess the quality of OSS when considering the results of the questionnaire survey. We target the OSS systems used in the development projects of Fujitsu Kyushu Network Technologies Limited. When comparing the questionnaire result with each development type, with five questions, there is a difference of 20% or more in proportion that "Important" or "Somewhat important" is answered. We set the weight for each evaluation item based on the questionnaire for each development type, and as a result of evaluating 6 OSS systems, we find that our approach detects 7 items from 12 items that developers evaluated as risky..
4. Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi, Ordered types for stream processing of tree-structured data, Journal of Information Processing, 10.2197/ipsjjip.19.74, 19, 74-87, 2011, [URL], Suenaga, et al. have developed a type-based framework for automatically translating tree-processing programs into stream-processing ones. The key ingredient of the framework was the use of ordered linear types to guarantee that a tree-processing program traverses an input tree just once in the depth-first, left-to-right order (so that the input tree can be read from a stream). Their translation, however, sometimes introduces redundant buffering of input data. This paper extends their framework by introducing ordered, non-linear types in addition to ordered linear types. The resulting transformation framework reduces the redundant buffering, generating more efficient stream-processing programs..
5. Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi, Refinement type checking via assertion checking, Journal of Information Processing, 10.2197/ipsjjip.23.827, 23, 6, 827-834, 2015.11, [URL], A refinement type can be used to express a detailed specification of a higher-order functional program. Given a refinement type as a specification of a program, we can verify that the program satisfies the specification by checking that the program has the refinement type. Refinement type checking/inference has been extensively studied and a number of refinement type checkers have been implemented. Most of the existing refinement type checkers, however, need type annotations, which is a heavy burden on users. To overcome this problem, we reduce a refinement type checking problem to an assertion checking problem, which asks whether the assertions in a program never fail; and then we use an existing assertion checker to solve it. This reduction enables us to construct a fully automated refinement type checker by using a state-of-the-art fully automated assertion checker. We also prove the soundness and the completeness of the reduction, and report on implementation and preliminary experiments..
6. Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi, Verifying relational properties of functional programs by first-order refinement, Science of Computer Programming, 10.1016/j.scico.2016.02.007, 137, 2-62, 2017.04, [URL], Much progress has been made recently on fully automated verification of higher-order functional programs, based on refinement types and higher-order model checking. Most of those verification techniques are, however, based on first-order refinement types, hence unable to verify certain properties of functions (such as the equality of two recursive functions and the monotonicity of a function, which we call relational properties). To relax this limitation, we introduce a restricted form of higher-order refinement types where refinement predicates can refer to functions, and formalize a systematic program transformation to reduce type checking/inference for higher-order refinement types to that for first-order refinement types, so that the latter can be automatically solved by using an existing software model checker. We also prove the soundness of the transformation, and report on implementation and experiments..

九大関連コンテンツ

pure2017年10月2日から、「九州大学研究者情報」を補完するデータベースとして、Elsevier社の「Pure」による研究業績の公開を開始しました。
 
 
九州大学知的財産本部「九州大学Seeds集」