TSSS(Tsukuba Software Science Seminar)

Tsukuba Software Science Seminar is a seminar, consisting of research talks on theory and practice of computer software and related topics.. The seminar is held in the University of Tsukuba or AIST Tsukuba site.

Suggestions are welcome; if you have suggestion for talks on programming languages, formal methods including program analysis and verification, or related research fields, please send it to the organizers by e-mail (tsss-kanji(at)logic.cs.tsukuba.ac.jp).

TSSS 2022-1

Date:    Jan. 27 (Thu), 2022,  15:00-
Place:   Zoom Virtual Meeting 
Speaker: Aart Middeldorp (Professor, University of Innsbruck)
         http://cl-informatik.uibk.ac.at/users/ami/

Title:   Synthesis in the First-Order Theory of Rewriting

Abstract:

The first-order theory of rewriting is decidable for linear,
variable-separated rewrite systems. In this theory important
properties of rewrite systems like termination, confluence and
normalization are readily expressed. The decision procedure is
based on tree automata techniques and implemented in FORT. In this
presentation I will be present recent results on synthesizing
rewrite systems that satisfy properties expressible in the
first-order theory as well new results on deciding properties on
non-ground terms.

The presentation is based on joint work with Alexander Lochmann
and Fabian Mitterwallner.

TSSS 2019-1

日時:11月22日(金)15時〜17時
会場:筑波大学総合研究棟B 11階 1111号室
話者:角田健太郎(首都大)
表題:対称ラムダ計算の型規則と古典論理的推論

概要:
 1990年代から2000年代にかけてさかんに研究された古典論理体系と対応する計算体系に関する諸研究を踏まえ、Gent-zen(1934,1935)のNKとは異なる仕方での古典自然演繹体系の形式化の方法(特に、NKのように自然演繹の推論規則間の対称性を崩してしまうことのないような形式化の方法)を考察し、計算体系の関数構成に寄り添うような古典論理的推論とはどのような形をしているのかを報告する。
 より具体的には、Filinski(1989)により提案され、浅井・阪上・上田ら(2009,2010)により再形式化された対称ラムダ計算(symmetric lambda calculus、以降SLCと呼ぶ)の研究をまず紹介し、そして浅井らの研究もとに発表者が作った、SLCと同等で、かつ計算状態の入れ子を許すような機構を持つ計算体系およびその型規則と対応する古典自然演繹体系を定義し、その推論図式の読み下し方を報告する。

自己紹介:
 角田健太郎(つのだけんたろう)と申します。首都大学東京の哲学科の博士課程に所属しております。
 これまで、法政大学で安東先生に論理学を教わり、首都大学東京で岡本先生に論理学の哲学を教わり、そして最近(竹内さんが紹介してくださり)東邦大学の木村先生に計算論理を教わりました。
 何を疑問に思い、研究しているのかを述べます。まず、初めて自然演繹を教わったときから、NK証明図を書くことがNJ証明図を書くことに比べてとても難しいことの理由が気になっていました。また束論の勉強をしていて相対擬補元と論理記号⊃(ならば)の関係を知ったときから、⊃の双対の論理記号に関する推論規則をどうにかして使えば、古典自然演繹をもっと簡単に書くことができるのではないか、と気になっていました。
 今年に木村先生より継続計算と論理に関する研究を教わってからは、上の疑問が解かれる光がさして興奮しています。最近は継続を扱う計算体系と古典論理体系の関係を調べています。
 何とぞよろしくお願いします。

TSSS 2017-3


Date:      June 7 (Wed), 2017
Time:      14:00〜
Place:     SB1111 (11th floor, Sogokenkyuto-B, Univ. of Tsukuba)  
           (筑波大学 総合研究棟B 1111号室)
Speaker:   山本 和彦 (IIJ Innovation Institute)
Title:     OCamlerのためのHaskellの並行機能入門

Abstract: 

8年間Haskellでネットワークのライブラリやサーバを作って来た経験からいう
と、Haskellは素早いプロトタイピングを可能にし、高度で安全な並行機能を
提供しています。素早いプロトタイピングが可能であるのは、豊かな型と強力
な型システムのおかげであり、この点はOCamlも同等です。一方で、OCamlと比
べると、高度で安全な並行機能はHaskell特有と言えるでしょう。この講義で
は、Haskellの並行機能として、軽量スレッドやSTM(Software Transactional
Memory)を説明します。また、遅延評価が実戦で本当に役立つ例も紹介します。

著者ホームページ:  http://www.mew.org/~kazu/

TSSS 2017-2


Date:      Mar 16 (Thu), 2017
Time:      15:00-
Place:     SB1014 (10th floor, Sogokenkyuto-B, Univ. of Tsukuba)  
           (筑波大学 総合研究棟B 1014号室)
Speaker:   Mohammad Reza Mousavi (Halmstad University, Sweden)
Title: 	   Model-Based Testing Cyber-Physical Systems

Abstract: Cyber-physical systems are the result of the omnipresent and
tight integration of computation and communication infrastructures with
physical devices and human beings. This tight integration leads to enormous
challenges in the design and verification of such systems. Model-based
testing is a rigorous verification technique, which is recently adapted to
deal with cyber-physical systems. In this talk, we present an overview of
the challenges facing model-based testing of cyber-physical systems. These
involve defining a formal notion of conformance on hybrid systems as well
as sound and efficient algorithms for test-case generation and conformance
analysis. We provide an overview of our ongoing research in these
directions.

(Joint work with: Arend Aerts (TU/Eindhoven),  Gustavo Carvalho (UF de
Pernambuco) , Hugo Leonardo  (UF de Pernambuco), Morteza Mohaqeqi (Uppsala
U), Michel A. Reniers (TU/Eindhoven), and Augosto Sampaio (UF de
Pernambuco))

Biography:

Mohammad Mousavi is a professor of Computer Systems Engineering at Halmstad
University and a guest professor of Software Engineering at Chalmers
and Gothenburg University, Sweden. He received his Ph.D. in Computer Science
in 2005 from Eindhoven University of Technology, The Netherlands.
Since then, he has been postdoctoral researcher (2006-2007) at Reykjavik
University, Iceland, and assistant and associate professor (2005-2013) at
TU Eindhoven. He is an editor of Science of Computer Programming and
PeerJ Computer Science. He is also the co-authors of Modeling and Analysis
of Communicating Systems, published by the MIT Press. His research interests
are in model-based testing and formal verification.

http://ceres.hh.se/mediawiki/index.php/Mohammad_Mousavi

TSSS 2017-1

Date:      Jan 19 (Thu), 2017
Time:      14:00-15:00
Place:     SB1014 (10th floor, Sogokenkyuto-B, Univ. of Tsukuba)  
           (筑波大学 総合研究棟B 1014号室)
Speaker:   戸澤 一成 (東京大学 数理科学研究科)
Title: 	   メタラムダ計算を用いた限定継続への意味付け

Abstract:
 本講演では,メタラムダ計算を用いた限定継続への意味付けを紹介する.
限定継続演算子は,計算の各時点において参照する限定子が異なるという意味
で,動的な性質を持つ.この動的性質は,メタラムダ計算における textual
substitution との間に類似性がある.この類似性に着目し,メタラムダ計算
をターゲットに持つ新たなCPS変換を構成した.新たなCPS変換は,限定継続演
算子の動的性質に対し直接的な特徴付けを与えるものである.これにより限定
継続を扱う計算体系の公理系に対し,メタラムダ計算の機構を用いた統一的な
説明を与えることができる.また,answer-type modification を許す型
体系に対し,contextual modal typeとの対応を与える.

TSSS 2016-2

Date:      Oct 24 (Mon), 2016
Time:      15:00-16:00
Place:     産総研本部情報棟6階第10会議室(06306)
Speaker:   井上健太(千葉大学理学研究科)
Title: 	   代数ニューラルネットワークのCoqにおける形式化

Abstract:
 今日、機械学習の分野で、ニューラルネットワークと呼ばれるグ
