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 | 懇親会 |
-------------------------------(cut here)------------------------------- 第1回CSPSAT講演会 (2010年2月4日) 参加申込 お名前: 懇親会に ・ 出席します ・ 欠席します (一方を残してください) -------------------------------(cut here)-------------------------------