Nima Roohi

About Me

I am a postdoctoral scholar in the Computer Science and Engineering Department at the University of California, San Diego, working with Prof. Sicun Gao on model checking and formal synthesis techniques for control and planning problems in robotics. Before joining UCSD, I was a postdoc in the Department of Computer & Information Science at the University of Pennsylvania, working with Prof. Insup Lee, Prof. Oleg Sokolsky, and Prof. James Weimer on development of modeling and verification techniques for cyber-physical systems. I obtained my Ph.D. in Computer Science under the supervision of Prof. Mahesh Viswanathan at the University of Illinois, Urbana-Champaign. My Ph.D. dissertation title is Remedies for Building Reliable Cyber-Physical Systems. Also, while I was a Ph.D. student, I obtained my M.Sc. degree in Mathematics from UIUC. Before joining UIUC, I took my M.Sc. in Software Engineering from Sharif University of Technology under the supervision of Prof. Seyed Hassan Mirian Hosseinabadi, and I earned my B.Sc. also in Software Engineering from Amirkabir University of Technology under supervision of Mr. Bahman Pourvatan.

*** I moved to Amazon as an Applied Scientist. This page will no longer be updated. ***

Research Interests

Formal Verification, Robot Locomotion, Cyber-Physical Systems, Statistical Verification, Robust Model Checking and Monitoring, Temporal Logic, Automata Theory, Theorem Proving.

Publications

2020	Nima Roohi, Yu Wang, Matthew West, Geir Dullerud, and Mahesh Viswanathan. STMC: Statistical Model Checker with Stratified and Antithetic Sampling. To appeare at International Conference on Computer-Aided Verification (CAV), 2020.
2019	Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov Control. Conference on Neural Information Processing Systems (NeurIPS) 3245–3254, 2019.
2019	Sicun Gao, James Kapinski, Jyotirmoy Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Arechiga, and Soonho Kong. Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems. International Conference on Computer-Aided Verification (CAV) 137–154.
2019	Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir Dullerud. Statistical Verification of PCTL Using Antithetic and Stratified Samples. Formal Methods in System Design (FMSD) 1572-8102:1–19.
2018	Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Relating Syntactic and Semantic Perturbations of Hybrid Automata. International Conference on Concurrency Theory (CONCUR) 26:1–26:16.
2018	Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, and Insup Lee. Self-Driving Vehicle Verification Towards a Benchmark. arXiv:1806.08810.
2018	Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir Dullerud. Statistical Verification of PCTL Using Stratified Samples. Analysis and Design of Hybrid Systems (ADHS), International Federation of Automatic Control (IFAC)–PapersOnline 51(16):85–90.
2018	Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, and Insup Lee. Parameter Invariant Monitoring for Signal Temporal Logic. International Conference on Hybrid Systems: Computation and Control (HSCC) 187–196.
2018	Nima Roohi and Mahesh Viswanathan. Revisiting MITL to Fix Decision Procedures. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS 10747:474–494.
2017	Nima Roohi. Remedies for Building Reliable Cyber-Physical Systems. Ph.D. Thesis. Department of Computer Science, University of Illinois at Urbana-Champaign.
2017	Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-Linear Hybrid Automata. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 10205:573–588.
2017	Nima Roohi, Yu Wang, Matthew West, Geir Dullerud, and Mahesh Viswanathan. Statistical Verification of Toyota Powertrain Control Verification Benchmark. International Conference on Hybrid Systems: Computation and Control (HSCC) 65–70.
2017	Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Robust Model Checking of Timed Automata under Clock Drifts. International Conference on Hybrid Systems: Computation and Control (HSCC) 153–162.
2016	Yu Wang, Nima Roohi, Geir Dullerud, and Mahesh Viswanathan. Stability Analysis of Switched Linear Systems defined by Regular Languages. IEEE Transactions on Automatic Control (TAC) 62(5):2568–2575.
2016	Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir Dullerud. Verifying Continuous-Time Stochastic Hybrid Systems Via Mori-Zwanzig Model Reduction. IEEE Conference on Decision and Control (CDC) 3012–3017.
2016	Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Hybridization based CEGAR for Hybrid Automata with Affine Dynamics. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 9636:752–769.
2015	Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir Dullerud. A Mori-Zwanzig and MITL Based Approach to Statistical Verification of Continuous-time Dynamical Systems. Analysis and Design of Hybrid Systems (ADHS), International Federation of Automatic Control (IFAC)–PapersOnline 48(27):267–273.
2015	Pavithra Prabhakar, Nima Roohi, and Mahesh Viswanathan. Deciding Concurrent Planar Monotonic Linear Hybrid Systems. International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), LNCS 9268:256–269.
2015	Nima Roohi and Mahesh Viswanathan. Statistical Model Checking for Unbounded Until Formulas. Software Tools for Technology Transfer (STTT) 17(4):417–427.
2015	Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir Dullerud. Statistical Verification of Dynamical Systems Using Set Oriented Methods. International Conference on Hybrid Systems: Computation and Control (HSCC) 169–178.
2014	Yu Wang, Nima Roohi, Mahesh Viswanathan, and Geir Dullerud. Stability of Linear Autonomous Systems Under Regular Switching Sequences. IEEE Conference on Decision and Control (CDC) 5445–5450.
2014	Nima Roohi and Mahesh Viswanathan. Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints. International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), LNCS 8711:191–205.
2012	Gwen Salaün, Tevfik Bultan, and Nima Roohi. Realizability of Choreographies using Process Algebra Encodings. IEEE Transactions on Services Computing (TSC) 5(3):290–304.
2011	Nima Roohi and Gwen Salaün. Realizability and Dynamic Reconfiguration of Chor Specifications. Informatica, 35(1):39-49.
2009	Gwen Salaün and Nima Roohi. On Realizability and Dynamic Reconfiguration of Choreographies. Workshop on Autonomic and Self-Adaptive Systems (WASELF) (Selected Paper to be Published in Informatica).
2009	Nima Roohi. Choreography and Orchestration of Coordinators in Component-Based Systems. M.Sc. Thesis, Sharif University of Technology, Tehran, Iran (In Persian).
2009	Nima Roohi, Gwen Salaün, and Seyed-Hassan Mirian-Hosseinabadi. Analyzing Chor Specifications by Translation into FSP. Foundations of Coordination Languages and Self-Adaptive Systems (FOCLASA), ENTCS 255:159–176.
2007	Bahman Pourvatan, Arash Afshar, and Nima Ruhy. Modeling Sequential and Concurrent Programs with Reo and Constraint Automata. Foundations of Coordination Languages and Self-Adaptive Systems (FOCLASA).
2007	Bahman Pourvatan and Nima Rouhy. An Alternative Algorithm for Constraint Automata Product. International Conference on Fundamentals of Software Engineering (FSEN), LNCS 4767:412–422.