ラフを用いて学習を行う、ディープラーニングと呼ばれる手法が大
きな注目を集めている。しかし、このニューラルネットワークにお
いてその学習が行われるメカニズムや、与えられた問題に対し、そ
れを解くのに最適な構造が判明しておらず、また学習後のニューラ
ルネットワークの正当性の判定もあいまいである等、ブラックボッ
クスとして利用されているのが現状である。本研究の目的はニュー
ラルネットワークの構造を数学的な手法で解明することである。
 具体的な研究方法としては、ニューラルネットワークを代数を用
いて記述し、これのもつ性質を調べることでニューラルネットワー
クの構造がもつ性質を解析を行う。
 また、この代数ニューラルネットワークを証明支援系Coqで形式
化する。
 本発表では、Coqで形式化した代数ニューラルネットワークの定
義やいくつかの性質、それらをまとめたライブラリを紹介する。
 また、それを用いて符号問題と呼ばれるEXOR問題を一般化した問
題の解の存在性の証明も行い、この結果から階層型ニューラルネッ
トワークを多層化することへの考察を発表する。

TSSS 2016-1

Date:      Aug 31 (Wed), 2016
Time:      13:00-14:00 (pm)
Place:     SB1014 (10th floor)  (筑波大学 総合研究棟B 1014号室)
Speaker:   Rene Vestergaard 
Title: 	   Principles and mechanisms of molecular-biology reasoning
           (分子生物学における推論の原理と仕組み)

Abstract:
  Science relies on external correctness, involving statistics and
reproducibility. Mathematics relies on internal correctness, where
reasoning must be able to be formalized within a consistent axiomatic
system (read: a logic). At first sight, these two correctness
notions appear to be entirely unrelated, with mathematics seemingly
unable to help with the current reproducibility crisis throughout
science.

We show that molecular-biology reasoning can be formalized the way
_Principia Mathematica_ did for mathematics and that the resulting
axiomatic system enjoys its own Curry-Howard-style Correspondence
between the logic and an induced computational side. Computationally,
molecular-biology reasoning amounts to a process calculus and we
discuss the relevant trace-monoid construction that sequentializes the
considered concurrent computation. The big reveal in this talk will be
that this allows us to predict the possible life-cycles of a
considered organism from its molecular programming: its `genotype',
via standard computational considerations of its (open-system)
execution: its `phenotype'. We call this new type of information an
organism's `synchrotype'. We will also sketch how the computational
understanding allows us to simulate organisms, thereby bridging
internal and external correctness. The simulation machine is actually
the equivalent of a proof assistant, only presented visually. The work
will be illustrated with our complete verification of the internal
correctness of the standard molecular-biology reference: "A Genetic
Switch, 3rd Edition".

Time permitting, the audience will be invited to speculate about the
meaning of the constructed logic's cut rule and other technical
issues.

TSSS 2015-7

Date:      Dec 14 (Mon), 2015
Time:      15:15-16:15 (pm)
Place:     SB1111 (11th floor)  (筑波大学 総合研究棟B 1111号室)
Speaker:   廣川直(JAIST)
Title: 	   等式推論と完備化

Abstract:
1970年、Knuth と Bendix は等式を自動証明する完備化手続きを考案し、
等式を扱う現代の定理自動証明システムの礎を築いた。完備化は与えられ
た等式公理を同値変形してゆき、完備性(停止性と合流性)を持つ項書換
えシステムへ変換する手法である。ひとたび完備なシステムが得られれば、
等式の成立・不成立は単純な計算で決定できるようになる。

本発表では完備化の基礎を振り返ったのち、MaxSAT を利用する最新の完
備化手法(極大完備化)を紹介する。

TSSS 2015-6

Date:      Jul 17 (Fri), 2015
Time:      11:00-12:00 (am)
Place:     SB1112 (11th floor)  (筑波大学 総合研究棟B 1112号室)
Speaker:   川本裕輔 (産総研)
Title: 	   統計的手法によるJavaプログラムの定量的情報流解析

Abstract:
定量的情報流解析(quantitative information flow analysis)は、
システムの出力データに漏洩する秘密情報の量を計算する解析技術
であり、最近十数年間、盛んに研究されてきた。この解析技術では、
システムの出力データと秘密情報の間の対応関係を、情報理論にお
ける通信路としてモデル化し、エントロピーを用いて秘密情報の量
を定義する。本研究では、従来技術における状態爆発を避けるため
に、統計的手法を用いて、プログラムから漏洩する秘密情報の量を
推定する手法を提案する。具体的には、Javaプログラムをランダム
に何度も実行して得られるトレース集合から漏洩情報量を統計的に
推定し、95%信頼区間を計算する。本発表では、我々が開発した解
析ツールleakiEstとLeakWatchを紹介し、いくつかのシステムの解
析例を通じて、技術の有効性を実証する。

TSSS 2015-5

Date:      Jun 22 (Mon), 2015
Time:      15:00-16:00 (pm)
Place:     SB1014 (10th floor)  (筑波大学 総合研究棟B 1014号室)
Speaker:   中正和久 (信州大学 大学院総合工学系研究科)
Title: 	   Mizarライブラリにおける検索・閲覧技術の研究

Abstract:
近年、Feit-Thompsonの定理やケプラー予想の厳密証明など、定理証明支援系
が比較的複雑な問題を扱うケースが増えており、これに伴って、形式検証ライ
ブラリの大きさは増加の一途を辿っている。ライブラリの発達は、定理・定義
の再利用性を高め、証明作業を効率化させる反面、利用者がライブラリの全容
を把握して、必要な定理・定義を探し出すことを困難にする。本講演では、こ
のような問題に対するMizarコミュニティの取り組みを紹介するとともに、今
後の展望について考察を述べたい。

TSSS 2015-4

Date:      Apr 23 (Thu), 2015
Time:      15:30-16:30 (pm)
Place:     SB1001 (10th floor)  (筑波大学 総合研究棟B 1001号室)
Speaker:   新屋良磨(東京工業大学 大学院情報理工学研究科)
Title: 	   正規言語と代数と論理の対応:An Introduction to Eilenberg’s
           Variety Theorem

Abstract:
正規表現やオートマトンが正規言語の表現方法であることは情報系の方々には
広く知られていますが,一方で代数や論理でも正規言語が特徴づけられるとい
うことはあまり知られていません.本発表では variety という視点から眺め
ることで,言語・代数・論理の三つの異なる概念が非常に美しい対応を見せる
ことを紹介していきます.

TSSS 2015-3

Date:  Mar. 23, 2015
Place: National Institute of Advanced Industrial Science and
Technology (AIST), Tsukuba central, AIST Tsukuba Headquarters and
Information Technology Collaborative Research Center
Map: map1 map2

10:00 - 10:45 Runtime verification using a process algebra CSP,
Yoriyuki Yamagata
10:45 - 11:00 Discussion
11:00 - 13:00 Break
13:00 - 13:45 Applying Formal Methods in Trust and Security systems, Liu Yang
13:45 - 14:00 Discussion
14:00 - 14:15 Break
14:15 - 15:00 Using Model Checking and Theorem Proving to Validate and Verify
Cyber-Physical Systems, Chen-wei Wang
15:00 - 15:15 Discussion


Title: Runtime verification using a process algebra CSP
Speaker: Yoriyuki Yamagata
Abstract:
A process algebra such as CSP, CCS, and pi-calculus is used to
describe a concurrent system. In this talk, we introduce a tool called
CSP_E, CSP for event monitoring. CSP_E tests a runtime log against a
specification given by CSP, and report whether the log satisfies the
given specification or not. CSP_E is implemented as a internal DSL
within Scala programming language.

