Granty

• Algorytmy online dla problemów konfiguracyjnych

  Kierownik: dr hab. Marcin Bieńkowski

  Okres realizacji: 2023-2026

  Projekt badawczy finansowany przez Narodowe Centrum Nauki

• Od silnych logik deskrypcyjnych do fragmentów logiki pierwszego rzędu z wieloma zmiennymi: wnioskowania w strukturach skończonych

  Kierownik: dr hab. Emanuel Kieroński

  Okres realizacji: 2022-2026

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Wnioskowanie ilościowe odporne na perturbacje

  Kierownik: dr Jakub Michaliszyn

  Okres realizacji: 2021-2025

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Wydajne algorytmy rozproszone i równoległe dla dużych i dynamicznych danych

  Kierownik: prof. dr hab. Tomasz Jurdziński

  Okres realizacji: 2021-2024

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Efektywne wykorzystanie randomizacji: od szeregowania do AdWords

  Kierownik: dr Łukasz Jeż

  Okres realizacji: 2021-2025

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Algorytmy dla projektowania połączeń w warunkach niepewności

  Kierownik: dr hab. Jarosław Byrka

  Okres realizacji: 2021-2025

  Projekt badawczy finansowany przez Narodowe Centrum Nauki

• Algebraiczne techniki zrównoleglania algorytmów

  Kierownik: dr Przemysław Uznański

  Okres realizacji: 2020-2023

  Projekt badawczy finansowany przez Narodowe Centrum Nauki

• Odkrywanie ukrytej struktury danych na podstawie obserwacji

  Kierownik: dr hab. Jan Chorowski/ dr hab. Piotr Wnuk-Lipiński

  Okres realizacji: 2020-2023

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Maszyny abstrakcyjne dla języków programowania: podejście derywacyjne

  Kierownik: prof. dr hab. Witold Charatonik

  Okres realizacji: 2020-2023

  Projekt badawczy finansowany przez Narodowe Centrum Nauki

• Optymalizacja kombinatoryczna w warunkach niepewności: matroidy, skojarzenia i funkcje submodularne

  Kierownik: dr Marek Adamczyk

  Okres realizacji: 2020-2023

• Optymalizacja kombinatoryczna przez pryzmat trasy komiwojażera i skojarzeń

  Kierownik: dr hab. Katarzyna Paluch
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2019-2022
  Kwota: 588 000 zł

• Projektowanie algorytmów rozproszonych dla silnie obciążonych sieci

  Kierownik: dr hab. Tomasz Jurdziński

  Okres realizacji: 2018-2022

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

   

• Wybrane zagadnienia kompresji gramatykowej

  Kierownik: dr hab. Artur Jeż

  Okres realizacji: 2018-2023

  Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Zastosowanie algorytmiki w kontekście wybranych zagadnień społecznych i ekonomicznych.

  Kierownik: mgr Krzysztof Sornat
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2018-2019

• Algorytmiczna optymalizacja online dla problemów grafowych

  Kierownik: dr hab. Marcin Bieńkowski

  Okres realizacji: 2017-2023

  Projekt badawczy finansowany przez Narodowe Centrum Nauki

• Algorytmy online dla problemów pakowania i pokrywania

  Kierownik: mgr Maciej Pacut
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2017-2018

• Algebraic Effects and Continuations

  Kierownik: Maciej Piróg
  Projekt finansowany przez Narodowe Centrum Nauki
  Okres realizacji: 2017–2019

• Skalowalne metody wnioskowania o imperatywnych programach współbieżnych

  Kierownik: Filip Sieczkowski
  Projekt finansowany przez Narodowe Centrum Nauki
  Okres realizacji: 2017–2020

