Date&Time: May 16(Thu), 17:00- Place: 第１２会議室(本部・情報棟6階), 産総研つくば中央 Speaker: 平井洋一(産総研) Title: 並列データ構造の検証、次の一手 Abstract: 並列索引構造の検証をしたい。ファイルシステムやデータベースの索引に 使われていて重要である。スタックやキューの並列版の検証は自動化 できて性能を競っているのに、索引構造の並列版の検証は手動でさえ十 分でない(たとえばlinearizabilityを形式手法で示せていない)。ところで 実は、大勢が検証しようとしている並列索引構造もそうでない並列索引 構造もある。特に応用範囲が広いのに研究されていない並列索引構造 を紹介する。
Date&Time: Feb. 25(Mon), 15:30- Place: Room SB-1001 (総合研究棟B, 10階), 筑波大学 Speaker: 塚田武志（東北大学大学院情報科学研究科） Title: ２レベルゲームによる共通型の意味論 Summary: 木 T と木オートマトン A が与えられたとき，T が A に受理されるか否 かを争う，証明者と反証者の間のゲーム G を考えることができる．ゲー ム G のルールは木 T の構造にしたがって定義され，この意味でゲーム G は木 T の構造の上のゲームであると言うことができる． これを一般化のひとつが，本発表で述べる２レベルゲームである．２レベ ルゲームは（単純型付きの）Boehm木の構造の上のゲームである．すなわ ち，与えられたBoehm木 M が与えられた性質 P を満たすかを争う， Boehm木 M の構造にしたがって定義されるゲームである． 本発表では，２レベルゲームのアイデアと基本的な性質をみたのち，２レ ベルゲームが共通型システムと呼ばれる型システムの完全かつ健全な意味 論を与えることをみる．また，２レベルゲームのプログラム検証への応用 に関する展望を述べる．
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).
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.
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.
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の手法を提案する。
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.
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.
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)
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.
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.
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.
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/
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.
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 の理解
により、複雑なプログラムの検証も可能になった。
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.)
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
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)
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.
Workshop on Symbolic Computation and Software Verification
Date: Apr 8-9, 2010
Link
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
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.
日時: 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.
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.
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.
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.