You are not logged in | Log in
Return to the list of seminars

Seminar Semantics, Logic, Verification and its Applications

Weekly research seminar


Organizers

Information

Fridays, 12:15 p.m. , room: 5820

Research fields

List of talks

  • May 27, 2022, 12:15 p.m.
    Konrad Zdanowski (UKSW)
    Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter
    Zostanie przedstawiona praca panów Rybakov i Shaktov, pt. Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter pokazująca nierozstrzygalność logik modalnych i intuicjonistycznych z dwoma zmiennymi i jednym unarnym …

  • May 20, 2022, 12:15 p.m.
    Aleksy Schubert (MIMUW)
    On word unification in Coq
    W trakcie referatu przedstawiony zostanie szkic dowodu poprawności podstawowych własności algorytmu znajdowania unifikatorów na słowach oraz zakres jego formalizacji w Coq-u. A sketch of algorithm correctness for an algorithm to solve word unification problem will …

  • May 13, 2022, 12:15 p.m.
    Marcin Benke (MIMUW)
    Theorem Proving for All
    Jedną z istotnych zalet czystych języków funkcyjnych, takich jak Haskell jest możliwość równościowego wnioskowania o programach. Jednakże do tej pory takie wnioskowanie miało charakter zewnętrzny względem programu: już to (najczęściej) ręcznie „na papierze”, już to …

  • March 25, 2022, 12:15 p.m.
    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 …

  • March 25, 2022, 12:15 p.m.
    Jacek Chrząszcz (MIMUW)
    News in Coq
    Na referacie przedstawione zostaną ostatnie dodatki do narzędzia do dowodzenia twierdzeń Coq.

  • March 11, 2022, 12:15 p.m.
    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 meet.google.com/xiq-ruco-ayy Pozdrawiam, Aleksy Schubert

  • March 11, 2022, 12:15 p.m.
    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 …

  • Jan. 28, 2022, 12:15 p.m.
    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: https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13904 ). The author presents an implementation of an …

  • Jan. 21, 2022, 12:15 p.m.
    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.

  • Dec. 3, 2021, 12:15 p.m.
    Marcin Benke (MIMUW)
    E)TiML: A Functional Language for Practical Complexity Analysis
    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 …

  • Nov. 26, 2021, 12:15 p.m.
    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: https://us02web.zoom.us/j/83143002443?pwd=dnlSQ05pVjB3L3cwSUkzOEVOTnJVUT09

  • Nov. 19, 2021, 12:15 p.m.
    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 …

  • Nov. 5, 2021, 12:15 p.m.
    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 …

  • Oct. 29, 2021, 12:15 p.m.
    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.

  • Oct. 22, 2021, 12:15 p.m.
    Paweł Urzyczyn (MIMUW)
    NP-completeness of BCI
    We will see a proof of NP-completness of propositional implicational logic BCI, in which each assumption is used exactly once.