Static Analysis at Scale
Staatiline analüüs suurel skaalal
Techniques for concurrency, side effects, and sound program reasoning.
Meetodid konkurentsuse, kõrvalmõjude ja korrektse programmipõhjenduse jaoks.
Programming Languages · University of Tartu
Programmeerimiskeeled · Tartu Ülikool
Research Fellow focused on rigorous program analysis and trustworthy software. Teadur, kelle fookus on rangetel programmianalüüsi meetoditel ja usaldusväärsel tarkvaral.
I am a Research Fellow in Programming Languages at the Institute of Computer Science, University of Tartu. I work on static analysis and abstract interpretation, including Datalog and differential dataflow approaches.
Olen Tartu Ülikooli arvutiteaduse instituudi programmeerimiskeelte teadur. Tegelen staatilise analüüsi ja abstraktse interpretatsiooniga, sh Datalogi ja diferentsiaalse andmevoolu lähenemistega.
Open to collaboration
Avatud koostööle
Interested in program analysis, explainable verification, and proof assistants.
Huvitatud programmianalüüsist, selgitatavast verifitseerimisest ja tõestuskeskkondadest.
Research themes
Uurimisteemad
Static analysis and abstract interpretation for real-world systems.
Staatiline analüüs ja abstraktne interpretatsioon reaalsüsteemidele.
Datalog and differential dataflow for incremental analysis.
Datalog ja diferentsiaalne andmevoog inkrementaalseks analüüsiks.
Explainable verification and proof assistants (Rocq/Coq).
Selgitatav verifitseerimine ja tõestuskeskkonnad (Rocq/Coq).
Highlights
Esiletõstetud
What I work on
Millega tegelen
Datalog + Differential Dataflow
Datalog + diferentsiaalne andmevoog
Incremental program analysis via higher-order dataflow programs.
Inkrementaalne programmianalüüs kõrgema järgu andmevoolu programmidega.
Proof Assistants in Teaching
Tõestuskeskkonnad õppetöös
Interactive theorem proving and Rocq/Coq in the curriculum.
Interaktiivne teoreemitõestus ja Rocq/Coq õppekavas.
Projects
Projektid
Tools and systems
Tööriistad ja süsteemid
Goblint
Sound static analyzer for multithreaded C, developed in collaboration with TU Munich.
Korrektsust säilitav staatiline analüsaator mitmelõimelisele C‑le, koostöös TUM‑iga.
Põder
Java bytecode analyzer focused on explainable results.
Java baitkoodi analüsaator, mis rõhutab selgitavat tulemust.
Publications
Publikatsioonid
Publications
Publikatsioonid
2024 · Incremental Evaluation of Dynamic Datalog Programs as a Higher-order DBSP Program
2023 · On the Suitability of Differential Dataflow for Datalog Interpretation in Highly Dynamic Settings
2018 · Demand-driven interprocedural analysis for map-based abstract domains
2013 · How to combine widening and narrowing for non-monotonic systems of equations
Group
Rühm
Laboratory for Software Science
Software Science’i labor
I am part of the Laboratory for Software Science at the University of Tartu. The lab focuses on formal methods, type systems, and verifying system properties.
Kuulun Tartu Ülikooli Software Science’i laborisse. Labor keskendub formaalmeetoditele, tüübisüsteemidele ja süsteemiomaduste verifitseerimisele.
Explore the group, projects, and thesis topics on the lab site.
Loe rühma, projektide ja lõputööteemade kohta labori lehelt.