• Algorytmiczna optymalizacja online dla problemów grafowych

  Kierownik: dr hab. Marcin Bieńkowski
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2017-2022
  Kwota: 1 225 850 zł

  Celem projektu jest stworzenie nowych algorytmicznych metod dla problemów związanych z optymalizacją online. Rozważane problemy dotyczą szerokiego zakresu zagadnień związanych z sieciami komputerowymi, telekomunikacją, sieciami transportowymi i zarządzaniem łańcuchem dostaw. Projekt nie skupia się na konkretnych zastosowaniach, lecz na fundamentalnych bazowych mechanizmach, kluczowych w wielu procedurach optymalizacyjnych.

  Kierunki badawcze projektu zostały podzielone na trzy kategorie: i) konstrukcja i analiza algorytmów online dla dynamicznego rozmieszczania zasobów w grafach, ii) konstrukcja i analiza algorytmów online dla problemów wypożyczania zasobów, iii) badanie korzyści wynikających z możliwości zmiany kolejności żądań i ich agregacji.

• Szeregowanie zadań w celu maksymalizacji liczby ukończonych zadań

  Kierownik: dr Łukasz Jeż
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2017-2020

• Zastosowanie nowoczesnych metod algorytmicznych w rozwiązywaniu NP-trudnych problemów klastrowania

  Kierownik: mgr Krzysztof Sornat
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 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
  

• Algorytmiczne podstawy optymalizacji sieci logistycznych

  Kierownik: dr hab. Jarosław Byrka
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2016-2021
  Kwota: 1 494 600 zł
  

  Szybki rozwój sieci transportowych wymusza automatyzację zarządzania logistyką. W procesie minimalizacji kosztów transportu stosuje się matematyczne modele problemów decyzyjnych. Największymi wyzwaniami dla badaczy przy konstrukcji metod optymalizacyjnych jest złożoność obliczeniowa podejmowanych problemów oraz konieczność planowania w warunkach niepewności.

  Na przykład przyszłe zapotrzebowanie na transport zależy od wielu nieprzewidywalnych czynników takich jak dynamika decyzji społecznych. Najlepsze znane algorytmy konstrukcji i zarządzania sieciami transportowymi są wciąż dalekie od perfekcji. Są one też często skomplikowanymi kompozycjami procedur powstałych celem realizacji prostszych zadań. Wiele otwartych problemów jest związanych z synchronizacją transportu w kontekście dynamicznie pojawiających się zleceń transportowych.

  W ramach projektu będą rozwijane nietrywialne metody algorytmiczne dla fundamentalnych problemów optymalizacyjnych związanych z sieciami transportowymi. W szczególności członkowie projektu skoncentrują się na konstrukcji algorytmów dla planowania hierarchicznych sieci transportowych. Będę również badać złożoność problemu dynamicznej agregacji transportu w wielopoziomowych sieciach drzewiastych, uwzględniając dynamikę zapotrzebowania na transport na etapie projektowania sieci transportowej.

• 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
  

• Algorytmy online dla podstawowych problemów sieciowych

  Kierownik: dr hab. Marcin Bieńkowski
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2014-2017
  

  Współcześnie w Internecie przekazywanie pakietów opiera się na polityce best-effort: urządzenia sieciowe przekazują pakiety dalej jak najszybciej, nie udzielając jednak żadnych gwarancji na temat czasu dostarczenia. Podejście typu best-effort stosowane jest też w przypadku wielu innych bazowych mechanizmów sieciowych, takich jak organizacja tablic routingu, dostęp do współdzielonych danych etc. Celem niniejszego projektu naukowego jest konstrukcja i analiza algorytmów wprowadzających lub poprawiających konkretne gwarancje dotyczące jakości usług sieciowych (Quality of Service, QoS)

  Zidentyfikowaliśmy kilka bazowych mechanizmów sieciowych, które stanowią wyzwanie algorytmiczne, a których poprawienie przyniosłoby istotne korzyści dla już istniejących sieciowych zastosowań. Pierwsza część projektu poświęcona jest optymalizacji metod wykorzystywanych wewnątrz routerów. W jej ramach zamierzamy usprawnić algorytmy kolejkowania pakietów (określające który pakiet powinien zostać wysłany jako pierwszy, a który wyrzucony) a także badać związane z nimi algorytmy maksymalizujące liczbę poprawnie dostarczonych ramek obrazu. Chcemy też tworzyć metody kompresujące tablice routingu (działające również w warunkach ciągłych zmian w tablicach). Druga część projektu dotyczy dwóch istotnych zagadnień związanych z jednoczesną obsługą wielu użytkowników. Pierwsze zagadnienie to implementacja niezawodnej (potwierdzanej) transmisji multicastowej: w tym celu zamierzamy opracować algorytmy efektywnego agregowania potwierdzeń poszczególnych pakietów. Drugie zadanie to tworzenie algorytmów migracji wirtualnych współdzielonych usług, minimalizujące jednocześnie odczuwane przez użytkowników opóźnienia i pieniężne koszty migracji.

