| Powrót do listy seminariów |
| 2006-05-23, godz. 14:15 - 16, s. 5840, |
| Sławomir Białecki (Uniwersytet Warszawski) |
| Technika podziału jako strategia dowodzenia poprawności programów imperatywnych |
| Zaprezentuję przykłady użycia techniki podziału (partition testing) do udoskonalenia formalnego dowodzenia poprawności pętli (przez indukcję). Wykorzystując podział dziedziny indukcji zostanie w sposób automatyczny wyprowadzona ulepszona reguła dowodzenia przez indukcję. Reguła ta okazuję się łatwiejsza w użyciu, będząc "przykrojoną" do aktualnie dowodzonego konkretnego programu. Na podstawie artykułów: 1. Rainer Hahnle and Angela Wallenburg, Using a Software Testing Technique to Improve Theorem Proving. 2. Ola Olsson and Angela Wallenburg, Automatic Generation of Customized Induction Rules for Proving Correctnes of Imperative Programs. |
| 2006-03-24, godz. 15:00, s. 5870 |
| dr Adam Naumowicz (Uniwersytet w Białymstoku) |
| Mizar - prezentacja systemu oraz jego zasosowań w dydaktyce |
| MIZAR to komputerowy system do weryfikacji dowodów.
Tematem referatu będzie prezentacja:
* podstaw teoretycznych systemu Mizar,
* samego narzędzia w działaniu,
* zastosowań systemu w dydaktyce logiki i teorii mnogości.
Więcej informacji: http://mizar.uwb.edu.pl |
| 2005-11-08, godz. 14:15 - 16, s. 5840 |
| Marcin Benke (Uniwersytet Warszawski) |
| Cover - Combining Verification Methods in Software Development |
| The goal of the Cover project is to develop methods for improving software quality. The approach is to integrate a variety of verification methods into a framework which permits a smooth progression from hacking code to fully formal proofs of correctness. By a pragmatic integration of different techniques - testing, automated and interactive proving - in a next-generation program development tool, we hope to handle systems on a much larger scale than hitherto.
Więcej informacji: http://coverproject.org |
| 2005-10-18, godz. 14:15 - 16, s. 5840 |
| Bartek Klin (Uniwersytet Warszawski) |
| [SLIW] Teoria strukturalnej semantyki operacyjnej |
| 2005-10-11, godz. 14:15 - 16, s. 5840 |
| Aleksy Schubert (Uniwersytet Warszawski) |
| [Mobius] Logic for Java bytecode |
| 2005-10-04, godz. 14:15 - 16, s. 5840 |
| Aleksy Schubert (Uniwersytet Warszawski) |
| Ustalanie tematów referatów/Prezentacja projektu Mobius |
| 2005-05-24, godz. 15:00 - 16:00, s. 5820 |
| Nguyen Anh Linh (Uniwersytet Warszawski) |
| Negative Hyper-Resolution as a Proof Procedure for Disjunctive Logic Programming |
| 2005-05-24, godz. 14:15 - 15:00, s. 5820 |
| Jarosław Kuśmierek (Uniwersytet Warszawski) |
| Mixins, mixins, mixins... Everything is a mixin! |
| 2005-05-17, godz. 14:15 - 16, s. 5820 |
| Michal Strojnowski (Uniwersytet Warszawski) |
| Quantum programming languages |
Więcej informacji: http://www.mimuw.edu.pl/~alx/Seminarium/seminarium.html |