Research
Teadus
Sound methods for analyzing real-world programs with concurrency and side effects.
Korrektsete meetodite loomine reaalsete programmide analüüsiks (konkurentsus, kõrvalmõjud).
Incremental evaluation techniques for Datalog-based analysis pipelines.
Inkrementaalsed hindamismeetodid Datalogil põhinevatele analüüsitorudele.
Bringing analysis results closer to developers via explainable reporting.
Analüüsi tulemuste selgitamine arendajale arusaadaval kujul.
Interactive theorem proving with Rocq/Coq in teaching and research.
Interaktiivne teoreemitõestus Rocq/Coq keskkondades.
Projects
Projektid
A sound static analyzer for multithreaded C, developed in collaboration with Technical University of Munich.
Korrektsust säilitav staatiline analüsaator mitmelõimelisele C‑le, loodud koostöös Müncheni Tehnikaülikooliga.
Java bytecode analyzer with explainable, developer-friendly results.
Java baitkoodi analüsaator, mille tulemused on arendajale selgitatavad.
Funding
Rahastus