Seminaria ogólnoInstytutowe:


Informacje:

Poniedziałki, o godz. 13:00
Miejsce seminarium: sala seminaryjna IPI PAN
ul. Jana Kazimierza 5
e-mail: Beata.Konikowska@ipipan.waw.pl 

 Archiwum Seminarium Instytutowego  Archiwum Seminarium Doktoranckiego
2015/2016 2010/2011 2005/2006 2004/2005
2014/2015 2009/2010   2003/2004
2013/2014 2008/2009   2002/2003
2012/2013 2007/2008   2001/2002
2011/2012 2006/2007    

10.12.2018 - Seminarium Instytutowe - godz. 13:00,

Andrzej Jacek Blikle (IPI PAN) 

Streszczenie (autorskie):

Czy można sobie wyobrazić, by klient kupujący samochód podpisywał zrzeczenie się wszelkich praw do roszczeń (ang. disclosure), gdyby wady techniczne samochodu miały narazić go na szkody? Chyba nie. To dlaczego w przemyśle IT jest to powszechny standard?
Moim zdaniem ten paradoks bierze się stąd, że podczas gdy każdy produkt techniczny powstaje na gruncie matematycznych obliczeń stanowiących swoisty „dowód jego poprawności”, to w informatyce takich dowodów przeprowadzać nie umiemy.
Problem pozyskiwania matematycznych gwarancji poprawności programów pojawił się po raz pierwszy w pracy Alana Turinga w roku 1949. Później przez kilka dekad podejmowano ten temat pod hasłem dowodzenia poprawności programów, a równolegle też próby definiowania takich semantyk języków programowania, które byłyby podstawą do prowadzenia dowodów poprawności.
Niestety w żadnym z obu obszarów nie dopracowano się metod, które weszłyby na stałe do repertuaru narzędzi inżynierii oprogramowania. Wreszcie zaniechano tych badań, co autorzy mo-nografii Deductive Software Verification z roku 2016 podsumowali stwierdzając (tłumaczenie moje):
Przez wiele lat pojęcie formalnej weryfikacji było niemalże synonimem weryfikacji funkcjonalnej. W ostatnich latach staje się coraz bardziej jasne, że pełna funkcjonalna weryfikacja programu jest dla prawie wszystkich zastosowań celem iluzorycznym.
W mojej ocenie niepowodzenie opisanych wyżej prób miało dwa źródła:
Po pierwsze, dla większości istniejących języków programowania zapewne nie da się zbudować takiej semantyki, która mogłaby służyć do praktycznego dowodzenia poprawności programów. To oczywiście tylko opinia, ale fakt, że od 1949 roku tego nie udało się tego dokonać, o czymś jednak świadczy.
Po drugie, nawet gdyby taką semantykę zbudowano, to dla większości programów dowodów po-prawności nie da się przeprowadzić z prostego powodu, że one poprawne nie są! Stąd też praktyczną wartość dowodzenia poprawności upatrywano w nadziei, że próba dowodzenia poprawności programu wskaże na zawarte w nim błędy.
W trakcie seminarium przedstawię pewną nową propozycję podjęcia problemu poprawności pro-gramów, a także wyjaśnię, dlaczego wymaga to „odwrócenia tradycyjnej kolei rzeczy”. Choć moja propozycja jest oparta na dość specyficznej matematyce, postaram się przedstawić ją w sposób strawny dla osób, które tej matematyki mogą nie znać. A tym, którzy chcieliby do niej sięgnąć, proponuję moją książkę (w stanie surowym) „Denotacyjna inżynieria języków programowania”, którą mogę udostęp-nić w wersji cyfrowej. Z jej wydaniem na razie się nie spieszę, by zebrać jak najwięcej opinii czytel-ników. I oczywiście, za wszelkie takie opinie będę niezmiernie wdzięczny.

26.11.2018 - Seminarium Instytutowe - godz. 13:00,

Wojciech Jamroga (IPI PAN) 

