Diplomovou práci svým zadáním považuji za obtížnou. Jedná se o pilotní práci ve směru, kterému se ve výzkumné skupině VeriFIT plánujeme věnovat--analýze přístupových politik založenou na SMT solvingu. Jednalo se o výzkumnější práci u které předem nebylo zcela jasné, na jaké problémy se narazí. Přestože problémů nebylo málo, podařilo se vytvořit kvalitní práci, která zásadním způsobem přispívá k analýze přístupových politik. 

Student se ve své práci významně podílel na vývoji nástroje pro analýzu Rego politik vyvýjenou ve spolupráci se skupinou VeriFIT. Je v plánu připravit článek, který zahrnuje studentovu práci, a poslat jej na prestižní konferenci. 

Student během semestru docházel na pravidelné schůzky. Aktivně přicházel s nápady, které si experimentálně ověřoval a řešil nejrůznější technické problémy, které se po cestě objevily. Na schůzky chodil připraven. Co se týče aktivity během řešení, nemám co vytknout.

Evaluation level: zadání splněno

Požadavky byly splněny.

Technická zpráva má logickou strukturu: nejdříve je zaveden jazyk Rego, potom je formálně definována jeho sémantika a pak následuje typový systém a algoritmus pro typovou inferenci. V další části je definován převod do SMT a následuje návrh dvou analýz (pro kolize a subsumpce) pro Rego politiky. Dále následuje popis implementace a experimentální vyhodnocení. Práce je pochopitelná, byť z důvodu své formálnější povahy vyžaduje při četbě vyšší míru soustředění.

Práce cituje relevantní literaturu, a to jak průmyslové zdroje (stránky pro technologii OPA), tak i vědecké práce (zabývající se, např., formalizacemi specifikačních jazyků, SMT solvery, atp.). Citace jsou v pořádku.

Práce je jedním ze základů nástroje, který cílí na usuzování o Rego politikách v použití v průmyslové sféře. Tento nástroj ještě neexistuje, ale má již nyní velmi dobrý základ, na kterém lze dále stavět. Dále by bylo dobré práci (po dokončení) zkusit publikovat jako vědecký článek.