東北大学大学院 情報科学研究科 情報基礎科学専攻 小林･住井研究室

This Page
Home

Main Contents

研究の概要

小林・住井研究室では，型システムなどの手法を利用したプログラム解析の研究を行っています．

近年，交通システム，医療機器，電子政府，電子商取引等，あらゆる社会基盤がコンピュータによって制御されつつあります．このような状況においては，ソフトウェアの欠陥が人命や財産の喪失という重大な事態を引き起こします．そこで，当研究室では，しっかりとした理論的土台に基づいたプログラミング言語処理系やプログラム検証ツールを構築することにより，正しく安全なソフトウェアの開発を支援することを目指しています．

新着情報

2011/11/11 受賞 住井准教授が日本IBM科学賞を受賞しました．
2011/11/1 受賞 住井准教授がRIEC Award東北大学研究者賞を受賞しました．
2011/06/09 受賞 小林教授が日本ソフトウェア科学会基礎研究賞を受賞しました．
2011/06/09 受賞 卒業生の上嶋氏と住井准教授が日本ソフトウェア科学会論文賞を受賞しました．
2011/06/07 発表 ポスドクの海野氏がPLDI 2011（プログラミング言語の設計と実装に関する国際会議）にて，論文"Predicate Abstraction and CEGAR for Higher-Order Model Checking"(小林教授，D2の佐藤亮介君との共著)に関する発表を行いました．
2011/03/29 発表 小林教授がFoSSaCS 2011（ソフトウェア科学と計算の構造の基礎に関する国際会議）にて，論文"A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes"に関する発表を行いました．
2011/03/28 発表 D3のAdrien Pierard君がFoSSaCS 2011（ソフトウェア科学と計算の構造の基礎に関する国際会議）にて，論文"Sound Bisimulations for Higher-Order Distributed Process Calculus"(住井准教授との共著)に関する発表を行いました．
2011/02/28 講演会 国立情報学研究所の定兼邦彦氏をお招きして講演会を行いました．
2010/12/14 講演会 Aarhus UniversityのOlivier Danvy氏をお招きして講演会を行いました．
2010/12/03 講演会 Trinity College DublinのVasileious Koutavas氏をお招きして講演会を行いました．
2010/12/01 発表 ポスドクの海野氏がAPLAS 2010（プログラミング言語およびシステムに関するアジア会議）にて，論文"Verification of Tree-Processing Programs via Higher-Order Model Checking"に関する発表を行いました．
2010/10/21 講演会 CNRSのDavid Monniaux氏，Thomas Gawlitza氏をお招きして講演会を行いました．
2010/07/26 受賞 住井准教授がマイクロソフトリサーチ日本情報学研究賞を受賞しました．
2010/06/17 講演会 Institute of Cybernetics, Tallinn University of TechnologyのKeiko Nakata氏をお招きして講演会を行いました．
2010/03/26 発表 M2の塚田武志君がFoSSaCS 2010（ソフトウェア科学と計算の構造の基礎に関する国際会議）にて，論文"Untyped Recursion Schemes and Infinite Intersection Types"に関する発表を行いました．
2010/01/22 発表 小林教授がPOPL 2010（プログラミング言語の原理に関する国際会議）にて，論文"Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification"に関する発表を行いました．
2010/01/20 発表 寺内助教がPOPL 2010（プログラミング言語の原理に関する国際会議）にて，論文"Dependent Types from Counterexamples"に関する発表を行いました．
2009/12/15 発表 住井准教授がAPLAS 2009（プログラミング言語およびシステムに関するアジア会議）にて，論文"The Higher-Order, Call-by-Value Applied Pi-Calculus"に関する発表を行いました．
2009/11/09 講演会 京都大学の四熊尚方氏をお招きして講演会を行いました．
2009/10/21 講演会 神戸大学の江口直日氏をお招きして講演会を行いました．
2009/09/15 講演会 東京大学の川本裕輔氏をお招きして講演会を行いました．
2009/09/09 発表 ポスドクの海野氏がPPDP 2009（宣言的プログラミングの原理と実践に関する国際会議）にて，論文"Dependent Type Inference with Interpolants"に関する発表を行いました．
2009/09/08 発表 住井准教授がCSL 2009（計算機科学論理学に関する欧州会議）にて，論文"A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References"に関する発表を行いました．
2009/09/07 発表 小林教授がPPDP 2009（宣言的プログラミングの原理と実践に関する国際会議）にて，論文"Model-Checking Higher-Order Functions"に関する発表を行いました．
2009/08/12 発表 小林教授がLICS 2009（計算機科学における論理に関する国際会議）にて，論文"A Type System Equivalent to Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes"に関する発表を行いました．
2009/08/10 発表 D1の安岡宏俊君がSAS 2009（静的解析に関する国際会議）にて，論文"Polymorphic Fractional Capabilities"に関する発表を行いました．
2009/07/22 講演会 東京大学の松田一孝氏をお招きして講演会を行いました．
2009/07/05 発表 小林教授がICALP 2009（オートマトン，言語およびプログラミングに関する国際会議）にて，論文"Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus"に関する発表を行いました．
2009/07/01 発表 M2の塚田武志君がTLCA 2009（型付ラムダ計算とその応用に関する国際会議）にて，論文"A Logical Foundation for Environment Classifiers"に関する発表を行いました．
2009/05/26 受賞 寺内助教が野口研究奨励賞を受賞しました．
2009/05/08 講演会 京都大学の五十嵐淳氏をお招きして講演会を行いました．
2009/03/26 発表 住井准教授がESOP 2009（プログラミングに関する欧州会議）にて，論文"A Theory of Non-Monotone Memory (Or: Contexts for free)"に関する発表を行いました．
2009/03/26 発表 M2の菊地大介君がESOP 2009（プログラミングに関する欧州会議）にて，論文"Type-Based Automated Verification of Authenticity in Cryptographic Protocols"に関する発表を行いました．
2009/03/24 講演会 国立情報学研究所のZhenjiang Hu氏をお招きして講演会を行いました．
2009/02/26 講演会 電気通信大学の中野圭介氏をお招きして講演会を行いました．
2009/01/30 受賞 小林教授が日本学術振興会賞を受賞することが決まりました．
2009/01/24 発表 M1の佐藤亮介君がPLAN-X 2009（XMLのためのプログラミング言語技法に関する国際ワークショップ）にて，論文"Ordered Types for Stream Processing of Tree-Structured Data"に関する発表を行いました．
2009/01/23 発表 小林教授がPOPL 2009（プログラミング言語の原理に関する国際会議）にて，論文"Types and higher-order recursion schemes for verification of higher-order programs"に関する発表を行いました．
2008/12/18 講演会 京都大学の照井一成氏をお招きして講演会を行いました．
2008/12/10 発表 ポスドクの末永君がAPLAS 2008（プログラミング言語およびシステムに関するアジア会議）にて，論文"Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References"に関する発表を行いました．
2008/11/21 講演会 国立情報学研究所の龍田真氏をお招きして講演会を行いました．
2008/10/21 講演会 京都大学の長谷川真人氏をお招きして講演会を行いました．
2008/10/15 講演会 東京大学の稲葉一浩氏をお招きして講演会を行いました．
2008/09/17 講演会 京都大学の蓮尾一郎氏をお招きして講演会を行いました．
2008/09/12 講演会 Coverity社のJohn Kodumal氏をお招きして講演会を行いました．
2008/08/06 講演会 MITの梅野真也氏をお招きして講演会を行いました．
2008/07/18 受賞 小林教授と大崎人士博士（産業総合技術研究所）による論文"Tree Automata for Non-Linear Arithmetic"が，RTA 2008（項書換えと応用に関する国際会議）にて，最優秀論文賞を受賞しました．
2008/07/10 発表 小林教授がCAV 2008（コンピュータ支援検証に関する国際会議）にて，論文"A Hybrid Type System for Lock-Freedom of Mobile Processes"に関する発表を行いました．
2008/06/25 発表 寺内助教がCSF 2008（コンピュータセキュリティの基礎に関する国際会議）にて，論文"A Type System for Observational Determinism"に関する発表を行いました．
2008/06/17 WEB ホームページを更新しました．
2008/06/13 講演会 京都大学の五十嵐淳氏をお招きして講演会を行いました．
2008/06/09 発表 寺内助教がPLDI 2008（プログラミング言語の設計と実装に関する国際会議）にて，論文"Checking Race Freedom via Linear Programming"に関する発表を行いました．
2008/05/30 受賞 元M2の須藤崇君と小林教授による論文「並行プログラミング言語へのチャネル使用法宣言の導入」が，平成19年度情報処理学会論文賞を受賞しました．
2008/04/19 受賞 住井准教授が「再帰的高階言語におけるプログラム等価性証明手法」に関する研究により，第7回船井情報科学奨励賞を受賞しました．
2008/04/16 発表 小林教授がFLOPS 2008（関数型・論理型プログラミングに関する国際会議）にて，招待講演"Substructural Type Systems for Program Analysis"を行いました．
2008/04/15 発表 D3（東京大学より指導委託）の海野君が，FLOPS 2008（関数型・論理型プログラミングに関する国際会議）にて，論文"On-Demand Refinement of Dependent Types"に関する発表を行いました．
2008/04/01 発表 寺内助教がESOP 2008（プログラミングに関する欧州会議）にて，論文"Inferring Channel Buffer Bounds via Linear Programming"に関する発表を行いました．
2008/04/01 発表 M2の金子君がESOP 2008（プログラミングに関する欧州会議）にて，論文"Linear Declassification"に関する発表を行いました．