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

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


学会発表等
1. Hokuto Muraoka, Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato, Revertに着目した不確かさに関する実証的分析, ソフトウェアエンジニアリングシンポジウム2019, 2019.08.
2. Yuta Takahashi, Naoyasu Ubayashi, Ryosuke Sato, Yasutaka Kamei, 集合知を用いた深層学習による自動バグ修正, ソフトウェアエンジニアリングシンポジウム2019, 2019.08.
3. 松井 健,鵜林 尚靖,佐藤 亮介,亀井 靖高, 敵対的サンプルに対するニューラルネットワークモデルの学習無し修正とその評価, 日本ソフトウェア科学会第36回大会, 2019.09.
4. Naoyasu Ubayashi, Hokuto Muraoka, Daiki Muramoto, Yasutaka Kamei, Ryosuke Sato, Poster
Exploring uncertainty in GitHub OSS projects: When and how do developers face uncertainty?, 40th ACM/IEEE International Conference on Software Engineering, ICSE 2018, 2018.05, [URL], Recently, many developers begin to notice that uncertainty is a crucial problem in software development. Unfortunately, no one knows how often uncertainty appears or what kinds of uncertainty exist in actual projects, because there are no empirical studies on uncertainty. To deal with this problem, we conduct a large-scale empirical study analyzing commit messages and revision histories of 1,444 OSS projects selected from the GitHub repositories..
5. Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi, Automatically disproving fair termination of higher-order functional programs, 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, 2016.08, [URL], We propose an automated method for disproving fair termination of higher-order functional programs, which is complementary to Murase et al.'s recent method for proving fair termination. A program is said to be fair terminating if it has no infinite execution trace that satisfies a given fairness constraint. Fair termination is an important property because program verification problems for arbitrary ω-regular temporal properties can be transformed to those of fair termination. Our method reduces the problem of disproving fair termination to higher-order model checking by using predicate abstraction and CEGAR. Given a program, we convert it to an abstract program that generates an approximation of the (possibly infinite) execution traces of the original program, so that the original program has a fair infinite execution trace if the tree generated by the abstract program satisfies a certain property. The method is a nontrivial extension of Kuwahara et al.'s method for disproving plain termination.We implemented a prototype verification tool based on our method and confirmed its effectiveness..
6. Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato, ICE-based refinement type discovery for higher-order functional programs, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, 2018.01, [URL], We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine learning, their Ice framework uses implication constraints, which consist of pairs (x, y) such that if x satisfies an invariant, so does y. From these constraints, Ice infers inductive invariants effectively. We observe that the implication constraints in the original Ice framework are not suitable for finding invariants of recursive functions with multiple function calls. We thus generalize the implication constraints to those of the form ((x
1
, ⋯, x
k
), y), which means that if all of x
1
, ⋯, x
k
satisfy an invariant, so does y. We extend their algorithms for inferring likely invariants from samples, verifying the inferred invariants, and generating new samples. We have implemented our method and confirmed its effectiveness through experiments..
7. Adrien Champion, Naoki Kobayashi, Ryosuke Sato, HoIce
An ICE-Based Non-linear Horn Clause Solver, 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, 2018.01, [URL], The ICE framework is a machine-learning-based technique originally introduced for inductive invariant inference over transition systems, and building on the supervised learning paradigm. Recently, we adapted the approach to non-linear Horn clause solving in the context of higher-order program verification. We showed that we could solve more of our benchmarks (extracted from higher-order program verification problems) than other state-of-the-art Horn clause solvers. This paper discusses some of the many improvements we recently implemented in HoIce, our implementation of this generalized ICE framework..
8. Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato, Can abstraction be taught? Refactoring-based abstraction learning, 6th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2018, 2018.01, Can the notion of abstraction be taught to students? It is a very difficult question. Abstraction plays an important role in software development. This paper shows that refactoring is effective for students to learn the notion of abstraction. We focus on design abstraction, because it is one of the crucial parts in teaching the essence of software engineering. To explore for a well-balanced separation of concerns between design and code, it is not avoidable to go back and forth between them. To help a student find an appropriate abstraction level, we introduce abstraction-aware refactoring patterns consisting of MoveM2C (Move concerns from Model to Code) and CopyC2M (Copy concerns from Code to Model). The patterns enable a student to refine abstraction while preserving not only external functionality but also traceability between design and code..
9. Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi, Combining higher-order model checking with refinement type inference, 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2019, in affiliation with the annual Symposium on Principles of Programming Languages, POPL 2019, 2019.01, [URL], There have been two major approaches to fully automated verification of higher-order functional programs: higher-order model checking and refinement type inference. The former approach is precise, but suffers from a bottleneck in the predicate discovery phase. The latter approach is generally faster than the former, thanks to the recent advances in constrained Horn clause (CHC) solving, but is imprecise, in that it rejects some valid programs. To take the best of the two approaches, we refine the higher-order model checking approach, by employing CHC solving in the predicate discovery phase. We have implemented the new approach and confirmed that the new system can verify more programs than those based on the previous two approaches..
10. 村岡 北斗, 村本 大起, 鵜林 尚靖, 亀井 靖高, 佐藤 亮介, Git開発履歴情報に基づく不確かさの可視化, ソフトウェア工学研究会, 2018.11.
11. 村本 大起, 佐藤 亮介, 鵜林 尚靖, 亀井 靖高, 関数型言語における停止性検証のためのランキング関数の回帰推定, ソフトウェアサイエンス研究会, 2018.03.
12. 中野 大扉, 亀井 靖高, 佐藤 亮介, 鵜林 尚靖, CVE記述が存在するセキュリティバグ修正に関する調査, ソフトウェア工学研究会, 2018.03.
13. 村本 大起, 佐藤 亮介, 鵜林 尚靖, 亀井 靖高, 高階関数型言語におけるランキング関数の回帰推定, 第34回全国大会ウィンターワークショップ2018・イン・宮島, 2018.01.
14. 金原 雅典, 佐藤 亮介, 鵜林 尚靖, 亀井 靖高, 機械学習を用いたCoq上の命題論理の自動証明, 第34回全国大会ウィンターワークショップ2018・イン・宮島, 2018.01.
15. 村岡 北斗, 亀井 靖高, 佐藤 亮介, 鵜林 尚靖, 不確かさ分析用公開データベースの作成に向けて, 第34回全国大会ウィンターワークショップ2018・イン・宮島, 2018.01.
16. 中野 大扉, 亀井 靖高, 佐藤 亮介, 鵜林 尚靖, セキュリティバグ修正におけるCVE情報の実証実験に向けて, 第34回全国大会ウィンターワークショップ2018・イン・宮島, 2018.01.
17. 金原 雅典, 佐藤 亮介, 鵜林 尚靖, 亀井 靖高, 機械学習によるCoq上の命題論理の自動証明に関する研究, ソフトウェア工学研究会, 2018.03.
18. 西中 隆志郎, 鵜林 尚靖, 亀井 靖高, 佐藤 亮介, ソフトウェア開発履歴情報からのAPI Q&A知識の自動抽出, FOSE2017, 2017.11.
19. 廣瀬 賢幸, 鵜林 尚靖, 亀井 靖高, 佐藤 亮介, Stack Overflowを利用した自動バグ修正の検討, FOSE2017, 2017.11.
20. 中野 大扉, 亀井 靖高, 佐藤 亮介, 鵜林 尚靖, 高山 修一, 岩永 裕史, 岩崎 孝司, OSS事前品質評価における重み付け手法の実証実験, FOSE2017, 2017.11.
21. 三浦 圭裕, 亀井 靖高, 鵜林 尚靖, 佐藤 亮介, OSSプロジェクトにおけるTangledコミットの実証分析, 日本ソフトウェア科学会第34回全国大会, 2017.09.
22. 村本 大起, 江 冠逹, 村岡 北斗, 深町 拓也, 鵜林 尚靖, 亀井 靖高, 佐藤 亮介, ソフトウェア開発における不確かさに着目した OSS コミットログ解析, ソフトウェアエンジニアリングシンポジウム2017, 2017.09.
23. Ryosuke Sato, Naoki Kobayashi, Modular verification of higher-order functional programs, 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, 2017.01, Fully automated verification methods for higher-order functional programs have recently been proposed based on higher-order model checking and/or refinement type inference. Most of those methods are, however, whole program analyses, suffering from the scalability problem. To address the problem, we propose a modular method for fully automated verification of higher-order programs. Our method takes a program consisting of multiple top-level functions as an input, and repeatedly applies procedures for (i) guessing refinement intersection types of each function in a counterexample-guided manner, and (ii) checking that each function indeed has the guessed refinement intersection types, until the whole program is proved/disproved to be safe. To avoid the whole program analysis, we introduce the notion of modular counterexamples, and utilize them in (i), and employ Sato et al.’s technique of reducing refinement type checking to assertion checking in (ii). We have implemented the proposed method as an extension to MoCHi, and confirmed its effectiveness through experiments..
24. Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno, Temporal verification of higher-order functional programs, 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, 2016.01, We present an automated approach to verifying arbitrary omegaregular 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..
25. Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi, Verifying relational properties of functional programs by first-order refinement, ACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015, 2015.01, 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 preliminary implementation and experiments..
26. Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi, Predicate abstraction and CEGAR for disproving termination of Higher-Order functional programs, 27th International Conference on Computer Aided Verification, CAV 2015, 2015.07, We propose an automated method for disproving termination of higher-order functional programs. Our method combines higherorder model checking with predicate abstraction and CEGAR. Our predicate abstraction is novel in that it computes a mixture of under- and overapproximations. For non-determinism of a source program (such as random number generation), we apply underapproximation to generate a subset of the actual branches, and check that some of the branches in the abstract program is non-terminating. For operations on infinite data domains (such as integers), we apply overapproximation to generate a superset of the actual branches, and check that every branch is nonterminating. Thus, disproving non-termination reduces to the problem of checking a certain branching property of the abstract program, which can be solved by higher-order model checking. We have implemented a prototype non-termination prover based on our method and have confirmed the effectiveness of the proposed approach through experiments..
27. Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi, Towards a scalable software model checker for higher-order programs, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013, 2013.02, In our recent paper, we have shown how to construct a fully- automated program verification tool (so called a "software model checker") for a tiny subset of functional language ML, by combin- ing higher-order model checking, predicate abstraction, and CE- GAR. This can be viewed as a higher-order counterpart of previ- ous software model checkers for imperative languages like BLAST and SLAM. The naïve application of the proposed approach, how- ever, suffered from scalability problems, both in terms of efficiency and supported language features. To obtain more scalable software model checkers for full-scale functional languages, we propose a series of optimizations and extensions of the previous approach. Among others, we introduce (i) selective CPS transformation, (ii) selective predicate abstraction, and (iii) refined predicate discovery as optimization techniques; and propose (iv) functional encoding of recursive data structures and control operations to support a larger subset of ML. We have implemented the proposed methods, and obtained promising results..
28. Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno, Predicate abstraction and CEGAR for higher-order model checking, 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'11, 2011.07, Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs..
29. 千葉 知也,佐藤 亮介,松田 一孝,小林 直樹, 関数型プログラムの不変条件のICE流学習手法, 日本ソフトウェア科学会第32回大会, 2015.09.

九大関連コンテンツ

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