Vinayak S. Prabhu Ph.D. University of California at Berkeley Assistant Professor Department of Computer Science Colorado State University Office: CSB 446

Research Areas

• Formal Methods for Verification and Synthesis.
• Formal Verification and Model Checking. Temporal logics.
• Embedded and Cyber-Physical Systems (CPS). Models of computation.
• Robustness issues in CPS. Conformance checking.
• Control of timed, hybrid and discrete-event systems.
• Multi-agent and autonomous systems.
• Scheduling.
• Security.

The goal of our research is to synthesize tools and algorithms to aid the development of reliable embedded and cyber-physical systems and devices, using techniques from formal methods (automata theory, logic), control theory, and software analysis. Our team deals with both theoretic and applied aspects, building on collaborations with researchers and industrial research labs from the US and from Europe.

Funding

Teaching

• Spring 2024: Foundations of Formal Methods and Cyber-Physical Systems (CS 522)
• Fall 2023: Automata, Logic, and Computation (CS 422)
• Fall 2023: Foundations of Computation (CS 580A7)
• Spring 2023: Foundations of Formal Methods and Cyber-Physical Systems (CS 522)
• Spring 2023: Research Topics: Temporal Logics and Monitoring (CS 793)
• Fall 2022: Automata, Logic, and Computation (CS 422)
• Fall 2022: Foundations of Computation (CS 580A7)
• Fall 2022: Research Topics: Temporal Logics and Monitoring (CS 793)
• Fall 2022: Research Topics: Programming Languages, High Peformance Computiing, Formal Methods (CS 793) with Sanjay Rajopadhye and Jedidiah Mcclurg
• Spring 2022: Foundations of Formal Methods and Cyber-Physical Systems (CS 522)
• Fall 2021: CS692 -- Formal Methods rotation (3 weeks)
• Fall 2021: Foundations of Computation (CS 580A7)
• Fall 2021: Automata, Logic, and Computation (CS 422)
• Spring 2021: CS692 -- Formal Methods rotation (3 weeks)
• Spring 2021: Foundations of Formal Methods and Cyber-Physical Systems (CS 522)
• Fall 2020: Research Topics: Formal Methods for Safe AI (CS 793)
• Spring 2020: Foundations of Cyber-Physical Systems (CS 522)
• Spring 2020: Research Topics: Testing and Optimization for CPS (CS 793)
• Fall 2019: Automata, Logic, and Computation
• Spring 2019: Foundations of Cyber-Physical Systems (CS 581A4)
• Fall 2018: Introduction to Analysis of Algorithms (CS 420)
• Spring 2018: Foundations of Cyber-Physical Systems (CS 581A4)

Program Committees

• 16th APCA International Conference on Automatic Control and Soft Computing (Controlo 2024))


• 11th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2020)


• 21st ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2018)


• 20th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2017)

Research Advisees

• Bassem Ghorbel (PhD)
• Takwa Rhaimi (PhD)
• Rye Easton (MS)

Alumni

• Rye Easton (CSU BS 2023 ➙ CSU Graduate progam)
• Campbell Bradley (advised with Sanjay Rajopadhye) (CSU BS 2023 ➙ CSU Graduate progam)
• Alex Karduna (advised with Sanjay Rajopadhye) (CSU BS 2023 ➙ CSU Graduate progam)
• Isaac Jacobson (advised with Sudipto Ghosh, Indrajit Ray, and Indrakshi Ray) (CSU BS 2022)
• Alperen Tercan (advised with Charles Anderson)(CSU MS 2022 ➙ University of Michigan PhD program)
• Meetkumar Savaliya (CSU MS 2022 ➙ Data Ductus)
• Mohit Singh (advised with Indrajit Ray) (CSU MS 2021 ➙ Intel)
• Jordan Peterson (advised with Indrakshi Ray) (CSU MS 2021 ➙ NREL)

Publications

• Bassem Ghorbel and Vinayak S. Prabhu, Quantitative Robustness for Signal Temporal Logic With Time-Freeze Quantifiers.  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume: 42, Issue: 12, IEEE 2023, pp. 4436 - 4449.


• Bassem Ghorbel and Vinayak S. Prabhu, Linear Time Monitoring for One Variable TPTL.   25th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2022, pp. 5:1-5:11.


• Vinayak S. Prabhu and Meetkumar Savaliya, Towards Efficient Input Space Exploration for Falsification of Input Signal Class Augmented STL.   20th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2022, pp. 1-11.


• Vinayak S. Prabhu, Mohit Singh, Indrajit Ray, Indrakshi Ray and Sudipto Ghosh, Detecting Secure Memory Deallocation Violations with CBMC.  Proceedings of the 8th ACM Cyber-Physical System Security Workshop, CPSS@AsiaCCS 2022, pp. 27-38.


• Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu and Sadegh Soudjani, Shrinking horizon Model Predictive Control with Signal Temporal Logic constraints under stochastic disturbances.   IEEE Transactions on Automatic Control,   Volume: 64 , Issue: 8, IEEE 2019, pp. 3324-3331.


