Category Archives: Uncategorized

A formal grammar for Magic: the Gathering

I wrote an ANTLR4 formal grammar for Magic: the Gathering cards.

It turns this

A Magic: the Gathering card

Or, more specifically, it turns this

Undergrowth — When you cast this spell, reveal the top X cards of your library, where X is the number of creature cards in your graveyard. You may put a green permanent card with converted mana cost X or less from among them onto the battlefield. Put the rest on the bottom of your library in a random order.

Into this:

You can try it out here: and you can download the grammar and the source code from

Read more »

Magisterské státnice na Matfyzu

For the sake of viewer convenience, the content is shown below in the alternative language. You may click the link to switch the active language.

Tento článek popisuje, jak fungovala ústní magisterská státní zkouška z informatiky na Matematicko-fyzikální fakultě Univerzity Karlovy (MFF, Matfyz) v září 2017. (verze v Google dokumentu)


Magisterská státnice se nazývá “ústní část státní závěrečné zkoušky”. Žádná písemná část neexistuje. Slovo “ústní” ji pouze rozlišuje od “obhajoby diplomky,” což je druhá část zkoušky. Není dělená na několik zkoušek podle předmětu (matematika/informatika) na rozdíl od bakalářské zkoušky. Na zkoušku je třeba se přihlásit před termínem uvedeným v harmonogramu, ale nelze se přihlásit dříve, než máte splněné všechny ostatní studijní povinnosti vyjma diplomové práce.

Read more »

Java Pathfinder Inspector

In the summer of 2016, I participated in the Google Summer of Code program, during which I updated and significantly improved the Java Pathfinder Inspector.

Java Pathfinder (JPF) is a framework for formal checking of Java programs. Its core consists of a virtual machine for Java bytecode, running itself on Java; this allows JPF to instrument the code and provide its own functionality for critical instructions. JPF is very extensible and many modules exist for various kinds of verification such as symbolic execution. JPF Inspector is one such JPF module that focuses on debugging capability.

JPF Inspector is a tool for inspection and control of Java Pathfinder execution. It supports breakpoints and single-step execution (forward and backward) at different levels of granularity, and it allows the user to examine and modify program state (threads, call stacks, and heap objects). Unlike with standard debuggers (GDB), it is also possible to control thread scheduling explicitly.

This is the first software engineering project for which I received actual money.

It is programmed in Java.

It was created at the age of 23, in 2016.


Read more »