Labor on moodustatud loogika ja semantika ning formaalmeetodide rühmadest (juhid Tarmo Uustalu ja Jüri Vain), uurib tugevalt tagatud tarkvara arendamise teooriaid, meetodeid ja tööriistu, spetsialiseerudes nii tõestustele (sertifitseeritud tarkvara) kui ka testimisele.
Viimastel aastatel on eraldi uurimisvaldkonnaks kujunenud rakenduslik masinõpe (juht Sven Nõmm).
formaliseeritud programmeerimisteooria, funktsionaalne ja sõltuvalt tüübitud programmeerimine, tarkvara verifitseerimine ja testimine
