Resume

Reza Soltani - Formal Methods Researcher

PhD candidate in formal methods working on safety-security co-analysis for cyber-physical systems. My research combines attack-fault-defense modelling, statistical model checking, and quantitative optimisation across smart grids, satellite missions, research reactors, and flexible production lines.

Research Profile

  • Safety-security co-analysis for cyber-physical systems
  • Attack-fault-defense and attack-defense trees
  • Statistical model checking and game-theoretic optimization
  • Model checking with UPPAAL SMC/Stratego, PRISM, and CPN Tools
  • Reliability modelling for grid, satellite, and reactor case studies

Academic Snapshot

Current profile highlights reflected in the latest CV.

  • Expected PhD completion: Aug 2026.
  • Research output: 10 conference papers or accepted conference papers, 3 journal papers, and 3 preprints.
  • Includes 2 A-ranked ICORE/CORE conference papers: DSN 2025 and CSF 2026 (accepted).
  • Google Scholar snapshot (30 Apr 2026): 63 citations, h-index 5, i10-index 2.
  • Teaching at the University of Twente: 200 hours, including 110 hours in Software Testing and Risk Assessment.
  • Co-supervised 3 MSc theses and 2 BSc theses; all listed MSc theses were completed.

Research Interests

Core themes, domains, and methods that define the current research profile.

Formal methodsSafety-security co-analysisAttack-fault-defense treesDependable cyber-physical systemsSmart gridsSatellite missions

Research Secondments

International, domain-facing work with local researchers and industry partners.

22 Jun - 20 Jul 2024 · Rio Cuarto, Argentina

National University of Rio Cuarto / INVAP SE

Visiting Researcher

  • Optimized spare-part strategies for research reactors with statistical model checking.
  • Worked with industry engineers to align reliability targets with formal analysis outcomes.
  • Co-authored journal work on optimal spare management.

8 Apr - 7 May 2025 · Beijing, China

Institute of Software, Chinese Academy of Sciences

Visiting Researcher

  • Research stay on formal methods for autonomous systems, uncertainty modelling, and strategy synthesis.
  • Collaborated with local researchers on dependable cyber-physical systems analysis.
  • Extended the broader MISSION research thread through in-person technical exchange.

24 Feb - 16 Mar 2026 · Beijing, China

Institute of Software, Chinese Academy of Sciences

Research Visitor

  • Follow-up visit on behavioural equivalence, bisimulation reduction, and attack-fault-defense trees.
  • Worked on statistical model checking for dependable cyber-physical systems.
  • Deepened the research collaboration built during the 2025 stay.

Student Supervision

BSc and MSc topics around ADTs, AFDTs, PRISM, MDPs, and game-theoretic analysis.

Co-supervised 3 MSc theses and 2 BSc theses; all listed MSc theses were completed.

3 MSc projects2 BSc projects
MSc

Attack-Defense Trees with Offensive and Defensive Attributes

Co-supervised: Danut Copae

Extended quantitative ADT analysis with defender attributes and Pareto-efficient trade-offs.

Led to a DSN 2025 publication.

MSc

Converting Attack-Fault Trees into Markov Decision Processes in PRISM

Co-supervised: Aleksandar Petrov

Strategy-aware analysis of attack-fault scenarios through MDPs in PRISM.

MSc

Transformation of Attack-Defense Trees into 2-player Game Automata

Co-supervised: Kirill Fedorov

Generative translation of ADTs into PRISM and game-automata models for quantitative strategy analysis.

BSc

Optimizing Security Strategies via Game-Theoretic ADTs

Co-supervised: Arsalaan Khan

Cost-effective attack-defense strategy analysis with PRISM.

BSc

Modelling Cybersecurity Risks with AFTs and Game Theory

Co-supervised: Lejla Skenderagic

Retry-attack modelling and dynamic risk quantification in attack-fault trees.

Experience

Research roles, visiting work, and self-directed infrastructure practice.

Sep 2022 - Present · Enschede, NL

PhD Candidate, Formal Methods

University of Twente

  • Safety-security co-analysis for cyber-physical systems using attack-fault-defense and attack-defense trees.
  • Statistical model checking and game-theoretic optimization for grid, satellite, and spare management cases.
  • Teaching and supervising work on testing, risk assessment, and attacker-defender modelling.
  • Expected PhD completion: Aug 2026.

22 Jun - 20 Jul 2024 · Rio Cuarto, Argentina

Visiting Researcher

National University of Rio Cuarto / INVAP SE

  • Optimized spare-part strategies for research reactors with statistical model checking.
  • Worked with industry engineers to align reliability targets with formal analysis outcomes.
  • Co-authored journal work on optimal spare management.

8 Apr - 7 May 2025 · Beijing, China

Visiting Researcher

