Menu
  • Specyfikacje ilościowe: uczenie się, algorytmy i zastosowania

    Kierownik: dr hab. Jan Otop
    Okres realizacji: 2018-2021
    Projekt badawczy finansowany przez Narodowe Centrum Nauki

    W dzisiejszych czasach systemy informatyczne stanowią nieodłączną część życia. Mimo dużych postępów w dziedzinach inżynierii
    oprogramowania i testowania, wciąż napotyka się na różnego rodzaju błędy, zarówno w sprzęcie, jak i w oprogramowaniu. Aby wyeliminować błędy zaproponowano formalną weryfikację, w której dowodzi się poprawności programów i układów cyfrowych. Formalna weryfikacja jest intensywnie badana teoretycznie oraz intensywnie rozwijana w przemyśle: Intel stosuje ją przy tworzeniu procesorów; Microsoft i Facebook stosują ją przy tworzeniu oprogramowania; Bosch stosuje ją przy projektowaniu tempomatów w samochodach. Wiodącą techniką w formalnej weryfikacji jest weryfikacja modeli, w ramach której sprzęt lub oprogramowanie abstrahuje się do uproszczonych struktur, nazywanych \emph{modelami}, celem dokonania weryfikacji ich poprawności.

    Weryfikacja modeli daje odpowiedź jakościową: ,,tak'' albo ,,nie''. Pozwala to odpowiadać na pytania w stylu ,,czy serwer odpowie na każde żądanie''. Jednak odpowiedź pozytywna na takie pytanie jest często niewystarczająca, gdyż nie określa, jak szybko serwer odpowie. Dlatego ważne są również aspekty ilościowe, na przykład pytanie ,,jaki jest średni czas pomiędzy żądaniem a odpowiedzią serwera''. Aby móc wnioskować o aspektach ilościowych systemów, stosuje się ilościową weryfikację modeli, w której można zadawać wartości liczbowe oraz otrzymywać liczby jako  odpowiedzi. Takie odpowiedzi niosą ze sobą więcej informacji, które lepiej oddają poprawność systemu. Pomimo swoich zalet, ilościowa weryfikacja modeli nie jest używana w praktyce z powodu licznych trudności. Opisywanie własności ilościowych jest trudne, problem weryfikacji własności  ilościowych jest obliczeniowo trudny, a interpretacja ilościowych odpowiedzi jest trudna. Celem tego projektu jest zniwelowanie powyższych trudności.

    W tym projekcie badawczym postaramy się usprawnić proces ilościowej weryfikacji modeli skupiając się na trzech etapach weryfikacji: specyfikacji własności ilościowych, algorytmach weryfikacji modeli względem własności ilościowych, oraz interpretacji odpowiedzi ilościowych zwracanych w procesie weryfikacji.

    Aby uczynić proces tworzenia specyfikacji łatwiejszym dla użytkowników, będziemy badali obliczeniowe uczenie się specyfikacji
    oraz języki zadawania specyfikacji. Będziemy badać dwa rodzaje problemów: uczenie \emph{offline}, w którym użytkownik jednorazowo podaje pewną listę przykładów i na ich podstawie generowana jest specyfikacja, oraz uczenie online, w czasie którego algorytm może zadawać użytkownikowi dodatkowe pytania dotyczące słów, a także pytać, czy dana specyfikacja jest taka, jak żądano. Podobne techniki uczenia się z powodzeniem sprawdzają się w klasycznej weryfikacji.

    Zakładając, że mamy zadaną specyfikację ilościową, kolejnym krokiem w weryfikacji jest obliczenie jej wartości na danym modelu systemu. Modele często bywają bardzo duże, dlatego ważne jest znajdowanie efektywnych algorytmów do weryfikacji, a w szczególności takich, które korzystają z technik pozwalających operować na mniejszy modelach. W tym projekcie podejmiemy próbę stworzenia takich algorytmów dla weryfikacji ilościowej.

    Podobnie jak w oprogramowaniu, błędy mogą się również zdarzać w specyfikacjach. Może to prowadzić do sytuacji, gdy w wyniku
    weryfikacji otrzymujemy informację, że nasz system zachowuje się poprawnie, podczas gdy tak nie jest. Planujemy stworzyć narzędzia wspomagające wykrywanie tego typu przypadków. Celem takich narzędzi byłoby wskazywanie użytkownikowi, że jego specyfikacja, na przykład, jest spełniona podejrzanie łatwo lub że wynik procesu weryfikacji nie zależy od dużej części modelu.

  • Combinatorial optimization through the lens of the traveling salesman route and matchings

    Leader: dr hab. Katarzyna Paluch
    Funded by Polish National Science Centre.
    2019-2022

  • Algorithmic techniques for solving social and economic issues

    Leader: mgr Krzysztof Sornat
    Funded by Polish National Science Centre.
    2018-2019

  • Online algorithms for packing and covering problems

    Leader: mgr Maciej Pacut
    Funded by Polish National Science Centre.
    2017-2018

  • Algebraic Effects and Continuations

    Leader: Maciej Piróg
    Funding agency: Polish National Science Centre
    Time frame: 2017–2019

  • Scalable reasoning about imperative concurrent programs

    Leader: Filip Sieczkowski
    Funding agency: Polish National Science Centre
    Time frame: 2017–2020

  • Algorithmic online optimization for graph problems

    Leader: dr hab. Marcin Bieńkowski
    Funded by Polish National Science Centre.
    2017-2022

    The goal of this project is to deliver new algorithmic methods for various problems related to online optimization. The considered problems span vast areas of computer networks, telecommunications, distribution networks and supply-chain management. Rather than focusing on a specific application, we address a broad scope of fundamental building blocks, crucial in many optimization procedures.

    The particular research directions we pursue are split into three categories: (i) developing online algorithms for efficient dynamic placement of resources in a graph, (ii) developing online algorithms for leasing of resources, (iii) investigating gains of reordering and aggregating demands.

  • Throughput Maximization Problems

    Leader: dr Łukasz Jeż
    Funded by Polish National Science Centre.
    2017-2020

  • Application of modern algorithmic methods for solving NP-hard clustering problems

    Leader: mgr Krzysztof Sornat
    Funded by Polish National Science Centre.
    2016-2019

  • Zastosowanie logiki z funkcjami częściowymi - Kierownik: dr hab Jean Marie de Nivelle

    Okres realizacji: 2016-2019

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Algorithmic fundamentals of supply chain networks

    Leader: dr hab. Jarosław Byrka
    Funded by Polish National Science Centre.
    2016-2021

    The drive to minimize costs in logistics, and supply-chain networks in particular, results in the need to aggregate traffic both in space and over time. This motivates the study of the underlying combinatorial optimization problems. The two biggest challenges are the intractability resulting from the presence of combinatorial constraints such as unsplittability of shipments, and the uncertainty of the future demand.

    State-of-the-art solution methods for a number of the fundamental network design and management problems are still far from being best possible and are often complex compositions of routines developed for more restricted settings. Also the issue of scheduling of shipments on the existing network leaves many unresolved questions, especially in the online case where shipment requests arrive over time.

    The particular directions we consider are: 1) to develop direct algorithms for a number of hierarchical network design settings based on rounding solutions to strong convex relaxations of the studied problems, 2) resolve the possibility to aggregate traffic on multilevel networks in the online request arrival model, 3) take temporal aspects of the anticipated demand into account at the stage of designing a network, possibly allowing designs with non-standard topologies.

  • Audioscope - system do automatycznego wyszukiwania treści w nagraniach w języku polskim metodą hybrydową - Kierownik: dr Paweł Rychlikowski

    Okres realizacji: 2015-2017

    Projekt realizowany w ramach Programu Badań Stosowanych Narodowego Centrum Badań i Rozwoju

  • Problemy komunikacyjne w bezprzewodowych sieciach sensorowych - Kierownik: mgr Michał Rożański

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki


  • Automaty z wagami dla własności kwantytatywnych - Kierownik: dr Jan Otop

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Zastosowanie rekurencyjnych i głębokich sieci neuronowych do modelowania akustycznego sygnału mowy - Kierownik: dr inż. Jan Chorowski

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Kompresja, logika, języki formalne: nowe podejścia łączące różne dziedziny - Kierownik: dr Artur Jeż

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Metody wnioskowania o programach w językach wyższego rzędu - Kierownik: prof. dr hab. Witold Charatonik

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Logiki do przetwarzania danych i weryfikacji - Kierownik: dr Jakub Michaliszyn

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Online algorithms for fundamental network problems

    Leader: dr hab. Marcin Bieńkowski
    Funded by Polish National Science Centre.
    2014-2017

    Currently in the Internet, packets are delivered using best-effort strategies: while network devices like routers and switches do their best, there are hardly any guarantees on timely packet delivery. The best-effort paradigm is also commonly used in other aspects of fundamental network echanisms, such as routing table organization, maintaining access to shared data, etc. The goal of the project is to design and analyze algorithms that introduce or improve quality of service (QoS) for network applications.

    We identified several fundamental network mechanisms that are algorithmically challenging and whose improvements — in a long term perspective — would bring qualitative change for already existing applications. The first part of the project focuses on optimizing the mechanisms used within a single router. We consider research challenges related to managing the queues of packets to be transmitted (e.g., answering the question which packet should be sent first and which should be dropped) and the problems of maximizing the number of correctly transmitted movie frames. We also plan to address the problem of compressing the routing tables (also in the presence of its frequent updates). The second part of the project focuses on two important issues arising while serving multiple users. The first task concerns the implementation of a reliable multicast transmission: to this end, we plan to efficiently aggregate the transmitted acknowledgements. The second task focuses on constructing smart mechanisms of migrating shared services, simultaneously minimizing the user-experienced latency and monetary costs of migration.

  • Hipoteza BDD/FC i okolice - Kierownik: mgr Tomasz Gogacz

    Okres realizacji: 2014-2017

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Synchronizacja automatów i hipoteza Cerny'ego - Kierownik: mgr Marek Szykuła

    Okres realizacji: 2014-2016

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Efficient approximation algorithms for finding the optimal traveling salesman tours and related problems

    Leader: dr Katarzyna Paluch
    Funded by Polish National Science Centre.
    2014-2017

    The traveling salesman problem (TSP) belongs to one of the most heavily researched problems in computer science due both to its theoretical appeal and wide applications. The key objective of the project is to design approximation algorithms for important variants of the traveling salesman problem achieving better approximation factors than those known so far. We are going to study the maximization variants of the traveling salesman problem, the minimization variants and the problems connected with finding cycle cover and matchings with special properties.

  • Języki i uczenie w General Game Playing - Kierownik: mgr Jakub Kowalski

    Okres realizacji: 2014-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Obliczenia rozproszone w sieciach dynamicznych - Kierownik: dr hab. Tomasz Jurdziński

    Okres realizacji: 2013-2016

    Projekt badawczy finansowane przez Narodowe Centrum Nauki

  • Konstrukcja i analiza skalowanych algorytmów dla sieci bezprzewodowych - Kierownik: dr hab. Tomasz Jurdziński

    Okres realizacji: 2013-2016

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • LP rounding approximation algorithms

    Leader: mgr Bartosz Rybicki
    Funded by Polish National Science Centre.
    2013-2016

  • Prototyp serwerowego Systemu Akceleracji zadań Analizy i wizualizacji obrazów mikroskopowych oraz Symulacji przepływów krwi do wykorzystania w biomedycznych systemach teleinformatycznych

    Kierownik:prof. Leszek Pacholski

    Okres realizacji: 2012-2013

    Projekt realizowany wspólnie z firmą Vratis w ramach programu "Innotech" Narodowego Centrum Badań i Rozwoju


  • COSSAR - Cooperative Spectrum Sensing Algorithms for Cognitive Radio - Stypendysta: Radosław Piesiewicz

    Okres realizacji: 2010-2012

    Projekt realizowany w ramach programu "Marie Curie Actions - Intra-European Fellowships" (IEF).


  • Struktura i interpretacja języków programowania w paradygmacie "dowody jako programy" - Kierownik: dr Małgorzata Biernacka

    Okres realizacji: 2012-2015

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Procedury decyzyjne w weryfikacji - Kierownik: prof. dr hab. Witold Charatonik

    Okres realizacji: 2012-2015

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Wokół logik modalnych - rozstrzygalność i złożoność - Kierownik: dr Jakub Michaliszyn

    Okres realizacji: 2012-2015

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • GreenNets (Power consumption and CO2 footprint reduction in mobile networks by advanced automated network management approaches)

    University of Wrocław coordinator: prof. Leszek Pacholski
    University of Wroclaw investigator: dr hab. Marcin Bieńkowski
    Funded within FP7-SME-2011-BSG
    2011-2013
    http://www.greennets.eu/

  • Dualne funkcje B-sklejane: konstrukcja i zastosowania - Kierownik: dr hab. Paweł Woźny

    Okres realizacji: 2011-2013

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Wydajne algorytmy i reprezentacje w teorii języków formalnych i automatów - Kierownik: dr Artur Jeż

    Okres realizacji: 2011-2014

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • LP-based approximation algorithms

    Leader: dr Jarosław Byrka
    Funded by Foundation for Polish Science within Homing Plus programme.
    2010-2013

  • Online scheduling

    Leader: mgr Łukasz Jeż
    Funded by Ministry of Science and Higher Education.
    2010-2011

  • Automaty, gramatyki, równania: minimalizacja i siła wyrazu - Kierownik: dr hab. Tomasz Jurdziński

    Okres realizacji: 2010-2012

    Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Zagadnienia złożoności i rozstrzygalności dla teorii logicznych motywowanych informatyką - Kierownik: prof. dr hab. Jerzy Marcinkowski

    Okres realizacji: 2010-2013

    Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Approximation algorithms under uncertainty

    Leader: dr Marcin Bieńkowski
    Funded by Ministry of Science and Higher Education.
    2010-2013

  • Automatyczne wnioskowanie w teoriach równościowych (promotorski) - Kierownik: prof. dr hab. Jerzy Marcinkowski

    Okres realizacji: 2009-2010

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Semantyka języków programowania i transformacji programów: derywacje i certyfikacja w teorii typów systemu Coq - Kierownik: dr Dariusz Biernacki

    Okres realizacji: 2009-2011

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Analiza kombinatoryczna algorytmów rozproszenia (promotorski) - Kierownik: prof. dr hab. Mirosław Kutyłowski

    Okres realizacji: 2008-2010

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Gramatyki koniunkcyjne i układy równań języków (promotorski) - Kierownik: prof. dr hab. Krzysztof Loryś

    Okres realizacji: 2008-2010

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Algorytmy aproksymacyjne i online - Kierownik: prof. dr hab. Krzysztof Loryś

    Okres realizacji: 2007-2010

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Metody teorii automatów i języków formalnych w problemach wyszukiwania wzorca, weryfikacji bezpieczeństwa systemów, złożoności obliczeniowej oraz w analizie języków naturalnych Kier: dr T. Jurdziński

    Okres realizacji: 2006-2008

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Konstrukcja i analiza algorytmów aproksymacyjnych dla grafowych problemów optymalizacyjnych (promotorski) - Kierownik: prof. dr hab. Krzysztof Loryś

    Okres realizacji: 2006-2008

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Dynamic networks: exploration and data management

    Leader: dr Marcin Bieńkowski
    Funded by Ministry of Science and Higher Education.
    2006-2008

  • Rozstrzygalność pewnych teorii logicznych motywowanych teorią informatyki - Kierownik: dr hab. Jerzy Marcinkowski

    Okres realizacji: 2006-2009

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Bezpieczeństwo obliczeń komputerowych - Kierownik: prof. dr hab. Leszek Pacholski

    Okres realizacji: 2006-2009

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Edukacja Informatyczna w Polskim Systemie Szkolnym (promotorski) - Kierownik: prof. dr hab. Maciej M. Sysło

    Okres realizacji: 2001-2002

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Optymalizacja kosztów obliczeń metod Monte Carlo syntezy obrazów przy zastosowaniu operatorów Minkowskiego i offsetów (promotorski) - Kierownik: prof. dr hab. Leszek Pacholski

    Okres realizacji: 2000-2001

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Równoległe i sekwencyjne algorytmy aproksymacyjne dla problemów kombinatorycznych i geometrycznych - Kierownik: prof. dr hab. Krzysztof Loryś

    Okres realizacji: 2000-2002

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Zastosowanie pojęcia typów do weryfikacji i certyfikacji programów - Kierownik: prof. dr hab. Leszek Pacholski

    Okres realizacji: 2000-2003

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Zastosowanie związków rekurencyjnych w teorii szeregów ortogonalnych - Kierownik: prof. dr hab. Stanisław Lewanowicz

    Okres realizacji: 1999-2001

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Specyfikacje ilościowe: uczenie się, algorytmy i zastosowania

    Kierownik: dr hab. Jan Otop
    Okres realizacji: 2018-2021
    Projekt badawczy finansowany przez Narodowe Centrum Nauki

     

    Wdzisiejszychczasachsystemyinformatycznestanowa˛nieodła˛czna˛cze˛´ s´ c ˙zycia. Mimodu˙zych poste˛pów w dziedzinach in˙zynierii oprogramowania i testowania, wcia˛˙z napotyka sie˛ na ró˙znego rodzajubłe˛dy,zarównowsprze˛cie,jakiwoprogramowaniu. Abywyeliminowa´cbłe˛dyzaproponowano formalna˛weryfikacje˛, w której dowodzi sie˛ poprawno´sci programów i układów cyfrowych. Formalnaweryfikacjajestintensywniebadanateoretycznieorazintensywnierozwijanawprzemy´ sle: Intel stosuje ja˛przy tworzeniu procesorów; Microsoft i Facebook stosuja˛ja˛przy tworzeniu oprogramowania; Bosch stosuje ja˛ przy projektowaniu tempomatów w samochodach. Wioda˛ca˛ technika˛w formalnej weryfikacji jest weryfikacja modeli, w ramach której sprze˛t lub oprogramowanie abstrahuje sie˛ do uproszczonych struktur, nazywanych modelami, celem dokonania weryfikacji ich poprawno´sci. Weryfikacja modeli daje odpowiedz´ jako´sciowa˛: „tak” albo „nie”. Pozwala to odpowiada´c na pytania w stylu „czy serwer odpowie na ka˙zde ˙za˛danie”. Jednak odpowiedz´ pozytywna na takie pytanie jest cze˛sto niewystarczaja˛ca, gdy˙z nie okre´sla, jak szybko serwer odpowie. Dlatego wa˙zne sa˛ równie˙z aspekty ilo´sciowe, na przykład pytanie „jaki jest ´sredni czas pomie˛dzy ˙za˛daniem a odpowiedzia˛serwera”. Aby móc wnioskowa´c o aspektach ilo´sciowych systemów, stosuje sie˛ ilo´ sciowa˛weryfikacje˛ modeli, w której mo˙zna zadawa´c warto´sci liczbowe oraz otrzymywa´c liczby jako odpowiedzi. Takie odpowiedzi niosa˛ze soba˛wie˛cej informacji, które lepiej oddaja˛poprawno´ s´c systemu. Pomimo swoich zalet, ilo´sciowa weryfikacja modeli nie jest u˙zywana w praktyce z powodu licznych trudno´sci. Opisywanie własno´sci ilo´sciowych jest trudne, problem weryfikacji własno´sciilo´sciowychjestobliczeniowotrudny,ainterpretacjailo´sciowychodpowiedzijesttrudna. Celem tego projektu jest zniwelowanie powy˙zszych trudno´sci. W tym projekcie badawczym postaramy sie˛ usprawni´c proces ilo´sciowej weryfikacji modeli skupiaja˛csie˛ natrzechetapachweryfikacji: specyfikacjiwłasno´sciilo´sciowych,algorytmachweryfikacji modeli wzgle˛dem własno´sci ilo´sciowych, oraz interpretacji odpowiedzi ilo´sciowych zwracanych w procesie weryfikacji. Aby uczyni´c proces tworzenia specyfikacji łatwiejszym dla u˙zytkowników, be˛dziemy badali obliczeniowe uczenie sie˛ specyfikacji oraz je˛zyki zadawania specyfikacji. Be˛dziemy bada´c dwa rodzaje problemów: uczenie offline, w którym u˙zytkownik jednorazowo podaje pewna˛liste˛ przykładów i na ich podstawie generowana jest specyfikacja, oraz uczenie online, w czasie którego algorytm mo˙ze zadawa´c u˙zytkownikowi dodatkowe pytania dotycza˛ce słów, a tak˙ze pyta´c, czy dana specyfikacja jest taka, jak ˙za˛dano. Podobne techniki uczenia sie˛ z powodzeniem sprawdzaja˛ sie˛ w klasycznej weryfikacji. Zakładaja˛c, ˙zemamyzadana˛specyfikacje˛ ilo´sciowa˛,kolejnymkrokiemwweryfikacjijestobliczenie jej warto´sci na danym modelu systemu. Modele cze˛sto bywaja˛bardzo du˙ze, dlatego wa˙zne jest znajdowanie efektywnych algorytmów do weryfikacji, a w szczególno´sci takich, które korzystaja˛ z technik pozwalaja˛cych operowa´c na mniejszy modelach. W tym projekcie podejmiemy próbe˛ stworzenia takich algorytmów dla weryfikacji ilo´sciowej. Podobnie jak w oprogramowaniu, błe˛dy moga˛ sie˛ równie˙z zdarza´c w specyfikacjach. Mo˙ze to prowadzi´c do sytuacji, gdy w wyniku weryfikacji otrzymujemy informacje˛, ˙ze nasz system zachowuje sie˛ poprawnie, podczas gdy tak nie jest. Planujemy stworzy´c narze˛dzia wspomagaja˛ce wykrywanie tego typu przypadków. Celem takich narze˛dzi byłoby wskazywanie u˙zytkownikowi, ˙ ze jego specyfikacja, na przykład, jest spełniona podejrzanie łatwo lub ˙ze wynik procesu weryfikacji nie zale˙zy od du˙zej cze˛´sci modelu.