高度計算機はHPCテックにお任せください。

　千代研究室様ではプログラミング言語理論・数理論理学にもとづき、プログラムの振る舞いや性質の解析・検証・変換技術の研究に取り組まれています。

　計算機の誕生から半世紀以上経った現代では膨大な数の計算機およびプログラムが交通・金融・医療など各分野で我々の生活を支える基盤として働いており、安心して暮らせる社会を実現するため、このようなプログラムを科学的に分析し、その正しさを確認する手段が求められています。

　本研究室一番の特徴は研究対象がプログラムであるということです。対象プログラムが与えられたときに、そのプログラムの持つ性質（たとえば実行中にエラーが発生することはない等）を静的に調べるための理論や技術を扱います。

　そのようなことは実行してみればわかるのに？　と思うかもしれませんが、実行してわかるのはあるひとつの状況、たとえばひとつの入力パターンにおける動きでしかありません。そうではなく、どのようなときにも成り立つ性質を得るためにはプログラムからその振る舞いを表す数学的モデルを作り網羅的に解析を行う必要があります。物体の動きを調べるときには運動方程式などの微分方程式によって数学的にモデル化するということをしますが、同様のことをプログラムを対象に行うと考えてください。ただし使うのは微分方程式ではなく状態遷移系や論理式を用います。

　研究課題としては、モデルをどう定義すべきか、プログラムからどのようにモデルを生成するか、およびそれをどう調べるかが大きな柱になりますが、これらのすべてにプログラムの意味を数学的に基礎づけるプログラミング言語理論が大きく関係しています。

　下の図は本研究室で扱う代表的な分野です。網羅的に振る舞いを調べるという特徴は、特にプログラムの信頼性やセキュリティのような、不具合が許されない問題を扱うのに適しています。

　ここにあげた分野以外にもデータベース分野やセマンティックweb分野における各種問い合わせ
（これもプログラムの一種です）への応用も検討しており、特にグラフ構造を持つデータを対象に
準同型写像を利用した研究を進めています。

成蹊大学 千代研究室　ホームページ
http://www.seikei.ac.jp/s-net/page/seminar_labo/rikou/labo_chiyo.html

　高度な静音化と安全放熱を両立した静音ラック
　ＨＰＣテック静音化ソリューション

　　　　HPCT-SR45は、マシンの仕様、搭載台数などに応じて最適な放熱マッチング、技術

　　　フィッティングを含めて提供しています。個々の案件に合わせた個別専用仕様とするこ

　　　とで、必要十分な静音性と運用の安全性が担保され、音と熱の課題を供給側責任にて

　　　完全解決いたします。
　　　　汎用製品とは大きく異なり、マシンと組み合わされたコンプリートパッケージで

　　　パーフェクトな結果、成果を用意いたします。

　以前からサーバ室をセミナー室に統合したかったため、静音性が高くサイズもコンパクトな静音ラックサーバは理想的な製品でした。コア数およびメモリ量が多いため熱の問題が若干不安でしたが、導入後熱暴走等のトラブルは一度もなく安定して稼働しています。スペースの制約がある研究室で高並列処理環境を導入する際、良い検討候補になるソリューションだと思います。