F(r)oggy reflections

A personal page of Jan Tušil

Selected projects

Here is a list of selected projects of mine, in no particular order.

Formal Semantics of C++ Subsets (2017-2018)

Developed a formal model of subsets of C++14, successfully identifying previously-unknown compiler bugs in state-of-the-art compilers, as well as a logical contradiction in the C++14 standard and subsequent drafts.

  • Tools K-framework, drafts of C++ standard documents, GCC, Clang
  • Recognition Awarded the Faculty Dean’s Prize for Outstanding Master’s Thesis
  • Status Historical research project
  • References
  • Tags C++

A formally verified programming languages framework (2024-??)

I designed, implemented, and formally verified a semantics-based programming language framework, named Minuska. The framework is intended as an alternative to K-framework, providing higher correctness guarantees (full formall verification with the exception of the user interface), higher performance, and simpler understandability, all powered by cleaned-up theory. The theory is a joint work with Jan Obdrzalek (MU) with occasional input from Traian Serbanuta (UNIBUC); the implementation is mostly mine, with a contribution from Michal Louda (MU), whom I have supervised for his Bachelor’ thesis.

A logic for security properties of programs in arbitrary deterministic programming languages (2022-2023)

Designed a universal logic for verifying security properties (such as noninterference) in arbitrary deterministic programming languages. Technically, the logic allows reasoning about the class of k-safety hyperproperties of software programs, and it has been formally proven to work (be sound and relatively complete) with any deterministic programming language, assuming that an operational model of the language is provided. The logic subsumes and simplifies existing hyperproperty logic known as Cartesian Hoare Logic, and extends a language-parametric logic for safety properties known as Reachability Logic, and hence was given the name “Cartesian Reachability Logic”. This work was done in collaboration with Traian Serbanuta (UNIBUC) and Jan Obdrzalek (MU).

  • Output Formal logic (syntax, semantics, proof system), mathematical proofs, examples
  • Publication LPAR'23
  • Status Core logic and proofs completed. Ready for immediate engineering implementation, for which multiple approaches are possible:
    • Implementation style: pragmatic (Rust, OCaml, …) vs fully verified (Rocq)
    • Scope: single proprietary language vs multi-language support
    • Automation level: deductive verification requiring manual invariants vs. semi-automated workflows
  • Tags security, programming-languages

Interactive theorem proving environment for a niche logic (2021-2023)

Implemented an interactive environment for matching logic within a general-purpose proof assistant (Rocq). This project initially started with the goal of connecting the K-framework tool to a proof assistant. Matching logic itself is quite niche; however, it has been used as a foundation for mentioned K-framework. One of the main goals was to make development of proofs in matching logic concise and machine-assisted. To this end, the implemenation uses a novel proof calculus in the style of natural deduction. This work is a collaboration with Peter Bereczky (ELTE) and Daniel Horpacsi (ELTE), who continue the development of the project with Kurucz Ádám, and builds on our former work done jointly with Xiaohon Chen (UIUC), Lucas Pena (UIUC), and Tamas Balint Mizsei (ELTE).