Fedor Shmarov

Email: fedor.shmarov@manchester.ac.uk
Address: 2.62 Kilburn Building, Oxford Road, Manchester, M13 9PL
Web: www.shmarov.com

Personal profile

I am an enthusiastic and motivated researcher currently involved in the SCorCH project where I work on developing tools and techniques for formal verification of software for capability hardware. I also have a strong background in mathematical modelling, model checking and formal verification of stochastic hybrid systems.

Work experience

December 2020 - present - The University of Manchester, Department of Computer Science
Position: Research Associate
Project title: SCorCH: Secure Code for Capability Hardware
Responsibilities: Development of novel techniques for verifying C/C++ programs for CHERI capability hardware
October 2017 - November 2020 - Newcastle University, School of Computing
Position: Research Assistant/Associate
Project title: Personalised ultraviolet B (UVB) treatment of psoriasis through biomarker integration with computational modelling of psoriatic plaque resolution
Responsibilities: Computational modelling of psoriasis onset, flare and clearance, analysis of clinical data

Education and qualifications

September 2013 - January 2018 - Newcastle University, School of Computing Science
Degree: PhD in Computing Science
Thesis title: Probabilistic Bounded Reachability for Stochastic Hybrid Systems
Supervisor: Dr Paolo Zuliani
Summary: I developed novel SMT-based methods combining formal verification techniques and statistical model checking for probabilistic reachability analysis of stochastic parametric hybrid systems. I implemented these methods in the tool called ProbReach
September 2012 - September 2013 - Newcastle University, School of Computing Science
Degree: MSc (with Distinction) in Advanced Computing Science
Awards: Philip Merlin prize presented by the School of Computing Science for the Best MSc Dissertation in the School
September 2007 - June 2011 - Tambov State Technical University, Department of Information Technologies
Degree: BSc (with Honours) in Information Science and Computer Technology

Publications

Journals

  • F. K. Aljaafari, R. Menezes, E. Manino, F. Shmarov, M. A. Mustafa, L. C. Cordeiro, "Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs", IEEE Access, vol. 10, pp. 121365-121384, 2022.
  • F. Shmarov, G. R. Smith, S. C. Weatherhead, N. J. Reynolds, P. Zuliani, "Individualised computational modelling of immune mediated disease onset, flare and clearance in psoriasis", PLoS Computational Biology 18 (9), e1010267, 2022.
  • N. Watson, N. Wilson, F. Shmarov, P. Zuliani, N. J. Reynolds, S. C. Weatherhead, "The use of psoriasis biomarkers, including trajectory of clinical response, to predict clearance and remission duration to UVB phototherapy", J Eur Acad Dermatol Venereol, 35: 2250-2258, 2021.
  • F. Shmarov, S. Soudjani, N. Paoletti, E. Bartocci, S. Lin, S. A. Smolka, P. Zuliani, "Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems", IEEE Access, vol. 8, pp. 180825-180843, 2020.

