Md. Ariful Islam

PhD Student
Concurrency and Verification Lab
Email: mdaislam@cs.stonybrook.edu

Home Research Academic CV

Research Interest

  • Cyber-physical Systems: Complex Biological Systems, Distributed Embedded Systems, Multi-agent Systems
  • Formal Methods: Model Checking, Abstract Interpretations, Temporal Logic, Automata Theory
  • System Identification: Parameter Estimations, Sensitivity Analysis, Optimization
  • Control Theory: Lyapunov Stability, Input-to-Output Stability, Controller Synthesis
  • Research Projects

  • Close Loop verification of ICDs: Working on closed-loop formal verification of Implantable Cardiac Devices (ICD) using cardiac electro-physiological models as a part of NSF-funded project named CyberHeart. Formal verification techniques, such as simulation-based model checking and reachability analysis, will be applied to high-fidelity cardiac electro-physiological models that capture electrical excitation induced by the ICD’s control software.
  • Parameter-Range Estimation of Tap Withdrawal in C. Elegans: Worked on formal verification of a nonlinear ODE model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in C. Elegans. Specifically, performed reachability analysis on the TW circuit model of Wicks et al. (1996), which enables to estimate ranges of key circuit parameters. Underlying the approach is the use of technique for automatically computing local discrepancy of general nonlinear systems. ([4])
  • AFib Challenge: Atrial Fibrillation (AFib) challenge problem of ( CMACS ) entails developing and applying advanced computational technique to analyze cardiac electro-physiology and understand the root cause of atrial fibrillation and facilitate model-based therapy. Major contribution:
  • Model Predictive Controllers (MPCs) for Neuron: Synthesized both online and explicit MPCs to control time-varying trajectories of a nonlinear ODE model. A piecewise affine model is used as the predictive model for MPCs. Explicit MPC is constructed by extending multi-parametric toolbox (MPT) and online MPC is synthesized using nonlinear programming (fmincon) in MATLAB.
  • Parameter Synthesis of Generic Flocking Model: Worked on parameter synthesis of multi-agent generic flocking systems using statistical model checking (SMC) and global optimization to analyze global emergent behavior such as formation of flocking. Genetic algorithm is chosen as global optimizer.
  • Publication

    Undergrad Thesis: Algorithms in Computational Geometry

    Poster & Presentations