Faculty of Science and Technology

千代 英一郎

チシロエイイチロウ  (Eiichiro Chishiro)

基本情報

所属
成蹊大学 理工学部 理工学科 准教授
学位
情報理工学博士(東京大学)

通称等の別名
Eiichiro Chishiro
J-GLOBAL ID
201501003039130240
researchmap会員ID
B000243692

論文

 12

MISC

 2
  • 中山 寛己, 高野 保真, 千代 英一郎
    情報処理学会論文誌プログラミング(PRO) 10(1) 34-34 2017年1月6日  
    近年,SMTソルバの研究がさかんに行われてきており,様々な制約問題を解けるよう飛躍的に進歩している.しかしながら,SMTソルバは線形制約式の解を短時間で求められることが多いのに対し,高次の制約式の解を求めるのに時間がかかってしまうことがある.たとえば,代表的なプログラム検査であるループ停止性検査等で必要となる複雑な制約式の場合,検査に数日を要することもあり,実用上の課題となっている.この問題に対して,本発表では,変数のとりうる値域を限定した検査を,値域を変えて繰り返すことで,制約式の充足可能性を推定する方法について報告する.それぞれの試行を短い時間で打ち切ることにより,結果が得られないことを避けることができる.In recent years, studies of SMT solvers are conducted flourishingly and progress drastically to be able to solve various constraint satisfaction problems. However, while the SMT solver tends to find solution of linear constraints efficiently, it may take a few days to find solutions of the higher degree constraints needed for checking loop termination. For this problem, we examine methods to estimate the satisfiability of constraints by iterative checking (trial) with range restriction of variables. In this presentation, we report some experimental results about trial.
  • 千代英一郎
    情報処理学会誌 48(7) 759-759 2007年7月  招待有り

書籍等出版物

 1

講演・口頭発表等

 7

教育内容やその他の工夫

 1
  • 年月日(From)
    2014/04/01
    年月日(To)
    2015/03/31
    件名
    2014年度
    概要
     昨年度の受講生からの意見をふまえて,これまでよりもさらに演習の比重を高めた.また,演習問題についても,学生にとって身近で具体性のある題材を選び,講義で説明した抽象的な概念の具体像が描けるように配慮して作成した.演習を通して多くの学生が理解できていないことが判明した事項については,補足説明を行うと共に簡単な例題をその場で解かせ,授業内で疑問点が解決できるように努めた.
     また,昨年度と同様,机上の知識でなく実践につながる知識となるように心がけ,データベースを実際に操作しながら講義で取り上げた技術の効果を確認したり,OSのソースコードを配布し,各種デバイスの制御がどのように実現されているのかを解説する等の取り組みを行った.特に学生が苦手とするハードウェアに密着したプログラミングについては重点的に解説を行った.