Vinayak S. PrabhuPh.D. University of California at Berkeley
Assistant Professor
Office: CSB 446 

Prospective Students: Funded positions available. Information
11th ACM/IEEE International Conference on CyberPhysical 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)
Linear Time Monitoring for One Variable TPTL.25th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2022, pp. 5:15:11.
Towards Efficient Input Space Exploration for Falsification of Input Signal Class Augmented STL.20th ACMIEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2022, pp. 111.
Detecting Secure Memory Deallocation Violations with CBMC. Proceedings of the 8th ACM CyberPhysical System Security Workshop, CPSS@AsiaCCS 2022, pp. 2738.
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. 33243331.
Parameter fault localization for debugging and performance optimization of control software. Proceedings of the 9th ACM/IEEE International Conference on CyberPhysical Systems, (ICCPS) 2018, pp. 230231.
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. 3133.
Testing CyberPhysical 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:1170:18.
The robot routing problem for collecting aggregate stochastic rewards. Proceedings of the 28th International Conference on Concurrency Theory (CONCUR), 2017, pp. 13:113:17.
Quantifying conformance using the Skorokhod metric. Formal Methods in System Design. Vol 50 (23), Springer 2017, pp. 168206.
Shrinking horizon Model Predictive Control with chanceconstrained Signal Temporal Logic specifications. Proceedings of the 2017 American Control Conference (ACC), IEEE 2017, pp. 17401746.
Computing distances between reach flowpipes. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2016, pp. 267276.
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. 234250 (Volume 2).
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. 199208.
Quantitative temporal simulation and refinement distances for timed systems. Transactions on Automatic Control, IEEE, 60(9), 2015, pp. 22912306.
Synthesis of memoryefficient, clockmemory free, and nonZeno safety controllers for timed systems. Information and Computation, Elsevier, 228 (2013), pp. 83119.
Quantitative timed simulation functions and refinement metrics for realtime systems. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2013, pp. 273282.
Finite automata with timedelay blocks. Proceedings of the 10th International Conference on Embedded Software (EMSOFT), ACM 2012, pp. 4352.
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. 223229.
Timed parity games: Complexity and robustness. Journal of Logical Methods in Computer Science, 7(4) (2011), pp. 155.
Synthesis of memory efficient realtime controllers for safety objectives. Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2011, pp. 221230.
QuanTM: A quantitative trust management system. Proceedings of the Second European Workshop on System Security (EuroSec), ACM 2009, pp. 2835.
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, SpringerVerlag, 2008, pp. 124140.
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, SpringerVerlag, 2008, pp. 87100.
Minimumtime reachability in timed games. Proceedings of the 34th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science 4596, SpringerVerlag, 2007, pp. 825837.
Timed alternatingtime temporal logic. Proceedings of the Fourth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 4202, SpringerVerlag, 2006, pp. 117.
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, SpringerVerlag, 2005, pp. 226241.
Assumeguarantee reasoning for hierarchical hybrid systems. Proceedings of the Fourth International Workshop on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 2034, SpringerVerlag, 2001, pp. 275290.
Tool (C++) for computing the Skorokhod distance between two continuoustime traces (given as sampled timepoints) based on the work in [CAV 2015], [FMSD 2017]. Available at Github