Institute of Software, Chinese Academy of Sciences

  • Research stay on formal methods for autonomous systems, uncertainty modelling, and strategy synthesis.
  • Collaborated with local researchers on dependable cyber-physical systems analysis.
  • Extended the broader MISSION research thread through in-person technical exchange.

24 Feb - 16 Mar 2026 · Beijing, China

Research Visitor

Institute of Software, Chinese Academy of Sciences

  • Follow-up visit on behavioural equivalence, bisimulation reduction, and attack-fault-defense trees.
  • Worked on statistical model checking for dependable cyber-physical systems.
  • Deepened the research collaboration built during the 2025 stay.

Nov 2022 - Present · Netherlands

Personal infrastructure hobby project

myhbd.net

  • Small self-directed hosting and server-administration playground used in spare time.
  • Practical work on Linux hardening, automation, and infrastructure experiments.
  • Keeps the research grounded in operational systems concerns.

Mar 2021 - Apr 2022 · Odense, Denmark

Researcher, CPS Security

University of Southern Denmark

  • Modeled flexible Industry 4.0 production systems in UPPAAL SMC/Stratego.
  • Validated safety and security properties under untrusted assets and variable workflows.
  • Designed controls to lower operational risk while maintaining production flexibility.

Nov 2017 - Jun 2020 · Tabriz, Iran

Research Assistant

University of Tabriz

  • Investigated IoT/6LoWPAN security threats and privacy-preserving PeDAAC improvements.
  • Published on opportunistic routing for constrained wireless networks.
  • Mentored IoT research projects and experiments across the lab.

Jun 2018 - Apr 2019 · Tabriz, Iran

IoT Researcher & Developer

Saymantech

  • Developed IoT features on Arm Mbed OS across NB-IoT, LoRaWAN, BLE, and NFC.
  • Built reusable embedded components and device security hardening patterns.
  • Guided C/C++ practices for embedded teams shipping connected devices.

Education

Academic training.

Sep 2022 - Aug 2026 (expected)

PhD in Formal Methods

University of Twente

2017 - 2019

M.Sc. Software Engineering

University of Tabriz

2014 - 2017

B.Sc. Software Engineering

Islamic Azad University of Tabriz

Publications Preview

Featured papers from the publication list.

2026 · IEEE Computer Security Foundations Symposium (CSF 2026, accepted)

Which attacks are most critical? Risk prioritization via attack tree importance measures

View publication

2025 · 2025 IEEE Annual Reliability and Maintainability Symposium - Europe (RAMS-Europe)

Querying Attack-Fault-Defense Trees: Property Specification in Smart Grid and Aerospace Case Studies

View publication

2025 · International Journal on Software Tools for Technology Transfer 27(3)

Optimal spare management via statistical model checking: a case study in research reactors

View publication

2025 · IEEE/IFIP DSN 2025

Attack-Defense Trees with Offensive and Defensive Attributes

View publication

Teaching

Courses and teaching support.

Q3 2023/2024 and Q3 2024/2025 · 110 hours

Software Testing and Risk Assessment (MSc)

Teaching assistant

Risk assessment methods, software testing techniques, test strategies, and state machines/labelled transition systems.

Q2 2022/2023 · 90 hours

Software Systems (BSc)

Teaching support

Java programming and software design/modelling, including UML use-case, class, sequence, and state-machine diagrams.

Service and Committees

Artifact evaluation and community service.

Artifact Evaluation Committee

International Symposium on Formal Methods (FM 2024)

Link

Artifact Evaluation Committee

International Symposium on Model Checking of Software (SPIN 2024)

Link

Artifact Evaluation Committee

Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025)

Link

Artifact Evaluation Committee

Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026)

Link

Academic Service

Ad-hoc reviewer for journals and conferences

Awards

Selected scholarships, rankings, and research mobility.

  • Ranked 2nd among M.Sc. students in Software Engineering, University of Tabriz (2020)
  • GraDAna Erasmus+ scholarship, Aristotle University of Thessaloniki (2019)
  • Top 0.5% among 25,000+ in Iran's national M.Sc. entrance exam (2017)
  • Summer School: Enabling Technologies for Industrial Internet of Things (ET-I2oT 2021), University of Pisa
  • Research mobility through Project MISSION / MSCA network: National University of Rio Cuarto, Argentina (22 Jun - 20 Jul 2024); Institute of Software, Chinese Academy of Sciences, Beijing (8 Apr - 7 May 2025 and 24 Feb - 16 Mar 2026)
  • Young Researchers and Elite Club, Islamic Azad University, Tabriz Branch (2016)

Technical Tools

Methods, languages, and infrastructure used across research and deployment work.

UPPAAL SMC / StrategoPRISMCPN ToolsStatistical model checkingGame-theory solversArm Mbed OSNB-IoT, LoRaWAN, BLE, NFCLinux hardeningLaTeX and scientific writingAttack-Defense and Attack-Fault-Defense Trees