Fedor Shmarov

Email: fedor.shmarov@newcastle.ac.uk
Address: Urban Sciences Building, 1 Science Square, Newcastle upon Tyne, NE4 5TG
Web: www.shmarov.com

Personal profile

I am an experienced and enthusiastic researcher currently working on the SCorCH project at the University of Manchester where I am developing tools and techniques for formal verification of software for capability hardware. I also have strong background in computational modelling, model checking and formal verification of stochastic hybrid systems.

Work experience

September 2023 - present - Newcastle University, School of Computing
Position: Lecturer
December 2020 - September 2023 - 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

  1. 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.
  2. 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.
  3. 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.
  4. 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.

    5. Conferences and Workshops

  5. F. K. Aljaafari, F. Shmarov, E. Manino, R. Menezes, L. C. Cordeiro, "EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution)", In 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), (accepted/in press), 2023.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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
  14. 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.
  15. 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.
  16. 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

Academic Conferences

Teaching and supervision

Software projects

Technical skills

Personal skills