Ashutosh Trivedi

Email: ashutosh.trivedi @
Web: Home , Twitter, Google Scholar, DBLP, ResearchID, ORCID , and ResearchGate.

“ My research focuses on applying rigorous mathematical reasoning techniques to design and analyze safe and secure cyber-physical systems (CPS) with guaranteed performance. I investigate foundational issues (decidability and complexity) related to modeling and analysis of CPS as well as practically focused tools that can be used by practitioners to analyze large systems at scale.

I am an assistant professor in the Department of Computer Science at the University of Colorado Boulder. I am affilited with the Programming Languages and Verification Group and the Theory Group at the University of Colorado Boulder.



Current Research.

Keywords: Formal Methods, Game Theory, Cyber-Physical Systems, Automata Theory and Logic

I am actively working on the following research projects:
  1. Space/Time Analaysis for Cybersecurity. The goal of this DARPA-sponsored project is to develop new program analysis techniques to allow analysts to discover Java applications with exploitable security vulnerabilities such as availability Discriminer (denial-of-service) and confidentiality (side-channels) vulnerabilities due to space and time usage of the programs. In identifying availability and confidentiality problems, our focus is to minimize both false positives and false negatives. In addition, it is often desirable that every identified vulnerability is presented with sufficient evidence towards an exploit of the vulnerability. In the case of availability problems, such evidence should be in the form of an input that triggers excessive resource usage, while for confidentiality problems, such evidence may a be pair of inputs that result in differential resource usage. I am particularly interested in combining static analysis techniques with run-time analysis to pinpoint program vulnerabilities. In one of our recent publications [1], we present a new run-time analysis technique for debugging Java bytecode to uncover potential causes for side-channels in time.
    Related publications: [1], [2].

  2. Counterexample Sensitivity-analysis for Cyber-Physical Systems. In this Toyota-sponsored project, I investigate simulation-based approaches to analyze a given set of counterexamples to correctness properties of CPS towards explaining and widening the Automotive CPS counterexamples to assist the system designer in further debugging. The resulting approach can be used by engineers to debug their CPS designs inside practical environments such as Simulink/Stateflow in MATLAB. Our approach extends classical sensitivity analysis to generalize neighborhood of counterexamples by computing a box neighborhood around the original counterexample so that sampling inputs in our neighborhood is highly likely to also produce a counterexample. The effectiveness of this approach was successfully demonstrated over many CPS models including automotive and closed-loop medical device control systems.
    Related publications : [1].

  3. Theory of Stochastic Hybrid Structures. The problem of mathematically modeling CPS is fundamental to analyzing their safety and security properties. However, CPS integrate many different aspects including time-criticality, nondeterminism, stochastic timed automata presence of multiple rational agents, rich continuous dynamics, stochastic behavior, and higher-level programming constructs such as heaps and recursion. This poses a fundamental challenge: a rich combination of these features yields models that are too complex to reason about. In this project I study several useful restrictions to these models to characterize the decidability/undecidability frontier as well as exact computational complexity of various verification and synthesis related questions. Parts of this projects were sponsored by a Liverpool-India fellowship, an IIT Bombay seed-grant, and the Indo-french project AVeRTS.
    Related publications : [1], [2], [3], [4], and [5].
    Talk (Video) : Multi-Mode Systems.

  4. Theory of Streaming String Transducers. The beautiful theory of regular languages is the cornerstone of theoretical computer science and formal language theory. The perfect harmony among the languages of finite words definable using Streaming String Transducers abstract machines (deterministic finite automata), algebra (regular expressions and finite monoids), and logic (monadic second-order logic) did set the stage for the generalizations of the theory to the theory of regular languages of infinite words, trees, and partial orders. Alur and Cerny have proposed a model of transducers, called streaming string transducers, that for regular transformations seems to be as appealing model as deterministic finite automata for regular languages. The goal of this project is to study theoretical properties of streaming string transducers and their applications in verification of CPS. This project has been supported by the NSF Expeditions in Computing award 1138996 and an IITB seed-grant.
    Related publications : [1], [2], [3], and [4].

Selected Publications.

  1. Discriminating Traces with Time
    Saeid Tizpaz-Niari, Pavol Cerny, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi
    In Proc. of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017).

  2. Mean-Payoff Games on Timed Automata .
    Shibashis Guha, Marcin Jurdzinski, Krishna S. and Ashutosh Trivedi.
    In Proc. of Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016.

  3. Symmetric Strategy Improvment .
    Sven Schewe, Ashutosh Trivedi, Thomas Varghese.
    In Proc. of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015).

  4. Regular Transformations of Infinite Strings.
    Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi.
    Proceedings of the 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS 2012.

  5. Optimal Scheduling for Constant-Rate Multi-Mode System.
    Rajeev Alur, Ashutosh Trivedi, and Dominik Wojtczak.
    Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, HSCC 2012.
    Best paper award, HSCC, CPS Week 2012.

  6. Recursive Timed Automata.
    Ashutosh Trivedi and Dominik Wojtczak.
    Proceedings of 8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010.

  7. Reachability-Time Games on Timed Automata [Full version].
    Marcin Jurdzinski and Ashutosh Trivedi.
    Proceedings of 34th International Colloquium on Automata, Languages and Programming, ICALP 2007.