Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze

Plan referatów/Talks schedule

Lista referatów

  • 2022-03-25, godz. 12:15, on-line

    Paweł Urzyczyn (MIMUW)

    Duality between Unprovability and Provability in Forward

    The speaker will talk about the paper Camillo Fiorentini, Mauro Ferrari: Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic. ACM Trans. Comput. Log. 21(3): 22:1-22:47 (2020), where a system is defined to derive refutation...

  • 2022-03-11, godz. 12:15, 5820

    Aleksy Schubert (MIMUW)

    Ethereum vulnerabilities

    Ethereum vulnerabilities   Ethereum is an open decentralised platform based upon peer-to-peer network principles. It enables the possibility to deploy decentralised applications that run on the platform and manage  the resources of financial kind available on the platform. I wil...

  • 2022-03-11, godz. 12:15, 5820

    Aleksy Schubert

    Ethereum vulnerabilities

    Szanowni Państwo, jeszcze jeden dodatek, referat p.t. Ethereum vulnerabilities - jak wszystkie referaty tego seminarium do odwołania - będzie on-line pod linkiem Pozdrawiam, Aleksy Schubert ...

  • 2022-01-28, godz. 12:15, 5820

    Konrad Zdanowski (Cardinal Stefan Wyszynski University)

    Intuitionistic SAT solver

    I will present an article by F. Besson, Itauto: An Extensible Intuitionistic SAT Solver, which was presented at the conference Interactive Theorem Proving, ITP 2021 (url: ). The author presents an implementation of an intuitionistic ...

  • 2022-01-21, godz. 12:15, 5820

    Aleksy Schubert (MIMUW)

    Prenex fragment of first-order intuitionistic logic and word unification

    I will recall an old result by Gurevich and Voronkov connecting the monadic case in the prenex intuitionistic predicate logic with equality with word unification. ...

  • 2021-12-03, godz. 12:15, 5820

    Marcin Benke (MIMUW)

    (E)TiML: A Functional Language for Practical Complexity Analysis (for Ethereum)

    TiML is a variant of ML whose types contain resource bounds, designed by Peng Wang as his PhD thesis on MIT. When a TiML program passes the typechecking, upper bounds on its resource usage can be guaranteed. One interesting application (or rather extension) of this language is using it for Ethereum...

  • 2021-11-26, godz. 12:15, 5820

    Aleksy Schubert (MIMUW)

    Verification of Ethereum programs

    The general overview of blockchain and smart contract technologies is given. Based upon that a state-of-the art verification technique VerX is discussed.   You can join the meeting under the Zoom link: ...

  • 2021-11-19, godz. 12:15, 5820

    Maciej Zielenkiewicz (MIMUW)

    Small model property reflects in games and automata

    Let's choose a logic theory having the small model property. I will show that the size of the small model used in the definition of the property can be directly used to show a limit on the number of maximal variables 1n an Aphrodite strategy in games for finding a proof. On the other hand I'll show ...

  • 2021-11-05, godz. 12:15, 5820

    Jacek Chrząszcz (MIMUW)

    Cameleer: a Deductive Verification Tool for OCaml

    Despite all the advances in deductive verification and proof automation over the past few decades, little attention has been given to the family of functional languages. We present Cameleer, a tool for the deductive verification of programs written in OCaml, with a clear focus on proof automa...

  • 2021-10-29, godz. 12:15, 5820

    Aleksy Schubert (MIMUW)

    NP-completeness of BCI - another view

    Another proof of NP-hardness of provability in BCI is presented. As a more natural source of the reduction, the one-in-three 3SAT problem is assumed. ...