Title: Using Model Checking and Theorem Proving to Validate and Verify
Cyber-Physical Systems
Speaker: Chen-wei Wang
Abstract:
In this talk I present part of the results that contribute to the
research project "Certification of Safety-Critical Software-Intensive
Systems" funded by the Ontario government. The project involves
various application domains: biomedical, automotive, and nuclear. This
talk focuses on the nuclear domain. Contributions are made by
researchers at York University and McMaster University. I first
present the use of an automated checking tools for Timed Transition
Models (TTM) to model, simulate, and validate cyber-physical systems,
with respect to discrete-time temporal properties. I then present the
use of tabular expressions and the PVS theorem prover to model and
verify function blocks that can be reused to build Programmable Logic
Controllers (PLCs). In both approaches, I use function blocks supplied
by the industrial standard 61131-3 for illustration. To conclude the
talk, I report lessons that we learn and mention ongoing research.

Title: Applying Formal Methods in Trust and Security systems
Speaker: Liu Yang
Abstract:
Cyber-attack detection, defense and recovery are important topics in
cybersecurity, but the ultimate goal of cybersecurity is to build
attack-free systems. Security verification and building attack-free
systems are very challenging tasks in view of the size and the
complexity of the systems. In this talk, we will present our recent
attempts in applying formal methods in modeling and verifying security
protocols, security protocol implementations, malware in Android OS
and even vulnerabilities. We will also discuss the challenges in
applying formal methods in security and possible solutions. Lastly, we
will introduce our recent research project “Securify: A Compositional
Approach of Building Security Verified System”, which aims at building
secure and verifiable systems ground-up.

Short Bio: Dr Liu Yang graduated in 2005 with a Bachelor of Computing
(Honours) in the National University of Singapore (NUS). In 2010, he
obtained his PhD and started his post doctoral work in NUS, MIT and
SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at
NUS to be the Principal Investigator in the area of Cyber Security. In
2012 fall, he joined School of Computer Engineering, Nanyang
Technological University as a Nanyang Assistant professor.

Dr. Liu specializes in software verification, security and software
engineering. His research has bridged the gap between the theory and
practical usage of formal methods to evaluate the design and
implementation of software for high assurance. His work led to the
development of a state-of-the-art model checker, Process Analysis
Toolkit (PAT). This tool is used by research institutions in over 70
countries for research and education. He has more than 100
publications and leading a research group of 30 people.

TSSS 2015-2

Date:      Mar 17 (Tue), 2015
Time:      14:00-15:00 (pm)
Place:     SB1111 (11th floor)  (筑波大学 総合研究棟B 1111号室)
Speaker:   木下 佳樹 (神奈川大学)
Title: 	   命令型プログラムの簡単な証明体系について

Abstract:

学部の学生を対象に、ホア論理あるいは最弱事前条件をもとにしたプログラム
の正当性の証明を講義することになった。教科書を探してみたが、構文と意味
の区別が明確でないもの、 wpの基本的な等式が公理なのか定理なのかわから
ないもの、取り扱うデータ(とくに配列)の定義が明確でないものなどばかり
で中々適当なものが見当たらない。while文の最弱事前条件の定義など、可算
個の引数をとる連言あるいは述語の帰納的定義なしには与えることができそう
にないが、そのようなことを明記した解説が見当たらず、読んで納得のできる
説明を見つけることができなかった。そこで、私が感じる問題点を解決するよ
うな体系を具体的に一つ、与えてみることにしたので報告する。以下のような
方針で体系を与えてみている。
  データは数(整数)か(多次元)配列;
  一階述語論理式を用い、可算連言を含む;
  構文的対象と意味的対象を明確に区別する;
  プログラムはダイクストラのコマンド;
  コマンドの意味を「状態」(変数への値の割当て、付値)の全体が作る集合
  Sの上の二項関係として与え、最弱事前条件はその二項関係の逆像がつくる
  Pow(S)上のendofunctionとして導く;
  最弱事前条件の等式(wp("x:= e", P) = P[x←e] など)は、コマンドの意味
  と述語の(Sの部分集合による)意味から証明できる定理として与える。

TSSS 2015-1

Date:      Feb 17 (Tue), 2015
Time:      11:00-12:00 (am)
Place:     SB911-1 (9th floor)  (筑波大学 総合研究棟B 911-1号室)
Speaker:   Adel Bouhoula (University of Carthage, Tunisia)
Title:     Proof by Induction and Computer Security Applications

Abstract:

Algebraic specifications provide a powerful method for the 
specification of abstract data types in programming languages 
and security software systems. Often, algebraic specifications 
are built with conditional equations. Semantically, the motivation 
for this is the existence of initial models; operationally, the 
motivation is the ability to use term rewriting techniques for 
computing and automatic prototyping. The formal development of a
system might give rise to many proof obligations. We must prove 
the completeness and the ground confluence of the specification 
and the validity of some inductive properties. 

In this talk, we will present procedures to test sufficient 
completeness and ground confluence and to prove or disprove 
inductive properties. Algebraic specifications and formal methods 
are also used to analyze and verify security protocols which allow 
agents to communicate securely over an insecure network. We will 
give some techniques both for the verification of security 
protocols and for identifying attacks on faulty protocols. In 
the last part of this talk, we will present an introduction to 
recent research studies regarding the detection and resolution 
of anomalies in security equipment configurations like in firewalls.

TSSS 2014-9

Date & Time: Dec 12 (Fri), 2014, 10:00-
Place:       SB1112 (11th floor)  (筑波大学 総合研究棟B 1112号室)
Speaker:     Jun Inoue
Title:       Staging で制御する Supercompilation

Supercompilation は強力なプログラム変換の枠組みで、融合変換や部分評価を
包含する事が知られている。Supercompilation は専ら全自動変換として研究さ
れてきたが、それではプログラムのどこがどの程度変換されるか予測する事が
難しい。そこでこの講演では、現在進めている staging で supercompilation
を表現しプログラマの制御下に置く研究を紹介する。

Supercompilation の特徴は、条件分岐の分岐先では条件式が真、という情報を
活用し、しかもその情報を条件式で直接言及されていない変数にまで伝播させ
る点にある。この研究ではそうした情報を staging の被生成変数
(future-stage variable) に付随するメタデータで表現し、破壊的に更新する
ことで同データの全複製に伝播させる手法で supercompilation を模倣した。
この成果は副作用つき staging の具体的で有用な使途を提供する他、部分評価
から生まれた staging が副作用によって部分評価を超えた表現力を持つという
点で理論的にも興味深い。

TSSS 2014-8

Date & Time: July 24 (Thu), 2014, 16:00- 
Place:       SB1001 (10th floor)  (筑波大学 総合研究棟B 1001号室)
Speaker:     Atsushi Igarashi (Kyoto University)
	     http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/
Title:       A Hoare Logic for SIMT Programs

Abstract: We study a Hoare Logic to reason about GPU kernels, which
are parallel programs executed on GPUs.  We consider the SIMT (Single
Instruction Multiple Threads) execution model, in which multiple
threads execute in lockstep (that is, execute the same instruction at
a time).  When control branches both branches are executed
sequentially but during the execution of each branch only those
threads that take it are enabled; after the control converges, all
threads are enabled and execute in lockstep again.  In this paper we
adapt Hoare Logic to the SIMT setting, by adding an extra component
representing the set of enabled threads to the usual Hoare triples.
It turns out that soundness and relative completeness do not hold for
all programs; a difficulty arises from the fact that one thread can
invalidate the loop termination condition of another thread through
shared memory.  We overcome this difficulty by identifying an
appropriate class of programs for which soundness and relative
completeness hold.  (Joint work with Kensuke Kojima)

TSSS 2014-7

Date & Time: July 17 (Thursday), 2014, 13:00- 
Place:       SB1112 (11th floor)  (筑波大学 総合研究棟B 1112号室)
Speaker:     Fadoua Ghourabi (Kwansei Gakuin University)
Title:       Formalizing the Qualitative Superposition of Rectangles 
	     in Isabelle/HOL

Abstract:
Qualitative spatial reasoning (QSR) provides methods to represent
spatial objects qualitatively. Being a subfield of artificial
intelligence, QSR approximates the human perception of the space,
namely where relation between spatial objects is a sufficient
information, and where computation is performed only when
necessary. The qualitative reasoning generally relies on
"pen-and-paper" proofs. Needless to say, a safer exploitation of a QSR
method requires a formal verification of its correctness. The purpose
of this research is to provide a full formalization of a practically
oriented QSR problem in a proof assistant.
 