Abstract:
SELENE is a recently proposed voting protocol that provides reasonable protection against coercion. Both verifiability and security of Selene are based on cryptographic machinery applied to the concept of tracking numbers assigned to votes. In this paper, we make the first step towards a formalization of selected features of the protocol by means of formulae and models of multi-agent logics. The models define the space of strategies for the voters, the election authority, and the potential coercer. We express selected properties of the protocol using the strategic logic ATLir, and conduct preliminary verification by model hecking. While ATLir allows for intuitive specification of requirements like coercion-resistance, model checking of ATLir is notoriously hard. We show that some of the complexity can be avoided by using a recent approach of approximate model checking, based on fixpoint approximations.

22.10.2018 - Seminarium Instytutowe - godz. 13:00,

Laure Petrucci (Université Paris 13) 

Camille Coti, Sami Evangelista, Laure Petrucci: One-Sided Communications and Distributed State Compression for Distributed Model-Checking

Abstract:
Communications are often the bottleneck in distributed state space exploration. To overcome this problem and benefit from the distributed model-scheme, we propose to use one-sided communications. We thus revisit the state of the art distributed algorithm and adapt it to RDMA clusters with an implementation over the OpenSHMEM library. Experiments conducted on the Grid'5000 cluster show that this asynchronous approach reduces the significant communication costs induced by process synchronisation in two-sided communications.
To further improve distributed model checking, we propose a distributed implementation of the collapse compression technique used by explicit state model checkers to reduce memory usage. This adapatation makes use of lock-free distributed hash tables based on one-sided communication primitives. The experiments reveal that, for some models, this distributed implementation can altogether preserve the memory reduction provided by collapse compression and reduce execution times by allowing the exchanges of compressed states between processes.

08.10.2018 - Seminarium Instytutowe - godz. 13:00,

Teofil Sidoruk (Instytut Podstaw Informatyki PAN) 

20181008 Sidoruk

W seminarium przedstawię dziewięć SAT-solverów, w tym nowoczesne narzędzia takie jak Lingeling, Glucose i Clasp, których efektywność zostanie porównana dla problemów obliczeniowych o różnej złożoności: od P (dwie popularne zagadki szachowe) do EXPTIME (wieże Hanoi), ale głównie będą to problemy NP-zupełne. Należą do nich problem odpowiedniości Posta (BPCP), extended string-to-string correction (ESCP) a także trzy klasyczne zagadnienia z teorii grafów. Ponadto dla niektórych problemów (m.in. BPCP i ESCP) definiujemy własne, oryginalne kodowania do SAT. Przedstawione wyniki eksperymentalne pozwalają na wyciągnięcie ciekawych wniosków odnośnie efektywności i przydatności SAT-solverów do rozwiązywania problemów o różnej złożoności. Ponadto, po przeprowadzonych testach analizuję formuły w postaci CNF zawarte w wygenerowanych benchmarkach w poszukiwaniu charakterystycznych wspólnych cech dla relatywnie najłatwiejszych i najtrudniejszych instancji.

04.06.2018 - Seminarium Instytutowe - godz. 13:00,

Przemysław Spurek (Uniwersytet Jagielloński) 

We propose a new generative model, Cramer-Wold Autoencoder (CWAE). Following WAE, we directly encourage normality of the latent space. Our paper uses also the recent idea from Sliced WAE (SWAE) model, which uses one-dimensional projections as a method of verifying closeness of two distributions. The crucial new ingredient is the introduction of a new (Cramer-Wold) metric in the space of densities, which replaces the Wasserstein metric used in SWAE. We show that the Cramer-Wold metric between Gaussian mixtures is given by a simple analytic formula, which results in the removal of sampling necessary to estimate the cost function in WAE and SWAE models.

As a consequence, while drastically simplifying the optimization procedure, CWAE produces samples of a matching perceptual quality to other SOTA models.

Marek Śmieja (Uniwersytet Jagielloński) 

We propose a general, theoretically justified mechanism for processing missing data by neural networks. Our idea is to replace typical neuron’s response in the first hidden layer by its expected value. This approach can be applied for various types of networks at minimal cost in their modification. Moreover, in contrast to recent approaches, it does not require complete data for training. Experimental results performed on different types of architectures show that our method gives better results than typical imputation strategies and other methods dedicated for incomplete data.

UWAGA! Ten serwis używa cookies i podobnych technologii.

Brak zmiany ustawienia przeglądarki oznacza zgodę na to.

Zrozumiałem