20.02.1975
Scopus Author ID 7005982452

Teenistuskäik

Töökohad ja ametid
01.03.2019–...   
Tallinna Tehnikaülikool, Infotehnoloogia teaduskond, Tarkvarateaduse instituut, Teadur (1,00)
2016–2018   
Data61 / CSIRO, Sydney, uurimisinsener (1,00)
2013–2014   
ICS AG, Stuttgart, arendusinsener (1,00)
2012–2013   
Critical Software SA, Coimbra, Järeldoktor (1,00)
2008–2010   
DFKI, Bremen, Teadur (1,00)
2003–2008   
Universität Bremen, Nooremteadur (1,00)
 
 
Haridustee
2003–2010   
Universität Bremen, doktorantuur arvutiteaduses
1997–2002   
Universität Bremen, diplomiõpingud arvutiteaduses

Kvalifikatsioon

Teadustöö põhisuunad
ETIS KLASSIFIKAATOR: 4. Loodusteadused ja tehnika; 4.6. Arvutiteadused; CERCS KLASSIFIKAATOR: P170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria); TÄPSUSTUS: tarkvara verifitseerimine, interaktiivsed teoreemitõestajad

Publikatsioonid

Klass
Aasta
Publikatsioon
 
3.1.
2018
3.1.
2017
1.2.
2016
1.2.
2016
2.3.
2010
3.1.
2010
1.2.
2006
3.1.
2004
29.01.2020
20.02.1975
Scopus Author ID 7005982452

Career

Institutions and positions
01.03.2019–...   
Tallinn University of Technology , School of Information Technologies, Department of Software Science, Researcher (1,00)
2016–2018   
Data61 / CSIRO, Sydney, research engineer (1,00)
2013–2014   
ICS AG, Stuttgart, development engineer (1,00)
2012–2013   
Critical Software SA, Coimbra, Post-Doc (1,00)
2008–2010   
DFKI, Bremen, Researcher (1,00)
2003–2008   
Universität Bremen, Junior Researcher (1,00)
 
 
Education
2003–2010   
Universität Bremen, PhD studies in computer science
1997–2002   
Universität Bremen, diploma studies in computer science

Qualifications

Fields of research
ETIS CLASSIFICATION: 4. Natural Sciences and Engineering; 4.6. Computer Sciences; CERCS CLASSIFICATION: P170 Computer science, numerical analysis, systems, control ; SPECIFICATION: software verification, interactive theorem provers

Publications

Category
Year
Publication
 
3.1.
2018
3.1.
2017
1.2.
2016
1.2.
2016
2.3.
2010
3.1.
2010
1.2.
2006
3.1.
2004
29.01.2020
  • Leitud 8 kirjet
PublikatsioonAutoridAastaVäljaande pealkiriKlassifikaatorFailAsutused
Towards verifying Ethereum smart contract bytecode in Isabelle/HOLAmani, Sidney; Bégel, Myriam; Bortin, Maksym; Staples, Mark2018Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 20183.1.
COMPLX: a verification framework for concurrent imperative programsAmani, Sidney; Andronick, June; Bortin, Maksym; Lewis, Corey; Rizkallah, Christine; Tuong, Joseph2017CPP '17 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, January 16-17, 2017, Paris, France3.1.
A formalisation of the Cocke-Younger-Kasami algorithmBortin, Maksym2016Archive of Formal Proofs1.2.Tallinna Tehnikaülikool, Infotehnoloogia teaduskond, Tarkvarateaduse instituut
Complx: a verification framework for concurrent imperative programsAmani, Sidney; Andronick, June; Bortin, Maksym; Lewis, Corey; Rizkallah, Christine; Tuong, Joseph2016Archive of Formal Proofs1.2.Tallinna Tehnikaülikool, Infotehnoloogia teaduskond, Tarkvarateaduse instituut
An approach to the extension of a theorem prover by advanced structuring mechanismsBortin, Maksym20102.3.
Structured formal development with quotient types in Isabelle/HOLBortin, Maksym; Lüth, Christoph2010Intelligent Computer Mathematics : 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010 and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010, Proceedings3.1.
Structured formal development in IsabelleBortin, Maksym; Johnsen, Einar Broch; Lüth, Christoph2006Nordic Journal of Computing1.2.
A first step towards formal verification of security policy properties for RBACDrouineaud, Michael; Bortin, Maksym; Torrini, Paolo; Sohr, Karsten2004Proceedings Fourth International Conference onQuality Software, QSIC 2004 : 8-10 September 2004 Braunshweig, Germany3.1.