Szoftverek helyességének garantálását támogató módszereket vizsgálok. Ebbe a formális specifikációknak bizonyítottan megfelelő programok készítésének módszerei éppúgy beletartoznak, mint a programozási nyelvek tulajdonságainak, szemantikájának vizsgálata, a statikus forráskódelemzés (például hibák felderítésére), a szemantikamegőrző programtranszformációk. Különös figyelmet szánok a konkurens, párhuzamos és elosztott programozási paradigmákra.

Kutatócsoportunk a kvantuszámítógépek programozásának módszereit vizsgálja. Programozási nyelveket és programfejlesztési eszközöket tervezünk. Megalkottuk a Piquassot (piquasso.com), mely fotonikus kvantumszámítógépek egy szimulátora.