• 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
  

• Efektywne algorytmy aproksymacyjne dla znajdowania optymalnej trasy komiwojażera i problemów pokrewnych

  Kierownik: dr Katarzyna Paluch
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 2014-2017
  

  Problem komiwojażera (Traveling Salesman Problem) jest jednym z najintensywniej badanych problemów informatycznych. Ma on zarówno duże znaczenie dla teorii informatyki, jak i dla praktyki. Głównym celem projektu będzie konstrukcja algorytmów aproksymacyjnych dla ważnych wariantów tego problemu, o współczynnikach aproksymacji lepszych niż znane dotychczas. W ramach projektu zamierzamy badać warianty maksymalizacyjne, minimalizacyjne oraz problemy dotyczące znajdowania pokryć cyklowych i skojarzeń o szczególnych własnościach.
  

• 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
  

• Algorytmy aproksymacyjne bazujące na zaokrąglaniu programów liniowych

  Kierownik: mgr Bartosz Rybicki
  Projekt finansowany przez Narodowe Centrum Nauki.
  Okres realizacji: 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

  
  

• 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)

  Koordynator na Uniwersytecie Wrocławskim: prof. Leszek Pacholski
  Wykonawca na Uniwersytecie Wrocławskim: dr hab. Marcin Bieńkowski, dr Rafał Nowak
  Finansowane w ramach FP7-SME-2011-BSG
  Okres realizacji: 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
  

• 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).

   

• LP-based approximation algorithms

  Kierownik: dr Jarosław Byrka
  Projekt realizowany w ramach Programu Homing Plus Fundacji na rzecz Nauki Polskiej.
  Okres realizacji: 2010-2013

• Szeregowanie online

  Kierownik: mgr Łukasz Jeż
  Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego.
  Okres realizacji: 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
  

• Algorytmy aproksymacyjne w warunkach niepewności

  Kierownik: dr Marcin Bieńkowski
  Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego.
  Okres realizacji: 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
  

• Sieci dynamiczne: eksploracja i zarządzanie danymi

  Kierownik: dr Marcin Bieńkowski
  Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego.
  Okres realizacji: 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
  

• Jeden krok od modelu relacyjnego. Kilka podstawowych zagadek baz danych

  Kierownik: prof. dr hab. Jerzy Marcinkowski

  Okres realizacji: 2017-2022

  Projekt finansowany przez Narodowe Centrum Nauki

• Logiki z uogólnionymi kwantyfikatorami zliczającymi dla programów operujących na danych i systemów bazodanowych

  Kierownik: Bartosz Bednarczyk

  Okres realizacji: 2018-2022

  Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

• Maszyny abstrakcyjne w implementacji języków programowania: podejście derywacyjne

  Kierownik: dr hab. Dariusz Biernacki

  Okres realizacji: 2021-2022

  Projekt badawczy finansowany przez Narodową Agencję Wymiany Akademickiej

• Automaty skończone: wybrane problemy i zastosowania łączące różne obszary badań

  Kierownik: dr Marek Szykuła

  Okres realizacji: 2022-2026

  Projekt badawczy finansowany przez Narodowe Centrum Nauki

• 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.