• Jyotirmoy V. Deshmukh, Xiaoqing Jin, Rupak Majumdar and Vinayak S. Prabhu, Parameter fault localization for debugging and performance optimization of control software.   Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems, (ICCPS) 2018, pp. 230-231.


• Rayna Dimitrova, Rupak Majumdar and Vinayak S. Prabhu, Causality analysis for Concurrent Reactive Systems (Extended Abstract).   Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology, CREST@ETAPS 2018, EPTCS Volume: 286, pp. 31-33.


• Jyotirmoy V. Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar and Vinayak S. Prabhu, Testing Cyber-Physical Systems through Bayesian Optimization . Transactions on Embedded Computing Systems (TECS), ESWEEK special issue for articles presented in the 2017 ACM SIGBED International Conference on Embedded Software (EMSOFT), vol 16(5s) ACM 2017, pp. 170:1-170:18.


• Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu and Sadegh Soudjani, The robot routing problem for collecting aggregate stochastic rewards.   Proceedings of the 28th International Conference on Concurrency Theory (CONCUR), 2017, pp. 13:1-13:17.


• Jyotirmoy V. Deshmukh, Rupak Majumdar and Vinayak S. Prabhu, Quantifying conformance using the Skorokhod metric.   Formal Methods in System Design.   Vol 50 (2-3), Springer 2017, pp. 168-206.


• Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu and Sadegh Soudjani, Shrinking horizon Model Predictive Control with chance-constrained Signal Temporal Logic specifications.   Proceedings of the 2017 American Control Conference (ACC), IEEE 2017, pp. 1740-1746.


• Rupak Majumdar, and Vinayak S. Prabhu, Computing distances between reach flowpipes.  Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2016, pp. 267-276.


• Jyotirmoy V. Deshmukh, Rupak Majumdar, and Vinayak S. Prabhu, Quantifying conformance using the Skorokhod metric.  Proceedings of the 27th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science 9207, Springer 2015, pp. 234-250 (Volume 2).


• Rupak Majumdar, and Vinayak S. Prabhu, Computing the Skorokhod distance between polygonal traces. [Technical report]  Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2015, pp. 199-208.


• Krishnendu Chatterjee, and Vinayak S. Prabhu, Quantitative temporal simulation and refinement distances for timed systems.  Transactions on Automatic Control, IEEE, 60(9), 2015, pp. 2291-2306.


• Krishnendu Chatterjee, and Vinayak S. Prabhu, Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems.  Information and Computation, Elsevier, 228 (2013), pp. 83-119.


• Krishnendu Chatterjee, and Vinayak S. Prabhu, Quantitative timed simulation functions and refinement metrics for real-time systems.  Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2013, pp. 273-282.


• Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Finite automata with time-delay blocks.  Proceedings of the 10th International Conference on Embedded Software (EMSOFT), ACM 2012, pp. 43-52.


• Mangal Kothari, Jose Pinto, Vinayak S. Prabhu, Pedro Ribeiro, Joao Borges de Sousa, and P.B. Sujit, Robust Mission Planning for Underwater Applications: Issues and Challenges.  Proceedings of the 3rd IFAC Workshop on Navigation, Guidance and Control of Underwater Vehicles (NGCUV), IFAC 2012, pp. 223-229.


• Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Timed parity games: Complexity and robustness.  Journal of Logical Methods in Computer Science, 7(4) (2011), pp. 1-55.


• Krishnendu Chatterjee, and Vinayak S. Prabhu, Synthesis of memory efficient real-time controllers for safety objectives.  Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2011, pp. 221-230.


• Andrew G. West, Adam J. Aviv, Jian Chang, Vinayak S. Prabhu, Matt Blaze, Sampath Kannan, Insup Lee, Jonathan M. Smith, and Oleg Sokolsky, QuanTM: A quantitative trust management system.  Proceedings of the Second European Workshop on System Security (EuroSec), ACM 2009, pp. 28-35.


• Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Timed parity games: Complexity and robustness.  Proceedings of the Sixth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 5215, Springer-Verlag, 2008, pp. 124-140.


• Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Trading infinite memory for uniform randomness in timed games.  Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 4981, Springer-Verlag, 2008, pp. 87-100.


• Thomas Brihay, Thomas A. Henzinger, and Vinayak S. Prabhu, and Jean-Francois Raskin, Minimum-time reachability in timed games.  Proceedings of the 34th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science 4596, Springer-Verlag, 2007, pp. 825-837.


• Thomas A. Henzinger, and Vinayak S. Prabhu, Timed alternating-time temporal logic.  Proceedings of the Fourth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 4202, Springer-Verlag, 2006, pp. 1-17.


• Thomas A. Henzinger, Rupak Majumdar, and Vinayak S. Prabhu, Quantifying similarities between timed systems.  Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 3829, Springer-Verlag, 2005, pp. 226-241.


• Thomas A. Henzinger, Marius Minea, and Vinayak S. Prabhu, Assume-guarantee reasoning for hierarchical hybrid systems.  Proceedings of the Fourth International Workshop on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 2034, Springer-Verlag, 2001, pp. 275-290.