大会講演論文集は査読を行っていません。各論文の著作権は各著者に属します。日本ソフトウェア科学会は著作権規定(2011年1月13日制定)第3条(b)にもとづく著作者の許諾に従って公開をしています。
本講演論文集中の論文を引用する場合には、大会講演論文を引用する場合の注意を御覧ください。
The proceedings are non-refereed. Authors of each article retain their copyrights in the article. JSSST publishes the articles under the JSSST copyright policy (in Japanese; January 13, 2011) 3(b).
日本ソフトウェア科学会 編
2023年9月12日～9月14日 東京大学本郷キャンパス
概要: 機械学習や生成モデルの技術が広く使われるようにつれて、今までの「ノイマン型アーキテクチャの計算機で、人が書いたプログラムを走らせる」という計算のやり方が大きく変化しつつある。この講演では、世の中で「計算」とみなせる様々な事象に触れながら、それらを「計算の仕様をどのように与えるか」という観点で分類することを提唱する。その上で、本学会を含むコンピュータサイエンスの研究・実務コミュニティが今後どのような課題にチャレンジすべきかを議論する。
概要: プログラミングの可能性と楽しさをすべての人に伝えたい、という想いでプログラミング言語ビスケットを開発して20年になります。小学生にとても人気のツールに成長しました。なぜ作ることになったのか、ビスケットを通じどのようなメッセージを子供達に伝えてきたか、どのような影響を子供達から受けたか、さらにAIの登場を受けて、これからどう変わるのか。実例とエピソードを交えてお話します。
概要: 本発表では、ChatGPTを用いることで、機能要求や非機能要求から所望のゴールモデル生成が可能なのかの初期実験結果を踏まえて、完成度の高い要求仕様書を生成することを支援するゴールモデル生成器の実現可能性を論じる。まずは、エージェントモデリング技術であるMAPE(Monitor-Analyze-Plan-Execute)-Kによって新人の要求分析者の行動をモデル化することで、外界の定義や活躍するLLMの登場場面と役割、さらにはLLM間の活用・連携プロセス、パターンを整理することが可能であることを示し、ゴールモデル生成器の実現に向けての研究課題を整理する。
概要: 1988年に職業研究者となって以来、いくつかのオブジェクト指向言語の実装に関わってきた。本講演ではその中から、ごみ集め、同期処理、ベンチマークに関するものを紹介し、特に、ごみ集めについては、オブジェクト指向言語の実装史の文脈でも議論してみたい。
概要: プログラミング言語の意味論（特に表示的意味論）と、圏論を介した数学（特に幾何学）との関係について、私が関わってきた事例とそれから学んだ教訓・展望を中心に、ざっくりお話ししたいと思います。
概要: 講演者は20年以上にわたって情報可視化の研究に従事してきた。情報可視化は世界的には現在も研究者が増加していて活発な議論がなされているが、日本ではそれに比べてまだコミュニティが小さいのが実情であり、ますますの普及と発展が望ましいと考えられる。本講演で講演者自身の情報可視化の研究を紹介するとともに、これらの研究が今後どのようにソフトウェア科学への貢献を含めた発展につながるのかを議論する。
概要: 継続は「残りの計算」を表す概念であり、さまざまなドメインで有用となることが知られています。本発表では、私がこれまでの研究で扱ってきた継続の応用例と、これからの研究で取り組む予定の課題について紹介します。
概要: ソフトウェアリポジトリマイニングはソフトウェアの開発履歴などの情報を分析し，ソフトウェア開発者に有用な知見を見つけ出す研究分野である．ここでの知見とは，そのまま開発者が利用可能なものや，機械学習・深層学習を開発履歴などの情報に適用する際に気をつけるべき点のようなものまで，さまざまなものを幅広く含む．そのため，この分野では，多くの研究者がさまざまな観点から研究を進めている．一方で，含む範囲が広すぎることもあり，その魅力や開発者にどのように喜ばれるのかが一見すると分かりにくい．本発表では，発表者の研究を具体例として概説しつつ，ソフトウェアリポジトリマイニングの魅力と，どのような問題を解決して開発者に喜ばれることを目指しているのかについて個人的な考えを紹介する．
概要: 「使いたくなる」アプリケーションを開発するためには、ユーザの課題を的確に捉え、解決する方法を考えることが必要である。そのためには確かなユーザの観察と的確な解決策の提案が必要である。しかし人は目の前のものごとを見る際に情報を簡略化して捉えがちであり、ありのままを見ることは難しい。ステレオタイプに囚われず解決策を考えることも難しい。そこでデザイン教育で用いられている手法をもとに、視点を変えてユーザの視点に気づく2つの手法を用いてデザイン演習を行った。目の前の状況を絵に描くことで見逃していたユーザの状況を捉える「スケッチ法」、思い込みに囚われずに解決策を検討する「異世界比較法」である。これによりユーザが「使いたくなる」視点を見極める力を身につける。
概要: 多くのシステムやサービスがネットワークを介した通信を前提とする中、ネットワーク障害がそれらの通信の阻害や品質の低下をたびたび引き起こしている。世界の様々なネットワーク運用者からの調査の結果、その障害の多くがネットワーク機器の設定間違えや人為的ミスによって発生したことが判明している。それらを防ぐ1つの方法として、形式検証の理論や技術をネットワーク運用に活用し、それらの障害を事前に防いだり、障害発生時に原因をすぐさま突き止めることを目的とする“Network verification”と呼ばれる研究がなされている。本発表では、初めにNetwork verificationの研究背景や動向を簡単に紹介する。次に、大規模ネットワークにおいて高速に、かつ正確にネットワーク障害を発見するために発表者が行った2つの研究を紹介する。ここでは、それら2つの手法を用いて国内最大規模のプライベートクラウドにおけるネットワーク障害の検証を行った結果も紹介する。
概要: アブストラクト：プログラミングにおける基本的な作業の一つに、プログラム同士を比較することがある。例えば2つのプログラムの実行結果が等しいことが分かれば、リファクタリングや最適化の正しさを保証することができるし、一方のプログラムが他方のプログラムより早く実行できると分かれば、最適化の効果を保証することもできる。実行結果の等しさを保証するための数理的手法については様々な研究がありよく知られている。しかし、実行結果の（質的な）等しさとコストの（量的な）違いを同時に保証するための数理的手法については、行われてきた研究が限定的である。本発表では、質的・量的両面からプログラム同士を比較するための手法について、時間コストに注目した発表者の最近の研究を紹介する。
[1-T] PAFL: Probabilistic Automaton-based Fault Localization for Recurrent Neural Networks (トップカンファレンス・トップ論文誌特別講演)
(Information and Software Technology, Volume 155, March 2023, 107--117)
[2-T] ArchRepair: Block-Level Architecture-Oriented Repairing for Deep Neural Networks (トップカンファレンス・トップ論文誌特別講演)
(ACM Transactions on Software Engineering and Methodology, Volume 32, Issue 5, pp.1--31)
[2-R-S] CTの思考育成を促進するプログラミング協働学習の提供
[5-R-S] 消費期限お知らせシステムの開発
[6-R-S] 複合現実デバイスを用いた模様替え補助システムの開発
[7-R-S] 道幅における個人の嗜好を考慮した 道案内システムの開発
[3-T] Envisioning software engineer training needs in the digital era through the SWEBOK V4 prism (トップカンファレンス・トップ論文誌特別講演)
[4-T] A Method to Semi-Automatically Identify and Measure Unmet Requirements in Learner-Created State Machine Diagrams (トップカンファレンス・トップ論文誌特別講演)
[10-R-S] べき集合クオンテールの別表現の発見
[11-R-S] アローに対する代数的エフェクトとエフェクトハンドラ
[14-R-S] 再帰的なグラフパターンに基づく反復パターンマッチングの効率化手法
[15-R-S] 同期的データフロープログラミングにおける逆計算の構成方式
[5-T] A Sound and Complete Algorithm for Code Generation in Distance-Based ISA (トップカンファレンス・トップ論文誌特別講演)
[6-T] Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake? (トップカンファレンス・トップ論文誌特別講演)
(PLDI 2023: Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI, pp.591–-614)
[17-R] 様相論理による統計的因果の形式化
[22-R] 段階的再構築における依存関係分析を用いた費用対効果の試算
[7-T] Towards Scalable Model Checking of Reflective Systems via Labeled Transition Systems (トップカンファレンス・トップ論文誌特別講演)
(IEEE Transactions on Software Engineering, Volume: 49, Issue: 3, pp.1299--1322, 2023)
[28-R-S] アジャイル開発を行うPBLチームの心理的安全性を測定するシステムの提案
[30-R-S] 3DCGを活用したプログラミング教育教材開発の試み
[32-R] 実務で使われるコードクローン検出・追跡システムをめざして
[8-T] An empirical study of issue-link algorithms: which issue-link algorithms should we use? (トップカンファレンス・トップ論文誌特別講演)
Empirical Software Engineering, Volume 27, P.136, 2022
[34-R-S] グラフ書換え言語におけるグラフ操作の軽量かつ静的な型検査
[36-R-S] 慣用句単位のコード翻訳を応用したプログラミング支援の提案
[38-R] 大規模言語モデルを用いたプログラミングを支援する言語機構
[40-R-S] 異なる定理証明支援系間の証明の再利用に向けた帰納型の変換
[42-R] 深層学習モデルコンパイラにおけるAIチップ用コード最適化
[1-I] 強化学習における不確実性説明手法の検討 (MLSE招待発表: 第6回機械学習工学ワークショップ最優秀発表賞)
[44-R-S] GPTを用いたデスクトップ・エージェント・システムの開発
[45-R-S] プロンプト作成の負荷を軽減する生成系AIを用いた学習支援ツールの提案
[49-R-S] 機械学習を用いた悪性Pythonパッケージの検出
[51-R] いくつかの組合せ子の非停止性
[52-R] 時間的性質類の言語的及び位相的特性
[53-R] 仮想人体生成モデルにおける品質管理
[54-R-S] 機械学習を用いたテーマパークのアトラクション待ち時間予測手法の確立
[9-T] A Generalized Backward Compatibility Metric (トップカンファレンス・トップ論文誌特別講演)
[55-R-S] SATySFi におけるドメイン固有型エラー診断
[56-R-S] 対話性と十分な実行速度を両立した組み込みマイコン向け開発環境の提案
[57-R-S] 学習者自身が物理現象をモデル化するシミュレータ SimSym の提案
[59-R-S] あがり症のためのプレゼンテーション補助システムの開発
[1-P] Formal Verification of Automated Driving: RSS and Safety Architectures
Abstract: We present our work on Responsibility-Sensitive Safety (RSS). RSS is a methodology to mathematically prove safety of automated driving. We formalise driving scenarios as programs containing differential equations. We develop dFHL, a logic based on Hoare logic, to prove properties of such programs. This allows us to prove properties of complex scenarios. Safety architectures, and in particular the simplex architecture, play a crucial role in safety of automated driving. We extend dFHL with proof rules tailored to prove properties of safety architectures. This allows us to formally define of the simplex architecture and formally prove its safety, as well as define new architectures and prove their safety.
[2-P-S] 生体情報に基づくデザイン思考要求獲得手法の提案
概要: ユーザの問題解決や新たなアイデア創出のためにデザイン思考が注目されている．要求獲得の場面で，ユーザが言葉では賛成を表明していても，困っていたり，ストレスを感じている場合がある．要求獲得において，ユーザの非言語要求を積極的に考慮することは重要である．本研究では，生体情報を活用して要求獲得することで，非言語要求を特定し，ユーザの真の要求を明らかにする手法を提案する．具体的には，デザイン思考による要求獲得ワークショップにおいて，カスタマージャーニーマップによる問題定義とアイデア創出の過程で，鼻部皮膚温度と脳波による生体情報を活用する．加えて，作成したカスタマージャーニーマップの「Thinking」と「Feeling」に，生体情報の計測結果を融合させて，言語からは浮かび上がらなかった感情を可視化し，ユーザの課題や解決策への賛成度合をより詳細に獲得する．
[3-P-S] 論理制約付き項書き換えシステムにおける末尾再帰変換の正当性証明と実装
概要: 論理制約付き項書き換えシステム(西田&Kop,2013)は項書き換えシステムを拡張した計算モデルの一つであり、論理制約をつけ加えた書き換え規則を用いることで通常の項書き換えシステムでは扱えない組み込み型を利用した計算を行うことができる体系である．末尾再帰関数とは再帰関数の特殊なケースであり、末尾再帰関数を用いた再帰プログラムはオーバーヘッドの少ないコードへコンパイルできることが知られている．このため、末尾再帰変換の様々な研究が行われており、項書き換えシステム上の末尾再帰変換とその変換の正しさが示されている(西田&Vidal,2014)．本研究では、先行研究の末尾再帰変換を論理制約付き項書き換えシステムへと拡張し、その変換の正しさを証明すると共に、その変換システムの実装を行った．
[4-P-S] 条件付き項書き換えシステムの危険対条件に基づく合流性検証
概要: 項書き換えシステム(TRS)は等式論理に基づく計算モデルである．TRSに条件部の記述を許して拡張したものを条件付き項書き換えシステム(CTRS) という．合流性はどのような計算順序を使っても同じ計算結果が得られるという性質であり，非決定的な計算を持つTRS において重要な性質である．CTRSの合流性を保証する危険対条件が提案されている(芳賀ら,2023)．しかし，その危険対条件をどのようにプログラム上で検証するか未解決であった．CTRSにおける合流性検証手法の一つとして条件付き危険対の実行不可能性の自動検証法が研究されている(Gutierrez and Lucas,2020)．本研究ではその手法を参考にして，定理自動証明器Prover9を用いた危険対条件の自動検証を試みる．実行不可能性検証では用いられない階層について符号化手法を検討するとともに，階層の性質を利用した検証方法を提案する.
[5-P-S] VASSからVASへの変換の MathCompによる形式化
概要: VAS(Vector Addition System)とVASS(Vector Addition System with State)は状態遷移系の一種であり、VASSからVASへの到達可能性を保つ変換がHopcroftとPansiotにより示されている。本研究では、この変換をMathComp上で形式化しただけでなく、証明に用いられていた条件を一般的なものに拡張した。またHopcroftらの変換の改良を与え、その最小性も形式化した。
[6-P-S] 階層グラフ書換え言語による線形論理のカット除去のエンコーディング
概要: 階層グラフ書換え言語LMNtalは，グラフ(接続構造)と膜(階層構造)を同時に扱う機能を持つプログラム言語である．本研究では，LMNtalでMultiplicative Exponential Linear LogicのProof Netsとカット除去による簡約が簡潔にエンコード可能であることを示す．これにより，LMNtal処理系のモデル検査機能によってカット除去に対する状態空間構築等が可能となることが期待される．
[7-P] リファクタリングのメリットを提示することによる効果の分析に向けた試み
概要: リファクタリングを実施するメリットを提示することで，リファクタリングを行う動機付けや学習に対する効果を分析するために学習教材を作成し，情報系学部の学生を対象として作成した学習教材による効果を分析する．本研究では，コードを読みやすくするリファクタリングについて，リファクタリングを行うことのメリットを提示した学習教材とメリットを提示しない学習教材を作成し，被験者を2つの群に分け，学習教材の違いによる効果を分析する．
[8-P] 後方参照と先読み付き正規表現の所属性判定問題 ∈ NL
概要: 野上と寺内により、後方参照付き正規表現の言語クラスREWBがindexed languages (IL)に含まれることが示された。ILはindexed grammar等で特徴づけられ、所属性判定問題—既知の文法Gに対し、入力された文字列sについて s ∈? L(G) を判定するもの—は入力の長さに関しNP完全である。一方で、REWB R と 文字列s の両方が与えられた時に s ∈? L(R) を判定する問題（区別のためマッチング問題と呼ぶ）も、AhoによりNP完全性が示されている。所属性判定問題は文法が既知の分、マッチング問題より容易になりうるが、既知の結果では計算量クラスとしては両者に差がない。本発表では、REWBとこれに先読みをつけた拡張の所属性判定問題がNL (Nondeterministic logspace)であることを述べる。