Bug Online

Matko Botinčan je mlad momak, ima 29 godina i većinu je svog života proveo u Zagrebu. Nakon osnovne škole pohađao je XV. matematičku gimnaziju (popularni MIOC), a već je i sâm izbor razreda (program matematičke gimnazije s dodatno pojačanom matematikom) dao naslutiti kamo će ga kasnije odvesti životni put. I zaista - Matko je diplomirao i magistrirao na matematičkom odjelu zagrebačkog PMF-a, a upravo se nalazi na doktorskom studiju u Cambridgeu, gdje se našao zahvaljujući zakladi Billa Gatesa. Kako je uspio osvojiti stipendiju, na kojim je projektima do sada radio i kako se gledaju informatički biznis i znanost, pročitajte na narednim stranicama

Kada si otkrio posebno zanimanje za matematiku?

Mislim da je to bilo negdje već u prvim razredima osnovne škole; fascinirao me proces računanja i kako je na različite načine moguće doći do jednakih odgovora na ista matematička pitanja. Također se sjećam kako me se posebno dojmila legenda o nastanku šaha.

Jesi ikad pomislio da bi išao studirati išta osim matematike?

Osim matematike jako me je zanimalo i računarstvo te sam se htio na studiju baviti objema disciplinama. Tako da je u obzir dolazio PMF - matematički odjel, smjer računarstvo - i FER. Jedan poznanik, profesor s FER-a, iskreno mi je rekao: FER te nauci praktičnim stvarima, PMF te nauci razmišljati. Nekako mi je bio veći izazov ovo drugo. Naravno, tijekom vremena iskristalizirali su se interesi i za neka sasvim područja - npr. ekonomija i socijalna psihologija. Tako da se u slobodno vrijeme pokušavam samoeducirati i u tom smjeru.

Nakon studija, ostao si na PMF-u kao znanstveni novak?

Nakon diplome zaposlio sam se na PMF-MO kao znanstveni novak s ciljem završavanja poslijediplomskog studija iz matematike. Tijekom rada na magisteriju, koji je bio iz područja teorijskog računalstva, shvatio sam da bih se u daljnjem znanstvenom radu definitivno želio baviti područjem računalstva koje se tiče formalne verifikacije softvera. Ono ima vrlo duboke temelje u teorijskom računalstvu, ali sve stvari koje se razvijaju u teoriji implementiraju se i u obliku konkretnih alata. Budući da u Hrvatskoj zapravo nema znanstvenika koji se bave tim područjem, bilo je potrebno povezati se s ljudima izvan Hrvatske. Tako sam negdje nakon magisterija polako prelazio iz standardne paradigme rada na fakultetu i započeo s boravcima u inozemstvu.

Što je to formalna verifikacija softvera?

Verifikacija softvera odnosi se na područje softverskog inženjerstva u kojem je cilj na neki način osigurati - ili, idealno, dokazati - da softverski produkt u potpunosti zadovoljava danu specifikaciju. Formalna verifikacija koristi rigorozne matematički bazirane metode kako bi formalno dokazala da softver zadovoljava danu, formalno zapisanu specifikaciju. Zapravo, ako se gleda malo šire, postoje dva generalna pristupa u formalnoj verifikaciji softvera. Jedan je baziran na transformaciji izvornog kôda softvera u niz matematičkih formula gdje se sve tvrdnje o odnosu specifikacije i implementacije iskazuju u terminima teorema koje onda provjeravaju (automatski) dokazivači teorema. Drugi je tzv. model checking u kojem se provodi eksploracija modela softvera s ciljem da se utvrdi da sva stanja danog modela zadovoljavaju neka formalno zadana svojstva.

Zatim si boravio neko vrijeme u Njemačkoj? Na čemu si tamo radio?

Boravio sam oko pola godina na RWTH Aachen u Njemačkoj, u grupi koja se bavi matematičkim osnovama računalstva. U Njemačkoj sam boravio još kao zaposlenik PMF-a, bila je riječ o klasičnom studijskom boravku. Ondje sam se bavio jednim posebnim tipom model checking problema i njegovim rješavanjem s pomoću kombinatornih igara. No pristup se u praksi pokazao neefikasnim, tako da nisam dalje nastavljao rad u tom području.

Što znači da je pristup neefikasan?                     

Neefikasan ovdje znači da su pripadni algoritmi imali preveliku računsku složenost da bi se mogli aplicirati na imalo kompleksnije modele ili specifikacije.