Implementation of Approximation Algorithms for the Max-Min Resource Sharing Problem. - Mihhail Aizatulin; Florian Diedrich; Klaus Jansen (WEA, 2006)

Computationally Sound Analysis of a Probabilistic Contract Signing Protocol. - Mihhail Aizatulin; Henning Schnoor; Thomas Wilke (ESORICS, 2009)

Extracting and verifying cryptographic models from C protocol code by symbolic execution. - Mihhail Aizatulin; Andrew D. Gordon 001; Jan Jürjens (CCS, 2011)

Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. - Mihhail Aizatulin; François Dupressoir; Andrew D. Gordon 001; Jan Jürjens (Formal Aspects in Security and Trust, 2011)

Computational verification of C protocol implementations by symbolic execution. - Mihhail Aizatulin; Andrew D. Gordon 001; Jan Jürjens (CCS, 2012)

A model-learner pattern for bayesian reasoning. - Andrew D. Gordon 001; Mihhail Aizatulin; Johannes Borgström; Guillaume Claret; Thore Graepel; Aditya V. Nori; Sriram K. Rajamani; Claudio V. Russo (POPL, 2013)

Verifying cryptographic security implementations in C using automated model extraction. - Mihhail Aizatulin (2015)

Verifying Cryptographic Security Implementations in C Using Automated Model Extraction. - Mihhail Aizatulin (CoRR, 2020)