A First Step Towards Formal Verification of Security Policy Properties for RBAC. - Michael Drouineaud; Maksym Bortin; Paolo Torrini; Karsten Sohr (QSIC, 2004)

Structured Formal Development in Isabelle. - Maksym Bortin; Einar Broch Johnsen; Christoph Lüth (Nord. J. Comput., 2006)

Structured Formal Development with Quotient Types in Isabelle/HOL. - Maksym Bortin; Christoph Lüth (AISC/MKM/Calculemus, 2010)

An approach to the extension of a theorem prover by advanced structuring mechanisms. - Maksym Bortin (2010)

COMPLX: A Verification Framework for Concurrent Imperative Programs. - Sidney Amani; June Andronick; Maksym Bortin; Corey Lewis; Christine Rizkallah; Joseph Tuong (Arch. Formal Proofs, 2016)

A formalisation of the Cocke-Younger-Kasami algorithm. - Maksym Bortin (Arch. Formal Proofs, 2016)

Towards verifying ethereum smart contract bytecode in Isabelle/HOL. - Sidney Amani; Myriam Bégel; Maksym Bortin; Mark Staples (CPP, 2018)

A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs. - Maksym Bortin (CoRR, 2020)

Synthesis of Implementations for Divide-and-Conquer Specifications. - Maksym Bortin (SBMF, 2022)

From THE BOOK: Two Squares via Involutions. - Maksym Bortin (Arch. Formal Proofs, 2022)

Structured development of implementations for divide-and-conquer specifications. - Maksym Bortin (Sci. Comput. Program., 2024)