We deal with the problem of arranging rectangles in the 2D plane. The
arrangement involves superposition under conditions of visibility. We
use relative directions to qualitatively represent the spatial objects
of interest, i.e. rectangles. We define properties to answer questions
about a superposition, for instance, whether it is successful or
whether the result is a valid rectangle. Checking these properties
formally is a challenge due to the number of the pairwise combinations
of rectangles. In an attempt to optimize the proofs, we group the
results of superposing the rectangles into equivalence classes. We
show that it is enough to check a property for a representative
element of an equivalence class.

TSSS 2014-6

Date & Time: June 20 (Friday), 2014, 15:30-
Place: SB1111 (11th floor), Tsukuba University
Speaker: LIU, Shuang (School of Computing, National University of Singapore)

Title: Towards direct model checking of UML state machines

UML diagrams are gaining increasing usage in Object-Oriented system
designs.  UML state machines are specifically used in modeling dynamic
behaviors of classes.  It has been widely agreed that verification of
system designs at an early stage will dramatically reduce the
development cost. Tool support for verification UML designs can also
encourage consistent usage of UML diagrams throughout the software
development procedure. In this work, we are motivated to provide
theoretical and practical support for model checking UML state
machines. We propose a formal operational semantics covering all
features of the latest version (2.4.1) of UML state machines
specification. The labeled transition system is adopted as the
semantic model, so as to use automatic verification techniques like
model checking. We implement our approach in a tool, named USMMC,
which turns model checking of UML state machines into practice. USMMC
is a self-contained toolkit, which provides editing, interactive
simulation as well as powerful model checking support for UML state
machines. The evaluation results show the effectiveness and
scalability of our tool.

Biodata: LIU Shuang is a PhD candidate in School of Computing,
National University of Singapore. Her research interest falls in
formal methods and software engineering, especially in the area of
integrating formal methods in requirement engineering and software
design phase. She is also interested in exploring various advanced
techniques, such as machine learning and natural language processing
techniques, to aid early defects detection in the software development
activities.

TSSS 2014-5


Date & Time: June 17 (Tuesday), 2014, 14:00- 
Place:       SB1111 (11th floor)  (筑波大学 総合研究棟B 1111号室)
Speaker:     Robert Glueck (DIKU, University of Copenhagen)
	     http://www.diku.dk/~glueck
Title:       Bootstrapping Compiler Generators from Partial Evaluators

Abstract:
Three-step bootstrapping of compiler generators from partial evaluators
(PE) is a viable alternative to the third Futamura projection. To
practically validate the theoretical insight, a novel PE-based compiler
generator was designed implemented for a recursive flowchart language.
This bootstrapping technique was found to produce the same compiler
generator that Gomard & Jones produced more that two decades ago by
self-application, but faster (on the same machine).
Compiler-generator bootstrapping has distinct properties that are not
present in the classic Futamura projections, such as the ability to turn
a PE into a compiler generator in one step without self-application.

Reference:

Glück R., Bootstrapping compiler generators from partial evaluators.
In Clarke E.M., et al. (eds.), Perspectives of System Informatics.
LNCS 7162, 2012. http://dx.doi.org/10.1007/978-3-642-29709-0_13

TSSS 2014-4

Date&Time:  2014年 5月 15日 (木) 15:30-
Place:      筑波大学 総合研究棟B 1001号室 (10階)
Speaker:    山形賴之(産総研)	

Title: ZIPC-to-PAT

Abstract:
キャッツ株式会社が開発しているソフトウェアモデリングツールZIPCに対して、
その記法をCSPに変換し、PATモデル検査器によりモデル検査するZIPC-to-PATに
ついて報告する。

TSSS 2014-3

Date&Time:  2014年 4月 11日 (金) 11:00-
Place:      筑波大学 総合研究棟B 1111号室 (11階)
Speaker:    Oleg Kiselyov 
p
Talk 1:
Extensible Effects: An Alternative to Monad Transformers
Oleg Kiselyov, Amr Sabry and Cameron Swords

We design and implement a Haskell library that solves the long-standing
problem of combining effects without imposing restrictions on their
interactions (such as static ordering). Effects arise from
interactions between a client and an effect handler (interpreter);
interactions may vary throughout the program and dynamically adapt to
execution conditions. Existing code that relies on monad transformers
may be used with our library with minor changes, gaining efficiency
over long monad stacks. In addition, our library has greater
expressiveness, allowing for practical idioms that are inefficient,
cumbersome, or outright impossible without a global re-write 
with monad transformers.

Our alternative to a monad transformer stack is a single monad, for
the coroutine-like communication of a client with its handler. Its
type reflects possible requests, i.e., possible effects of a
computation. To support arbitrary effects and their combinations,
requests are values of an extensible union type, which allows adding
and, notably, subtracting summands.  Extending and, upon handling,
shrinking of the union of possible requests is reflected in its type,
yielding a type-and-effect system for Haskell. The library is
lightweight, generalizing the extensible exception handling to other
effects and accurately tracking them in types.

The talk will use Haskell to motivate and illustrate extensible
effects, which however are not limited to Haskell.

TSSS 2014-2


Date&Time:  2014年 3月 14日 (金) 14:00-
Place:      筑波大学 総合研究棟B 1001号室 (10階)
Speaker:    Oleg Kiselyov 

Title:	    Code generation with effects and hygiene

Abstract:

The appeal of generative programming is ``abstraction without guilt'':
eliminating the vexing trade-off between writing high-level code and
highly-performant code. Generative programming also promises to
formally capture the domain-specific knowledge and heuristics used by
high-performance computing (HPC) experts. Effects are indispensable in
code generators, to report failures, to generate alternatives to
choose the fastest from, to introduce auxiliary variables, to
interchange loops, etc.  Extensive painful experience shows that
unrestricted effects interact with generated binders in undesirable
ways to produce unexpectedly unbound variables, or worse, unexpectedly
bound ones.  These subtleties hinder domain experts in using and
extending the generator.  A pressing problem is thus to express the
desired effects while regulating them so that the generated code is
correct, or at least correctly scoped, by construction.

Assuredly maintaining hygiene while reshuffling open code is not only
important practically but is interesting theoretically.  We present
two ways to solve the problem, from different angles. Both solutions
permit arbitrary effects, including mutable references and delimited
control, that move open code across generated binders. Both statically
guarantee that the generated code is well-typed and well-scoped.

On one hand, we generate code with quasi-quotation and ensure hygiene
at the generation time. Attempting to build code values with unbound
or mistakenly bound variables raises an exception with good
diagnostics. This approach requires no fancy types and has been
implemented in BER MetaOCaml (a superset of OCaml with data types and
operations for constructing and executing typed code values).

