Shromona Ghosh picture

Shromona Ghosh


I am a PhD Candidate in the Electrical Engineering and Computer Science Department, University of California at Berkeley, advised by Prof. Alberto Sangiovanni-Vincentelli. Previously, I have interned at Texas Instruments (Summer 2012), Cadence Design Systems (Summer 2014) and MSR (Summer 2017).

I am broadly interested in Safe Learning, Control Theory, Formal Methods, System Identification, Synthesis and Verification, Cyber Physical Systems and Data Driven Design.


System Identification from Data for Safe Learning
We are exploring the problem of modeling unknown dynamics in hybrid systems from historical and run time data while guaranteeing safety. We are considering both supervised and unsupervised learning based on the system domain. Due to the uncertainities in the unknown part of the system, we are looking into probabilitic models such as Markov Chains and Neural Networks and learnig specifications on the model in Probabilitic Signal Temporal Logic (PrSTL) which can be used for synthesis and verification purposes.

Diagnosis and Repair of Specifications for Controller Synthesis
We diagnose failures expressed in Signal Temporal Logic in a reactive control algorithm. Our tool, DiaRY, identifies the causes of infeasibility in the specifications and provides minimal timing and predicate repairs to make the controller synthesis problem feasible. This work was presented in Hybrid Systems: Computation and Control, 2016.

Requirement Engineering using Contracts
We are currently working on building a tool which could help us reason with contracts or specifications expressed in different mathematical formalisms (such as Linear Temporal Logic, Signal Temporal Logic). The tool would help the designer reason about the compatibility, consistency and realizability of specifications.

Robust Online Monitoring of Signal Temporal Logic
We developed an Online Monitor in C++ for testing systems whose specifications are expressed in Signal Temproal Logic. The Online Monitor saved up to 24% simulation time with minimal overhead. This work won the best paper award at Runtime Verification, 2015.

Compositional Synthesis from Linear Temporal Logic Primitives
We are developing a tool which takes as input a Linear Temporal Logic specification and uses a structural mapping approach (similar to DAGON) to map the specification to LTL primitives in a library. This approach is able to handle specification more general than GR1 specifications and at the same time reduce the doubly exponential complexity of synthesis from LTL.

Maintenance of Components in Safety Critical Hybrid Systems
We are looking at the problem of maintence of components in a Power System. We first model the components using graphical models and identify its acceptable behaviors. We then design monitors which tracks the behavior of the components during its operation and identify which components need maintenance ahead of time.


Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications
S. Ghosh, D. Sadigh, P. Nuzzo, V. Raman, A. Donze, A. Sangiovanni Vincentelli, S. Sastry and S. Seshia
HSCC, Vienna, Austria. Apr 2016 (passed Repeatibility Evaluation).

Robust Online Monitoring of Signal Temporal Logic
J. Deshmukh, A. Donze, S. Ghosh, X. Jin, G. Juniwal and S. Seshia,
RV, Vienna, Austria. Sep 2015; Best Paper Award

SmartScan + OPMISR : A Novel Scan Compression Architecture for Multi-Site Testing
R. Parekhji, R. Chandel, S. Ghosh, R. Suthapalli, G. Swathi and D.Gaur
CDN Live Conference, Bangalore, India. Oct 2012; Best Paper Award in Digital Front End Track