Awards

  • Florida Cybersecurity Center Collaborative Seed Award (2018-2019)
  • Best Paper Award at the 10th International Conference on Foundations of Privacy & Security FPS (2017)
  • UCF Predictive Analytics Innovation Fellow (2017-2018)
  • Air Force Office of Scientific Research Young Investigator Award (2016-2019)
  • UCF Faculty Senate (2016-2017)
  • National Science Foundation Computing and Communications Foundations -- Exploiting Parallelism & Scalability (2014-2017)
  • National Science Foundation Computing and Communications Foundations -- Software & Hardware Foundations (2014-2018)
  • Best Paper Award at IEEE International Conference on Computational Advances in Bio and Medical Sciences ICCABS (2014)
  • ASE/Air Force Summer Faculty Fellowship (2014)
  • Charles N. Millican Faculty Fellow (2013)
  • IEEE Orlando Outstanding Engineering Educator Award (2013)
  • Air Force Information Directorate Visiting Faculty Fellowship Program (2013)
  • Best Paper Award at IEEE International Conference on Computational Advances in Bio and Medical Sciences ICCABS (2011)

Recent Publications

S. Jha, S. Raj, S. K. Jha, and N. Shankar, “ Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems ,” in 16th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), Beijing, China, Forthcoming.Abstract

 

We propose an automatic synthesis technique to generate provably correct controllers of stochastic linear dynamical systems for Signal Temporal Logic (STL) specifications. While formal synthesis problems can be directly formulated as exists-forall constraints, the quantifier alternation restricts the scalability of such an approach. We use the duality between a system and its proof of correctness to partially alleviate this challenge. We decompose the controller synthesis into two subproblems, each addressing orthogonal concerns - stabilization with respect to the noise, and meeting the STL specification. The overall controller is a nested controller comprising of the feedback controller for noise cancellation and an open loop controller for STL satisfaction. The correct-by-construction compositional synthesis of this nested controller relies on using the guarantees of the feedback controller instead of the controller itself. We use a linear feedback controller as the stabilizing controller for linear systems with bounded additive noise and over-approximate its ellipsoid stability guarantee with a polytope. We then use this over-approximation to formulate a mixed-integer linear programming problem (MILP) to synthesize an open-loop controller that satisfies STL specifications. We demonstrate the effectiveness of the proposed technique on a set of case studies.

 

S. Raj, S. K. Jha, L. L. Pullum, and A. Ramanathan, “ SATYA: Defending against Adversarial Attacks using Statistical Hypothesis Testing ,” in The 10th International Symposium on Foundations and Practice of Security (FPS 2017), Nancy, France. (BEST PAPER AWARD), 2017.Abstract

The paper presents a new defense against adversarial attacks for deep neural networks. We demonstrate the effectiveness of our approach against the popular adversarial image generation method DeepFool. Our approach uses Wald's Sequential Probability Ratio Test to sufficiently sample a carefully chosen neighborhood around an input image to determine the correct label of the image. On a benchmark of 50,000 randomly chosen adversarial images generated by DeepFool we demonstrate that our method SATYA is able to recover the correct labels for 95.76% of the images for CaffeNet and 97.43% of the correct label for GoogLeNet. 

BEST PAPER AWARD

D. Chakraborty, S. Raj, J. C. Gutierrez, T. Thomas, and S. K. Jha, “ In-Memory Execution of Compute Kernels using Flow-based Memristive Crossbar Computing ,” in IEEE International Conference on Rebooting Computing 2017, Washington D.C., 2017.Abstract

 

Rebooting computing using in-memory architectures relies on the ability of emerging devices to execute a legacy software stack. In this paper, we present our approach of executing compute kernels written in a subset of the C pro- gramming language using flow-based computing on nanoscale memristor crossbars. Our framework also tests the correctness of the design using the parallel Xyces electronic simulation software. We demonstrate the potential of our design methodology by designing and testing a compute kernel for edge detection in images. 

 

