1 citations · 2 across the 4 of their papers we have counts for
10 papers
Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction
Yu Wang, Nima Roohi, Matthew West +2
We present a scalable methodology to verify stochastic hybrid systems. Using the Mori-Zwanzig reduction method, we construct a finite state Markov chain reduction of a given stocha…
The Complexity of Dynamic Data Race Prediction
Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan
Writing concurrent programs is notoriously hard due to scheduling non-determinism. The most common concurrency bugs are data races, which are accesses to a shared resource that can…
Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning
Yu Wang, Nima Roohi, Matthew West +2
Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model…
What's Decidable About Program Verification Modulo Axioms?
Umang Mathur, P. Madhusudan, Mahesh Viswanathan
We consider the decidability of the verification problem of programs \emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and r…
Revisiting MITL to Fix Decision Procedures
Nima Roohi, Mahesh Viswanathan
Metric Interval Temporal Logic (MITL) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITL re…
Decidable Synthesis of Programs with Uninterpreted Functions
Paul Krogmeier, Umang Mathur, Adithya Murali +2
We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class…