第1回 CSPSAT講演会

最終更新日:2010年2月

開催情報

日時:2010年2月4日(木) 15:00 〜
用務先:神戸大学 自然科学総合研究棟3号館(東) 4F
新井プロジェクト プレゼンテーション室(421号室) (アクセス方法)
用務地:〒657-8501 兵庫県神戸市灘区六甲台町1-1
最寄り駅:(JR東海道・山陽本線)六甲道 or (阪急神戸本線)六甲
共催:NII共同研究「SAT変換による制約最適化問題の限界突破」
講演者:Reiner Hähnle教授,Niklas Sörensson氏

プログラム

2月4日 (木)

15:00 〜 15:10 オープニングおよび講演者紹介
15:10 〜 16:10 Generating Unit Tests from Formal Proofs [PDF]
Reiner Hähnle (Chalmers University of Technology, Sweden)
abstract: We present an automatic mixed white/black box test generation method for Java based on attempts at formal verification of the implementation under test (IUT). Self-contained unit tests in JUnit format are generated automatically. The advantages of the approach are: (i) it makes use of the full information available in the IUT and in its formal model (if present), thus giving good hybrid coverage; (ii) a non-trivial formal specification of the IUT is unnecessary; (iii) it is adaptable to the skills users may possess in formal methods, in particular, normal Java developers are able to use the method.
16:10 〜 16:30 休憩
16:30 〜 17:30 What's new in MiniSat 2.2 [PDF]
Niklas Sörensson (Chalmers University of Technology, Sweden)
abstract: This talk will give an overview of the upcoming release of MiniSat as well as some of the plans for future development. While no longer the top-performer according the last SAT competitions, it is still competitive and certainly a big improvement compared to the last public release of MiniSat. Updated heuristics and improved data structures are the two key ingredients for the increased performance. The new heuristics are rapid restarts and phase-saving (both commonly used nowadays); the new data structures are designed to improve memory behavior and speed of unit-propagation. Additionally, the preprocessing part of MiniSat has been made more robust, for instance by using more compact data structures for model extension.
18:30 〜 20:30 懇親会

懇親会

日時:2010年2月4日(木) 18:30 〜
お店:七輪炭焼 一徳
〒657-0027 神戸市灘区永手町3丁目4-18
TEL: (078) 842-5030

参加申込

以下の参加申込を,まで お送りください.
-------------------------------(cut here)-------------------------------
第1回CSPSAT講演会 (2010年2月4日) 参加申込

お名前:

懇親会に
   ・ 出席します
   ・ 欠席します
   (一方を残してください)

-------------------------------(cut here)-------------------------------