システム構築/受託開発

数理的手法とは、計算機科学における数学を基盤としたソフトウェアシステムの仕様記述、開発、検証技術の総称です。ITプランニングでは、この数理的手法をシステム開発に多方面で採用。自動仕様チェックが可能なAlloy、豊かな型付けが可能な関数スタイルプログラミング言語OCaml、動作証明済みのプログラムを作成できる定理証明支援器Coqといった先進の技術を基に、お客様のご要望を素早く正確に実現します。

証券会社様向け情報システム

証券業界(特にFXや株式)の業務知識を背景に、各種情報ツールを開発しております。

  • チャートシステム(詳細はチャートソリューションをご覧ください)
  • iPhone端末, iPad端末, Android端末用FX取引クライアント
  • Windows, Mac用リッチクライアント
  • 金融工学や最適化技術を応用したシステム(オプションの価格付け、リスク評価、高速なバックテストシミュレーションなど)

証明済みプログラム作成/プログラム証明サービス

プログラム定理証明は、プログラムの正しさを検証する形式手法の一つです。プログラム定理証明は、Coq/Agdaなどの定理証明支援系と呼ばれるツールを用いて行います。弊社では、ミッションクリティカルなプログラムに対して、仕様記述と証明されたソフトウェアの作成を承ります。

事例:iZE Smart Desktopミドルウェアの正しさ検証

(株)アイズ様の「スマートデスクトップ・クライアント」の一部モジュールを請負開発し,その際証明支援器Coqを適用しました。(ソフトウェア科学会PPL2010においてポスター発表、TPP10にて発表)