I am a PhD student (FNP MPD Programme) and research assistant at ICS PAS. Most of my research concerns parametric model checking, i.e., an approach where the investigated models and properties are allowed to contain missing fragments. The general goal is to effectively synthesise at least some of these parameters; see my Publications list for more on that.

Here is a link to a simple parametric symbolic model checker I wrote: SPATULA. Another prototype tool that translates from parametric timed automata to CVC3-type SMT formulae is here: PTA2SMT.

I work under supervision of Prof. Wojciech Penczek.

My background is Mathematics and Computer Science in Robotics. I like both the theoretical and applied side of my work, and prefer to think of myself as an engineer with some math skills.

I am always open to exciting opportunities from the industry and research community. It might sound cliché, but I do try to stay hungry, stay foolish, and love learning new things. 

Please find here the package with my PhD thesis and accompanying software (SPATULA, PTA2SMT, and MCMAS-Parametric).


Contact info:

Michał Knapik, ICS PAS, ul. Jana Kazimierza 5, 01-248 Warszawa, Poland

email: Michal.Knapik@LARCH.ipipan.waw.pl (remove the tree part!)

Powered by CMSimple_XH | Login