Conferences and Workshops

  • K. Alshmrany, A. Bhayat, F. Brauße, L. C. Cordeiro, K. Korovin, T. Melham, M. A. Mustafa, P. Olivier, G. Reger, F. Shmarov, "Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities", in IEEE Secure Development Conference (SecDev 2022), Atlanta, GA, USA, pp. 52-58, 2022.
  • F. Brauße, F. Shmarov, R. Menezes, M. R. Gadelha, K. Korovin, G. Reger, L. C. Cordeiro, "ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC", in Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2022), pp 773–776, 2022.
  • A. Abate, H. Blom, M. Bouissou, N. Cauchi, H. Chraibi, J. Delicaris, S. Haesaert, A. Hartmanns, M. Khaled, A. Lavaei, H. Ma, K. Mallik, M. Niehage, A. Remke, S. Schupp, F. Shmarov, S. Soudjani, A. Thorpe, V. Turcuman, P. Zuliani, "ARCH-COMP21 Category Report: Stochastic Models", in Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 21), vol. 80, pp. 55-89, 2021.
  • M. Vasileva, F. Shmarov, P. Zuliani, "Probabilistic Reachability for Uncertain Stochastic Hybrid Systems via Gaussian Processes", in 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2020), Jaipur, India, pp. 1-11, 2020.
  • A. Abate, H. Blom, N. Cauchi, J. Delicaris, A. Hartmanns, M. Khaled, A. Lavaei, C. Pilch, A. Remke, S. Schupp, F. Shmarov, S. Soudjani, A.P. Vinod, B. Wooding, M. Zamani, P. Zuliani, "ARCH-COMP20 Category Report: Stochastic Models", in Proceedings of the 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 20), vol. 74, pp. 76-106, 2020.
  • F. Shmarov, N. Paoletti, E. Bartocci, S. Lin, S. Smolka, P. Zuliani, "SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems", in Proceedings of the 13th International Haifa Verification Conference (HVC 2017), pp. 131–146, 2017.
  • F. Shmarov, P. Zuliani, "Probabilistic Hybrid Systems Verification via SMT and Monte Carlo Techniques", in Proceedings of the 12th International Haifa Verification Conference (HVC 2016), LNCS, vol. 10028, pp. 152–168, 2016.
  • F. Shmarov, P. Zuliani, "SMT-based Reasoning for Uncertain Hybrid Domains", in AAAI16 Workshop on Planning for Hybrid Systems, 30th AAAI Conference on Artificial Intelligence (PlanHS 2016), pp. 624–630, 2016
  • C. Madsen, F. Shmarov, P. Zuliani, "BioPSy: an SMT-based Tool for Guaranteed Parameter Set Synthesis of Biological Models", in Computational Methods in Systems Biology (CMSB 2015), ser. LNCS, vol. 9308, pp. 182–194, 2015.
  • F. Shmarov, P. Zuliani, "ProbReach: a Tool for Guaranteed Reachability Analysis of Stochastic Parametric Hybrid Systems", in 1st International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2015), ser. EPiC Series in Computing, S. Bogomolov and A. Tiwari, Eds., vol. 37, pp. 40–48, 2015.
  • F. Shmarov, P. Zuliani, "ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Parametric Hybrid Systems", in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015). ACM, pp. 134–139, 2015.

Presentations and posters

  • F. Shmarov, P. Zuliani, G. Smith, N. Reynolds, "A Mechanistic Model of Psoriatic Epidermis and Psoriasis Therapies", Poster session at MRC PSORT consortium showcase, 2019.
  • F. Shmarov, "Probabilistic Bounded Reachability for Stochastic Hybrid Systems", Third Workshop on Design and Analysis of Robust Systems (DARS), 2018.
  • F. Shmarov, P. Zuliani, "ProbReach: Probabilistic Bounded Reachability for Uncertain Hybrid Systems", International Workshop on Formal Methods for Rigorous Systems Engineering of Cyber-Physical Systems (RiSE4CPS), 2017.
  • F. Shmarov, "Stochastic Hybrid Systems: Modelling Cancer and Psoriasis", International Workshop on Automated Reasoning for Systems Biology and Medicine (ARSBM), 2016.

Teaching and supervision

  • As Research Associate I have co-supervised 1 BSc student (who implemented an extension to my tool ProbReach as a part of the final project) and 6 Bioinformatics MSc students.
  • As PhD student I demonstrated and marked assignments for 6 different BSc and MSc modules in the School of Computing at Newcastle University:
    • CSC1021 “Programming I”,
    • CSC8105 “System Validation”,
    • CSC3324 “Understanding Concurrency”,
    • CSC1025 “Mathematics for Computer Science”,
    • CSC8317 “Introductory Programming for Biologists”,
    • CSC1024 “Computer Architecture”.

Technical skills

  • Formal Verification, Bounded Model Checking, Machine Learning, Artificial Intelligence, Mathematical Modelling
  • C/C++, Java, Python, R, MATLAB, SQL, Git, AWS, HPC
  • Linux, Windows, OS X

Software tools

  • ESBMC (https://github.com/esbmc/esbmc) - context-bounded model checker for verifying single- and multithreaded C/C++, Kotlin, and Solidity programs.
    Role: contributor
    Language: C/C++
  • ProbReach (https://github.com/dreal/probreach) - tool for formal and statistical verification of stochastic parametric hybrid systems.
    Role: lead developer and maintainer
    Language: C/C++
  • BioPSy (https://github.com/dreal/biology) - tool for parameter set synthesis in dynamical systems.
    Role: co-developer
    Language: C/C++, Java
  • System for area planning (https://github.com/shmarovfedor/area-planning) - tool for maximising the construction profit for a predefined region (MSc project).
    Role: sole developer
    Language: Java

Personal skills

  • Experienced public speaker and presenter
  • Ability to work in a team
  • Supervisory skills
  • Languages: English (fluent), Russian (native)