Relevant Seminars

RSS

Seminar Talk Announcement

  • Jan Onderka (Institute of Computer Science, Prague):

    Abstraction-Based Machine-Code Program Verification

    22.04.2025 13:30Room 318 (zoom) @ Institute of Computer Science
    Pod Vodárenskou věží 2
    Praha, 182 00
    Hora Informaticae

    Formal verification of programs in their binary machine-code representation can be used to prove or disprove low-level properties not verifiable using source code, such as correct manipulation of processor peripherals or the maximal used program stack size. While machine-code verification has been problematic due to the diversity of processor architectures and loss of higher-level information in machine code, I present a general verification solution based on model checking with an Input-based Three-valued Abstraction Refinement framework, applicable to arbitrary mu- calculus properties and digital systems expressible as Finite-State Machines. I introduce a free and open-source tool machine-check (https://machine-check.org) that instantiates the framework for Computation Tree Logic properties and digital systems described in a subset of the Rust programming language. We show and discuss its ability to verify properties of machine-code programs for the ATmega328P microcontroller, finding a previously unknown bug in one of the evaluated programs.

  • Václav Cenker (Palacky University in Olomouc):

    Free Algebras in Finitely Generated Varieties of Commutative BCK-Algebras

    23.04.2025 16:00Room 419 (zoom) @ Institute of Computer Science
    Pod Vodárenskou věží 2
    Praha, 182 00
    Applied Mathematical Logic Seminar

    In this talk, I will present a description of finitely generated free algebras in certain finitely generated varieties of commutative BCK-algebras. The construction relies on homomorphisms from free commutative BCK-algebras to free ŁBCK-algebras that extend the insertion of generators, allowing us to draw on existing results. A key step involves analyzing valuations and their equivalence classes, which leads to a precise count of the elements of the free algebras and a full structural characterization. In the final part of the talk, I will outline some ongoing work and open questions concerning the axiomatization of subvarieties of commutative BCK-algebras.

Past Talks