Fancier types (mainly, first-class polymorphism) on the other hand can
ensure hygiene even before the generator is run: a well-typed
generator, when run, will never even attempt to build ill-scoped code.
More insightfully, static types of generator expressions indicate the
lexical scopes of generated binders, hence preventing mixing up
variables with different scopes. We demonstrate this approach on a
Haskell code-combinator library, which may be regarded as a `staged
Haskell.'

TSSS 2014-1

Date&Time:  2014年 2月 14日 (金) 14:00-
Place:      筑波大学 総合研究棟B 1111号室 (11階)
Speaker:    佐藤 雅彦 (京都大学名誉教授)

Title:      A Name-Free Lambda Calculus

Abstract:
This talk introduces a name-free lambda calculus. In contrast to the fact 
that the traditional lambda calculus is defined as a calculus on open-terms 
containing free variables, the name-free lambda calculus presented here is 
a calculus on closed-terms. The definition of such a calculus is made 
possible by inductively defining the set of closed lambda terms without
using variables.  The advantage of the calculus over the name-carrying 
lambda calculus is that metatheorems about the calculus can be shown 
without using the notion of a variable and hence also without notions of 
alpha-equivalence, substitution and fresh names. It is shown that 
metatheorems can be proved more naturally in this name-free calculus than 
in the name-carrying calculus.

TSSS 2013-6

Date&Time:  2013年 11月6日 (水) 16:00-
Place:      筑波大学 総合研究棟B 1001号室 (10階)
Speaker:    片山 晋 (宮崎大学)
	    http://nautilus.cs.miyazaki-u.ac.jp/~skata/

Title:
MagicHaskeller on the Web: サービスとしての自動プログラミング

Abstract:
ウェブベースの自動プログラミングツールである,MagicHaskeller on the Web
の紹介を行う.本ツールは,手軽さ,使いやすさに重点を置いたものであり,
ウェブ検索エンジンを使うのと同様の感覚で短いプログラムを生成することが
できる.この講演では,MagicHaskeller on the Webの使用方法について紹介
した後,実装方法について説明し,また,Microsoft Excel 2013の同様の機能
であるFlash Fillとの比較検討を行う.

TSSS 2013-5

Date&Time:  8月7日 (水) 15:30-
Place:   筑波大学 総合研究棟B 1001号室
Speaker: Jacques Garrigue(名古屋大学)

Title: Ambivalent Types for Principal Type Inference with GADTs
       (Joint work with Didier Remy)

Abstract:
GADTs, short for Generalized Algebraic DataTypes, which allow
restricting type parameters for specific constructors, have many
useful applications.  However, pattern matching on GADTs
introduces local type equality assumptions, which are a source of
ambiguities that may destroy principal types, and must be resolved by type
annotations.

We introduce "ambivalent types" to tighten the definition of ambiguities
and better confine them, so that type inference has principal types,
remains monotonic, and requires fewer type annotations.

TSSS 2013-4

Date&Time:  July 25 (Thu) 16:00-
Place:   筑波大学 総合研究棟B 1001号室
Speaker: 西澤弘毅(神奈川大学 工学部 情報システム創成学科)

Title: クオンテイルと完備べき等左半環の表現定理
Abstract:
完備束に分配するモノイド構造が入った代数構造はクオンテイルと呼ばれ、
その典型例として、固定された集合上の二項関係全体が知られている。また、
クオンテイルの分配束を片側だけ弱めた代数構造が完備べき等左半環と呼ば
れ、その典型例として、固定された集合上の上に閉じた多重関係全体が知ら
れている。この講演では、クオンテイルの関係表現定理に関するいくつかの
結果と、完備べき等左半環の多重関係表現定理に関するいくつかの結果につ
いてまとめる。 
なお、この研究は鹿児島大学の古澤仁氏との共同研究である。

TSSS 2013-3

Date:    June 27 (Thu) 15:30-
Place:   Room 1001 (10th floor), Lab. of Adv. Res.-B bldg. ("Sogo-kenkyu-tou" B)
Speaker: Aart Middeldorp (University of Innsbruck)

Title:

 Beyond Peano Arithmetic - Automatically Proving Termination of the
 Goodstein Sequence

Abstract:

 Kirby and Paris (1982) proved in a celebrated paper that a theorem
 of Goodstein (1944) cannot be established in Peano (1889) arithmetic.
 We present an encoding of Goodstein's theorem as a termination
 problem of a finite rewrite system. Using a novel implementation of
 ordinal interpretations, we are able to automatically prove termination
 of this system, resulting in the first automatic termination proof for
 a system whose derivational complexity is not multiply recursive. The
 talk is based on joint work with Sarah Winkler and Harald Zankl.

TSSS 2013-2

Date&Time: May 16(Thu), 17:00-
Place: 第12会議室(本部・情報棟6階), 産総研つくば中央

Speaker: 平井洋一(産総研)
Title: 並列データ構造の検証、次の一手

Abstract:
並列索引構造の検証をしたい。ファイルシステムやデータベースの索引に
使われていて重要である。スタックやキューの並列版の検証は自動化
できて性能を競っているのに、索引構造の並列版の検証は手動でさえ十
分でない(たとえばlinearizabilityを形式手法で示せていない)。ところで
実は、大勢が検証しようとしている並列索引構造もそうでない並列索引
構造もある。特に応用範囲が広いのに研究されていない並列索引構造
を紹介する。

TSSS 2013-1

Date&Time: Feb. 25(Mon), 15:30-
Place: Room SB-1001 (総合研究棟B, 10階), 筑波大学

Speaker: 塚田武志(東北大学大学院情報科学研究科)

Title: 2レベルゲームによる共通型の意味論

Summary: 
木 T と木オートマトン A が与えられたとき,T が A に受理されるか否
かを争う,証明者と反証者の間のゲーム G を考えることができる.ゲー
ム G のルールは木 T の構造にしたがって定義され,この意味でゲーム
G は木 T の構造の上のゲームであると言うことができる.

これを一般化のひとつが,本発表で述べる2レベルゲームである.2レベ
ルゲームは(単純型付きの)Boehm木の構造の上のゲームである.すなわ
ち,与えられたBoehm木 M が与えられた性質 P を満たすかを争う,
Boehm木 M の構造にしたがって定義されるゲームである.

本発表では,2レベルゲームのアイデアと基本的な性質をみたのち,2レ
ベルゲームが共通型システムと呼ばれる型システムの完全かつ健全な意味
論を与えることをみる.また,2レベルゲームのプログラム検証への応用
に関する展望を述べる.

TSSS 2012-11

Date&Time: Dec. 20(Thu), 15:30-
Place: Room SB-1001 (総合研究棟B, 10階), 筑波大学

Speaker: Reynald Affeldt (産業技術総合研究所)

Title: Formal Verification of Shannon's Theorems
       (joint work with Manabu Hagiwara and Jonas Senizergues)

Summary: The most fundamental results of information theory are Shannon's
theorems. These theorems express the bounds for reliable data
compression and transmission over a noisy channel. Their proofs are
non-trivial but rarely detailed, even in the introductory literature.
This lack of formal foundations is all the more unfortunate that
crucial results in computer security rely solely on information theory
(the so-called ``unconditional security''). In this presentation, we
report on the formalization of a library for information theory in the
SSReflect extension of the Coq proof-assistant. In particular, we
produce the first formal proofs of the source coding theorem (that
introduces the entropy as the bound for lossless compression), and of
the channel coding theorem (that introduces the capacity as the bound
for reliable communication over a noisy channel).

TSSS 2012-10.5

Date & Time: Dec. 10 (Mon), 10:30 - 12:00
Place: Room SB-1112 (筑波大学 総合研究棟B 11階)

Speaker: Oleg Kiselyov (http://okmij.org/)

Title: Iteratees

Abstract:
  Iteratee IO is a style of incremental input processing with precise
  resource control. The style encourages building input processors from
  a user-extensible set of primitives by chaining, layering, pairing and
  other modes of compositions. The programmer is still able, where
  needed, to precisely control look-ahead, the allocation of buffers,
  file descriptors and other resources. The style is especially suitable
  for processing of communication streams, large amount of data, and
  data undergone several levels of encoding such as pickling,
  compression, chunking, framing.  It has been used for programming
  high-performance (HTTP) servers and web frameworks, in computational
  linguistics and financial trading.
  
   The talk will introduce programming with Iteratees in Haskell,
  contrasting them with |stdio|-like IO and Lazy IO and relating to
  online parser combinators. The talk will stress principles and
  characteristic examples common to all iteratee libraries across
  several languages.

TSSS 2012-10

Date&Time: Nov. 9(Fri), 15:00-16:00
Place: Room SB-1001 (Sogo-Kenkyuto-B, 10th Floor), University of Tsukuba

Speaker: Walid Taha (Halmstad University, Sweden)

Title: Staging, 15 years later

Abstract: 
Multi-stage Programming with Explicit annotations, or staging for
short, gives the programmer control over program evaluation order. It
enables rapid development of program generators and domain-specific
languages. Staging was introduced in 1997 in a paper by Tim Sheard, my PhD
advisor, and myself. Significant activity by numerous researches followed.
This talk reviews the key concepts and developments in the area of staging,
and suggests some promising directions for future work.

TSSS 2012-9

Date&Time: Oct. 22(Mon), 15:30-
Place: Room SB-1111 (Sogo-Kenkyuto-B, 10th Floor), University of Tsukuba

Speaker: 寺内 多智弘(名古屋大学)

Title: A Template-based Approach to Complete Predicate Refinement

Abstract:
SLAM, BLASTなどに代表されるソフトウェアモデル検査器が抱える課題の一つに、
抽象の詳細化(abstraction refinement)がある。モデル検査器の性能は
refinementのやり方に大きく依存し、refinementを誤ると停止性が損なわれる
こともある。この問題に対し、Jhala & McMillanはTACAS 2006の論文で「完全
なrefinement」の手法を提案した。この手法は、(predicate abstractionにお
いて)refinementを無限に間違え続けるということを防ぎ、モデル検査器の停止
性を保証することができる。具体的には、Jhala & McMillanは、限量子なしの
difference constraintとuninterpreted functionの一階述語論理の理論で有効
な手法を示した。しかし、これは非常に限られた理論であり、多くのモデル検
査器で用いられる線形演算の理論などに対応していない。今回は、線形演算や
配列など、より広い理論に対して有効な、完全なrefinementの手法を提案する。

TSSS 2012-8

Date&Time: Oct. 4 (Thu), 14:00-
Place: Room SB-1001 (Sogo-Kenkyuto-B, 10th Floor), University of Tsukuba

Speaker: Daan Leijen (Microsoft Research in Redmond)

Title: Koka: a function-oriented language with safe side-effects

Abstract: 
Koka is a new function-oriented language with strong static type
inference. A novel feature is the (side) effect inference
where every function shows the potential side-effects in its type. 
The Koka language essentially takes the strict evaluation 
from ML and combines it with monadic side effects from Haskell. 
In this talk, I will show how effect inference can be made to 
work in a polymorphic and higher-order setting. As a 
demonstration of its use, I will also show a safe tier-splitted 
program, where a single program has code that runs on both 
the server and client (using NodeJS and a Browser), but through 
the effect system we can guarantee that there is no 
unsafe sharing between client and server code.
See also http://www.rise4fun.com/koka/tutorial for more information.

Bio: 
Daan Leijen is a researcher at Microsoft Research in Redmond, 
WA, where he specializes in language design. In particular, he 
enjoys working on functional languages like Haskell and OCaml, 
and studied various type inference systems.
He was also the implementor of the Parsec parser library, and 
the Parallel extensions to .NET (Task library) that ships with Windows.

TSSS 2012-7

Date&Time: 9月21日 (金), 15:30-
Place: Room SB-1001 (Sogo-Kenkyuto-B, 10th Floor)
Speaker: Yasuhiko Minamide (University of Tsukuba) Title: Reachability Analysis of the HTML5 Parser Specification and its Application to Compatibility Testing Abstract: A draft standard for HTML, HTML5, includes the detailed specification of the parsing algorithm for HTML5 documents, including error handling. In this paper, we develop a reachability analyzer for the parsing specification of HTML5 and automatically generate HTML documents to test compatibilities of Web browsers. The set of HTML documents are extracted using our reachability analysis of the statements in the specification. This analysis is based on a translation of the specification to a conditional pushdown system and on a new algorithm for the reachability analysis of conditional pushdown systems. In our preliminary experiments, we generated 353 HTML documents automatically from a subset of the specification and found several compatibility problems by supplying them to Web browsers. This is joint work with Shunsuke Mori.

TSSS 2012-6

Date&Time: 7月26日 (木), 16:00-
Place: Room SB-1014 (Sogo-Kenkyuto-B, 10th Floor)

Speaker: Hiroshi Unno (University of Tsukuba)

Title:
MoCHi: Software Model Checker for a Higher-Order Functional Language

Abstract:
We will demonstrate MoCHi, a fully-automated program verification tool
(so called a "software model checker") for a subset of OCaml,
supporting integers, recursive data types (such as lists), exceptions,
higher-order functions and recursion. MoCHi is based on higher-order
model checking, and consists of three layers. The top layer transforms
a source program into an intermediate program of a core language,
which is a simply-typed call-by-value higher-order functional language
with recursion, booleans and integers (a la "PCF"). The transformation
is carried out by encoding exceptions and recursive data types using
higher-order functions. The middle layer further transforms the
intermediate program into a higher-order boolean functional program (a
la "finitary PCF"), by using predicate abstraction and
counter-example-guided abstraction refinement (CEGAR). Finally, on the
bottom layer, the higher-order boolean functional program is verified
by using a higher-order model checker TRecS. In this talk, we
use MoCHi to verify several sample programs, and explain how it works
internally. We will also discuss the current limitations and
ongoing/future work.
(Joint work with Ryosuke Sato and Naoki Kobayashi)

TSSS 2012-5

Date&Time: April 17 (Tue), 16:00-17:00
Place: Room SB-1111 (Sogo-Kenkyuto-B, 11th Floor)

Speaker: Yutaka Oiwa (AIST)

Title:
Fail-Safe C: a memory-safe ANSI-C compiler to make existing programs safe

Abstract:
Fail-Safe C は、完全なメモリ安全性を保証する ANSI-C (C90) 互換言語処理系です。 このコンパイラは規格で認められた自由なポインタ演算やキャスト操作にも 完全に対応し、既存のC言語プログラムにほとんど手を加えずに、 バッファ溢れや dangling pointer などによるメモリ破壊を防止し、 コンピュータウィルスなどの不正コードのメモリへの侵入を完全に抑止することができます。 ANSI-C との高い互換性により、メールサーバやDNSサーバなどいろいろな既存の さまざまなプログラムを最小限の変更で動作させることもできます。 今回の講演では、Fail-Safe Cによるメモリ安全性の保証手法のほか、 実用プログラムを動作させるための周辺環境やライブラリ整備についても お話しします。 Fail-Safe C is a completely memory-safe, completely ANSI-compatible C language (C90) compiler. It supports all C90 semantics including pointer arithmetics and pointer casts. By using this compiler, we can prevent all kinds of memory data corruptions caused by buffer overrun, dangling pointers etc., and thus prevent intrusion of malicious codes (such as computer viruses) into the program memory, with no or little modification of existing code bases. The high compatibility to the ANSI-C specification allows execution of various existing production-level programs such as mail and DNS servers. In the talk I will explain our effort for accepting existing huge programs, as well as the core methodology of the Fail-Safe C compiler.

TSSS 2012-4

Date&Time: April 11 (Wed), 15:00-17:00
Place: Room SB-1111 (Sogo-Kenkyuto-B, 11th Floor)

Speaker: Chung-chieh Shan (University of Tsukuba)
Title: Entailment above the word level in distributional semantics (joint work with Marco Baroni, Raffaella Bernardi, Ngoc-Quynh Do)

Abstract:
Distributional semantics (DS) and formal semantics (FS) are two ways to study natural-language meaning, whose strengths today are complementary. On one hand, DS represents meaning as vectors that summarize the contexts where expressions occur. This approach has successfully extracted semantic relations among words from large corpora. On the other hand, FS represents meaning as formulas and assembles them by composition rules. This approach has successfully modeled quantification and captured inference among phrases and sentences. We bring DS and FS closer by introducing two ways to detect entailment among phrases using their DS representations. Our first experiment shows that the entailment relation between adjective-noun constructions and their nouns (big cat |= cat), once represented as vector pairs, generalizes to entailment among nouns (dog |= animal). Our second experiment shows that entailment among quantifier phrases (many dogs |= some dogs) similarly generalizes to unseen quantifiers (all cats |= several cats). Moreover, the entailment relations in our two experiments appear to tap into different vector properties, as predicted by FS because nouns and quantifiers phrases have different types.

TSSS 2012-3

Date&Time: March 5 (Mon), 11:00-12:00
Place: Room SB-1111 (Sogo-Kenkyuto-B, 11th Floor)

Speaker: Sebastian Fischer(Christian-Albrechts-University of Kiel, Germany)
Title: Lazy Functional Logic Programming and Encapsulated Search

Abstract:
Functional Logic Programming (FLP) combines features from functional programming such as first-class functions and algebraic datatypes with features from logic programming such as unbound logic variables and nondeterministic search. I will introduce lazy (call-by-need) FLP using the Curry language and review different ways to encapsulate search, that is, to access different results of nondeterministic computations deterministically. The interaction of laziness and encapsulated search is an old problem with some new solutions in the FLP community. By talking about both the problem and some existing solutions, I hope to motivate discussion on the topic from the perspective of control operators in the presence of call-by-need.


TSSS 2012-2

Date: 15:00-16:00, Feb. 15 (Wed), 2012
Place: Room SB-1001 (Sogo-Kenkyuto-B, 10th Floor)

Speaker: Chung-chieh (Ken) Shan
Title: Embedding probabilistic languages

Abstract:
Probabilistic inference is popular in machine learning for writing
programs that classify music and locate planes. It is also useful in
cognitive science for modeling how people interpret words and recognize
faces. However, it is applied much less than it could be because
most inference programs are written from scratch by hand. Instead,
probabilistic models and inference procedures should be written as
separate reusable modules. To this end, we carried out and popularized
a new approach that is easier to use and more expressive, namely to
write models and inference in the same general-purpose language. Our
approach makes deterministic parts of models run at full speed and
lets inference procedures reason about themselves without interpretive
overhead. I will describe our approach and how we apply the same
inference implementations to multiple realistic models, with performance
competitive with the state of the art. This work exemplifies a
recurring theme: we can apply tools from programming-language theory,
such as continuations and staging, to represent declarative knowledge as
executable code instead of passive data.

Dr. Chung-chieh Shan's web page is
http://www.cs.ruters.edu/~ccshan/

TSSS 2012-1

Date & Time: February 7, 2012, 11:00 - 12:00
Venue : SB 110, University of Tsukuba

Speaker: Olga Caprotti
Department of Computer Science and Engineering,
Chalmers University of Technology and University of Gothenburg, Sweden

Title: MOLTO, Multilingual Online Translation

Abstract MOLTO's goal is to develop a set of tools for translating
texts between multiple languages in real time with high
quality. Languages are separate modules in the tool and can be varied;
prototypes covering a majority of the EU's 23 official languages will
be built. As its main technique, MOLTO uses domain-specific semantic
grammars and ontology-based interlinguas. These components are
implemented in GF (Grammatical Framework), which is a grammar
formalism where multiple languages are related by a common abstract
syntax. GF has been applied in several small-to-medium size domains,
typically targeting up to ten languages but MOLTO will scale this up
in terms of productivity and applicability.

A part of the scale-up is to increase the size of domains and the
number of languages. A more substantial part is to make the technology
accessible for domain experts without GF expertise and minimize the
effort needed for building a translator. Ideally, this can be done by
just extending a lexicon and writing a set of example sentences.

The most research-intensive parts of MOLTO are the two-way
interoperability between ontology standards (OWL) and GF grammars, and
the extension of rule-based translation by statistical methods. The
OWL-GF interoperability will enable multilingual
natural-language-based interaction with machine-readable
knowledge. The statistical methods will add robustness to the system
when desired. New methods will be developed for combining GF grammars
with statistical translation, to the benefit of both.

MOLTO technology will be released as open-source libraries which can
be plugged in to standard translation tools and web pages and thereby
fit into standard workflows. It will be demonstrated in web-based
demos and applied in three case studies: mathematical exercises in 15
languages, patent data in at least 3 languages, and museum object
descriptions in 15 languages.

TSSS 2011-3

Date: 16:00-17:00, Jan 12, 2012

Place: Room SB-1111

Speaker: Jun Inoue (Department of Computer Science, Rice University)

Title: Reasoning About Multi-stage Programs

Abstract:

Multi-stage プログラミング (MSP) は、プログラムの生成・合成・実行を指
示する為の特殊な注釈を用いて、プログラムを生成するプログラムを書く手
法である。MSP は専ら汎用性を犠牲にせずに実行効率が高いプログラムを書
くために効果的な手法として研究されてきた。しかし、従来そうし
た multi-stage プログラムの正しさを如何に証明するかという研究は乏しく、
そうした証明でとりうるアプローチも、multi-stage 特有の障碍が存在する
かもよく知られていなかった。本研究ではこの点を改善するた
め、multi-stage プログラムの検証に役立つような multi-stage λ算法の性
質とそれらを活用する証明技法を確立し、また証明の際に注意すべき MSP 言
語の特質を取りまとめた。

特に、本研究では multi-stage プログラムの検証に必然的な次の三つの疑問
点を解決した。第一に、プログラム言語に MSP の注釈機構を導入することで、
導入前の言語では等価であった式同士が等価でなくなる事はあるか。残念な
がら等価性が破壊される場合は存在し、一般に自由変数を含む項の扱いが導
入前とは異なってしまう。第二に、MSP の注釈は「注釈」の名の示す通りプ
ログラムの意味をほぼ変えないものと期待されて使われるが、それが厳密に
保証されるのはどのような場合か。本研究では、プログラムが一定の停止条
件を満たせば十分であることを示した。第三に、multi-stage プログラムに
外延的な論証 (∀x. f(x) = g(x) なら f = g など) を適用して良いか。本
研究では applicative bisimulation と呼ばれる双模倣を MSP 用に適応させ
ることで外延性のみならず、理論上は成立する全ての等式を証明できる、健
全で完全な証明手段を確立した。これらの成果を通じて深まった MSP の理解
により、複雑なプログラムの検証も可能になった。

TSSS 2011-2

Date: 14:00-16:00, Dec 15, 2011

Place: Room SB-1112

1. Kohei Suenaga (Kyoto University, JSPS Research Fellow (PD))
Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
(Joint work with Ichiro Hasuo)
2. Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
(Joint work with Tarmo Uustalu.)

Abstracts:

1. Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling

We add, to the common combination of a WHILE-language and a
Hoare-style program logic, a constant dt that represents an
infinitesimal (i.e. infinitely small) value.
The outcome is a framework for modeling and verification
of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics
and getting them right is a pressing challenge. We rigorously define
the semantics
of programs in the language of nonstandard analysis, on the basis of which the
program logic is shown to be sound and relatively complete.

2. Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While

In search for a foundational framework for reasoning about observable
behavior of programs that may not terminate, we have previously
devised a coinductive operational semantics for While. The
operational semantics keeps track of all the states that an execution
goes through as a trace (a possibly infinite sequence of states). The
trace is finite for a terminating execution and infinite for a
non-terminating execution. Subsequently we designed a Hoare logic
counterpart of our coinductive trace-based semantics and proved it
sound and complete. Our logic subsumes both the partial
correctness Hoare logic and the total correctness Hoare logic: they
are embeddible.

All the results have been formalized in Coq constructively.

In this talk, I will overview the coinductive operational semantics
and the Hoare logic, aiming at delivering the intuition behind.

(Joint work with Tarmo Uustalu.)

TSSS 2011-1

Date: 14:00-15:00, Mar 14, 2011

Place: Room SB-1001

Speaker: Marcin Paprzycki, Systems Research Institute of the Polish Academy of Sciences

Title: Introduction to Software Agents and their Applications

Abstract:

Since 1994 we are told that software agents will become the next revolution
in computing [3]. This change is to occur not only in the ways we construct
software [2] but also to profoundly impact human-computer interactions [1,
3]. Unfortunately, when we turn the computer on in the morning, we do not
contact our Personal Agent to receive a personalized newscast, our day-plan
and, on the basis of that plan as well as the weather forecast and knowledge
of our dressing-preferences, an advice what to wear. Similarly, when
creating software for an e-shop we do not utilize pre-existing agent-modules
(e.g. advertising agents, seller, inventory manager, etc.). Instead, there
exist only few successful large-scale implementations of agent systems.

In the seminar, a general introduction to software agents will be presented.
Discussion includes topics like: conceptual roots and definition of software
agents and agent systems, major points raised “for” and “against” software
agent systems, existing applications of agent systems, and possibility of
developing large scale agent systems. No previous exposure to software
agents and agent systems is assumed.

*References*

1. J. Hendler, Is There an Intelligent Agent in Your Future?, Nature, 11,March, 1999

2. N. R. Jennings, An agent-based approach for building complex software systems,
CACM, 44 (4), 2001, 35-41

3. P. Maes, Agents that Reduce Work and Information Overload, Communications of the ACM, 37(7),
1994, 31-40

TSSS 2010-5

Date: September 17, 2010

Place: Room SB-1001

Program:

13:00 - 14:00
Verifying floating-point algorithms using formalized mathematics
John Harrison (Intel Corporation, USA)
Abstract

14:15 - 14:45
Translating Regular Expression Matching into Transducers
Yasuhiko Minamide (University of Tsukuba)
(joint work with Yuto Sakuma and Andrei Voronkov)

14:45- 15:15
General bindings in Nominal Isabelle
Cezary Kaliszyk (University of Tsukuba)

15:15 - 15:45
Proof certificate for origami theorem proving
Tetsuo Ida (University of Tsukuba)

16:00 - 16:30
Modules for Origami Constructions
Fadoua Ghourabi (University of Tsukuba)

16:30 - 17:00
Web Origami System: WebEos
Asem Kasem (University of Tsukuba)

TSSS 2010-4

Date: 10:00-11:30, Sep 2, 2010

Place: Room SB-1001

Speaker: Cezary Kaliszyk, University of Tsukuba

Title: Computer Algebra and Proof Assistants

Abstract:

Computer algebra systems are programs that allow manipulation
and processing of mathematical expressions. However, the algorithms
provided are not formally verified, which makes computer
algebra systems less reliable than proof assistants.

In this talk we present an approach which bridges the gap
between the two classes of systems. We show a computer
algebra system that ensures absolute correctness of performed
simplifications by using the decision procedures present in
a proof assistant. We show how the system can be extended with
an approach for treating partiality and effective computation with
real numbers.

TSSS 2010-3

Workshop on Symbolic Computation and Software Verification
Date: Apr 8-9, 2010
Link

TSSS 2010-2

Date: 15:00-17:00, Mar 26, 2010

Place: Room SB-1001
Date: 15:00-17:00, Mar 24, 2010

Place: Room SB-1112

Speaker: Andreiv Voronkov, University of Manchester
Title: Tutorial on on satisfiability and theories/SMT

TSSS 2010-1

Date: 11:00-, Mar 11, 2010

Place: Room SB-1001

Speaker: Keiko Nakata, Institute of Cybernetics, Tallinn University of Technology

Title: Lazy modules

Abstract:

The ML module system is well-known for
its support for modular programming. Motivated by practical
experiences with lazy initialization of modules and the desire to
extend ML modules with recursion, we investigate hybrid evaluation
strategies between call-by-value and call-by-need for ML-style modules
supporting recursion. More precisely we propose and examine five
evaluation strategies: a call-by-value strategy and four call-by-need
strategies with different degrees of laziness. We formalize the
strategies by translating a source syntax for modules into target
languages, which are very much inspired by Felleisen and Hieb's
call-by-value lambda calculus with state and Ariola and Felleisen's
call-by-need cyclic lambda calculus. Different strategies are
expressed by tweaking the translation as well as the operational
semantics of the target languages. We look at the strategies through a
series of examples and state inclusion between the strategies.

TSSS 2009-4

日時:  15:00-, Aug 18, 2009

場所: Room SB-1014

講演者: 小林直樹(東北大学)

講演タイトル:型と高階再帰スキームに基づくプログラム検証

要旨:
本講演では、高階再帰スキームを用いた新しいプログラム検証手法を紹介する。
この手法は、高階関数と再帰を含むプログラムの(エラー状態などへの)到達
可能性などの性質を健全かつ完全に判定することができるという点で、これま
でに類をみないものであり、今後、MLなどの高レベルプログラミング言語用の
ソフトウェアモデル検査器の実現につながるものと期待できる。

高階再帰スキームは無限木を生成するための文法であり、ワード言語を考えた
場合には正規言語や文脈自由言語のクラスを真に包含する強力な体系でありな
がら、生成される木が様相μ計算で表現される任意の性質を満たすかどうかを
モデル検査する問題が決定可能であることが2006年にOngによって証明されて
いる。

講演ではまず、高階関数型言語のプログラムの検証問題の多くを、上記の高
階再帰スキームのモデル検査の問題に還元できることを示す[1]。これにより、
再帰を含む単純型付きλ計算で記述されたプログラムの制御フロー解析、到達
可能性問題、資源使用法検証問題などがすべて決定可能であることが導かれる。

次に、高階再帰スキームのモデル検査問題がインターセクション型システムに
おける型判定の問題に還元できることを示し[1,2]、それに基づいたモデル検
査アルゴリズムを提案する[3]。本モデル検査アルゴリズムを実装したモデル
検査器TRecSを用いた実験の結果、高階再帰スキームのモデル検査問題の最悪
計算量はn-EXPTIME 完全であるにもかかわらず、典型的なプログラムから得ら
れる再帰スキームのモデル検査問題の多くを高速に判定できることがわかった。

本講演内容の一部は、オックスフォード大学のLuke Ong教授との共同研究の結
果である。

参考文献:
[1] Naoki Kobayashi,
Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs,
POPL 2009, pp.416-428, 2009

[2] Naoki Kobayashi and Luke Ong,
A Type System Equivalent to Modal Mu-Calculus Model Checking of Recursion Schemes,
LICS 2009.

[3] Naoki Kobayashi,
Model-Checking Higher-Order Functions,
PPDP 2009.

TSSS 2009-3

Date: 11:00-12:00, Aug 7, 2009

Place: Room SB-1001

Speaker: Franz Winkler, RISC, Johannes Kepler University, Linz, Austria

Title: From Gauss to Groebner and Beyond

Abstract:
Many algorithmic methods in mathematics can be seen
as constructing canonical systems for deciding membership problems.
Important examples are Gauss' elimination method for linear systems,
Euclid's algorithm for computing greatest common divisors,
Buchberger's algorithm for constructing Gr\"obner bases, or
the Knuth-Bendix procedure for equational theories.
We explain the basic concept of canonical systems and investigate
the close connections between these algorithms.

TSSS 2009-2

Date: 10:30-11:30, Jun 19, 2009

Place: Room SB 911-1

Speaker: Prof. Dr. Helmut Schwichtenberg, Ludwig-Maximilians-Universität, München

Title: Program extraction in constructive analysis

Abstract:
We sketch a development of constructive analysis in Bishop's style,
with special emphasis on low type-level witnesses (using
separability of the reals). The goal is to set up things in such a
way that realistically executable programs can be extracted from
proofs. This is carried out for (i) the Intermediate Value Theorem
and (ii) the existence of a continuous inverse to a monotonically
increasing continuous function. Using the Minlog proof assistant,
the proofs leading to the Intermediate Value Theorem are formalized
and realizing terms extracted. It turns out that evaluating these
terms is a reasonably fast algorithm to compute, say, approximations
of the square root of 2.

TSSS 2009-1

Date: 3:30 - 15:00, May 1, 2009

Place: SB-1001

Speaker: Dr. Simon Kramer, University of Tsukuba

Title: A General Definition of Malware (joint work with Julian C. Bradfield, U Edinburgh)

Abstract:
We propose a general, formal definition of malware in the language of modal logic. Our definition is
general thanks to its abstract formulation, which, being abstract, is independent of --- but nonetheless
generally applicable to --- the manifold concrete manifestations of malware. From our formulation of
malware, we derive equally general and formal definitions of benware (not malware), anti-malware
(``antibodies'' against malware), and medware (``medicine'' for affected software). We obtain
theoretical tools and practical techniques for the detection, comparison, and classification of malware
and its derivatives. Our general defining principle is causation of (in)correctness.