S. Raj, A. Ramanathan, L. L. Pullum, and S. K. Jha, “ Testing Autonomous Cyber-Physical Systems using Fuzzing Features Derived from Convolutional Neural Networks ,” in ACM SIGBED International Conference on Embedded Software (EMSOFT), Seoul, South Korea, 2017.Abstract

 

Autonomous cyber-physical systems rely on modern machine learning methods such as deep neural networks to control their interactions with the physical world. Testing of such intelligent cyber-physical systems is a challenge due to the huge state space associated with high-resolution visual sensory inputs. In this paper, we demonstrate how fuzzing the input using patterns obtained from the convolutional lters of an unrelated convolutional neural network can be used to test the correctness of vision algorithms implemented in intelligent cyber-physical systems. Our method discovers interesting counterexamples to the pedestrian detection algorithm implemented in the popular OpenCV library. Our approach also unearths counterexamples to the correct behavior of an autonomous car similar to NVIDIA’s end-to-end self-driving deep neural net running on the Udacity open-source simulator. 

 

S. Raj and S. K. Jha, “ Predicting Success in Undergraduate Parallel Programming via Probabilistic Causality Analysis ,” in 8th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar-18) co-located with the 32nd IEEE International Parallel & Distributed Processing Symposium, Vancouver, Canada, 2018.Abstract

 

We employ probabilistic causality analysis to study the performance data of 301 students from the upper-level under- graduate parallel programming class at the University of Central Florida. To our surprise, we discover that good performance in our lower-level undergraduate programming CS-I and CS- II classes is not a significant causal factor that contributed to good performance in our parallel programming class. On the other hand, good performance in systems classes like Operating Systems, Information Security, Computer Architecture, Object Oriented Software and Systems Software coupled with good performance in theoretical classes like Introduction to Discrete Structures, Artificial Intelligence and Discrete Structures-II are strong indicators of good performance in our upper-level un- dergraduate parallel programming class. We believe that such causal analysis can be useful in identifying whether parallel and distributed computing concepts have effectively penetrated the lower-level computer science classes at an institution.

 

A. U. Hassen and S. K. Jha, “ Free Binary Decision Diagram Based Synthesis of Compact Crossbars for in-Memory Computing of Boolean Functions ,” in International Symposium on Circuits and Systems (ISCAS), Florence, Italy, 2018.Abstract

We introduce a new computer-aided design  approach based on Free Binary Decision Diagrams (FBDDs) for  implementing Boolean functions on crossbars using flow-based computing. Our crossbar synthesis procedure uses generalized FBDDs to design crossbars for a Boolean formula such that there is a flow of current from an input nanowire to an output nanowire through the sneak paths in the crossbar if and only if the Boolean formula evaluates to true.  Generalized FBDDs are more succinct representations of Boolean formula that traditional Reduced Ordered Binary Decision Diagrams (ROBDDs) because they do not require the same variable ordering along all paths of the decision diagram.   Our experimental results with the middle bit of a multiplier show that our designs are 69.9% more succinct than flow-based crossbar computing approaches designed using ROBDDs. 

A. Velasquez and S. K. Jha, “ Fault-Tolerant In-Memory Computing Using Paths-Based Logic and Heterogeneous Components ,” in Design, Automation, and Test in Europe (DATE), Dresden, Germany, 2018.Abstract

 

The memory-processor bottleneck and scaling difficulties of the CMOS transistor have given rise to a plethora of research initiatives to overcome these challenges. Popular among these is in-memory crossbar computing. In this paper, we propose a framework for synthesizing fault-tolerant computation- in-memory circuits based on bounded model checking. The resulting designs can be used to compute Boolean formulas using a constant number of read and write cycles. We demonstrate the effectiveness of the approach by generating addition and comparator circuits in the presence of common crossbar faults. 

 

More