# Publications

Forthcoming
A. Velasquez and S. K. Jha, “ 3D Crosspoint Memory as a Parallel Architecture for Computing Network Reachability ,” in IEEE International Conference on Computer Design (ICCD), Forthcoming.Abstract

We introduce a new in-memory computing design that can compute single-source reachability and transitive closure of graphs by using the natural parallel flow of information in three-dimensional crosspoint memories. The proposed design can be implemented using 3D crosspoint architectures with two layers of 1-diode 1-resistor (1D1R) interconnects. Our logic-in-memory design mitigates the infamous memory-processor bottleneck characteristic of John von Neumann architectures and has a runtime complexity of $\mathcal{O}(n)$ using $\mathcal{O}(n^2)$ devices for a graph with $n$ nodes. This compares favorably to efficient algorithms on John von Neumann architectures with a time complexity of $\mathcal{O}(n^3/p + n^2 \log p)$ on $p$ processors and a competing in-memory approach with runtime $\mathcal{O}(n^2)$ using $\mathcal{O}(n^3)$ components.

2018
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, 2018.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.

A. Velasquez and S. K. Jha, “ Parallel Transitive Closure Within 3D Crosspoint Memory ,” in ACM Symposium on Parallelism in Algorithms and Architectures, Vienna, Austria, 2018.
A. U. Hassen, D. Chakraborty, and S. K. Jha, “ Free Binary Decision Diagram Based Synthesis of Compact Crossbars for in-Memory Computing of Boolean Functions ,” Transactions on Circuits and Systems (TCAS) II, 2018.
A. U. Hassen and S. K. Jha, “ Free BDD based Computer-aided Design of Compact Memristor Crossbars for in-Memory Computing ,” in 14th IEEE / ACM International Symposium on Nanoscale Architectures (NANOARCH), Athens, Greece, 2018.
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.

L. L. Pullum, C. Steed, A. Ramanathan, and S. K. Jha, “ Mathematically Rigorous Verification and Validation of Scientific Machine Learning ,” in DOE ASCR Workshop on Scientific Machine Learning, 2018.
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.

2017
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.

A. Ramanathan, L. L. Pullum, S. Raj, Z. Husein, S. Pattanaik, and S. K. Jha, “ Adversarial attacks on computer vision algorithms using natural perturbations ,” in Tenth International Conference on Contemporary Computing, New Delhi, India, 2017, pp. in press.Abstract

Verifying the correctness of intelligent embedded systems is notoriously difficult due to the use of machine learning algorithms that cannot provide guarantees of deterministic correctness. In this paper, we investigate the histogram of oriented gradients (HOG) based human detection algorithm implemented in the popular OpenCV computer vision framework. Our validation efforts demonstrate that the OpenCV imple- mentation is susceptible to errors due to both malicious perturbations and naturally occurring fog phenomena. To the best of our knowledge, we are the first to explicitly employ a natural perturbation (like fog) as an adversarial attack using methods from computer graphics and demonstrate that computer vision algorithms are also susceptible to errors under such naturally occurring minor perturbations. Our methods and results may be of interest to the designers, developers and validation teams of intelligent cyber-physical systems such as autonomous cars.

S. Raj, S. K. Jha, L. L. Pullum, and A. Ramanathan, “ Statistical Hypothesis Testing using CNN Features for Synthesis of Adversarial Counterexamples to Human and Object Detection Vision Systems ,” Oak Ridge National Laboratory Technical Report, vol. ORNL/LTR-2017/118. 2017. Publisher's VersionAbstract

Validating the correctness of human detection vision systems is crucial for safety applications such as pedestrian collision avoidance in autonomous vehicles. The enormous space of possible inputs to such an intelligent system makes it difficult to design test cases for such systems. In this paper, we present our tool MAYA that uses an error model derived from a convolutional neural network (CNN) to explore the space of images similar to a given input image, and then tests the correctness of a given human or object detection system on such perturbed images. We demonstrate the capability of our tool on the pre-trained Histogram-of- Oriented-Gradients (HOG) human detection algorithm implemented in the popular OpenCV toolset and the Caffe object detection system pre-trained on the ImageNet benchmark. Our tool may serve as a testing resource for the designers of intelligent human and object detection systems.

S. Raj, et al., “ A theorem proving approach for automatically synthesizing visualizations of flow cytometry data ,” BMC Bioinformatics, vol. 18, no. 8, pp. 245, 2017. Publisher's VersionAbstract

Polychromatic flow cytometry is a popular technique that has wide usage in the medical sciences, especially for studying phenotypic properties of cells. The high-dimensionality of data generated by flow cytometry usually makes it difficult to visualize. The naive solution of simply plotting two-dimensional graphs for every combination of observables becomes impractical as the number of dimensions increases. A natural solution is to project the data from the original high dimensional space to a lower dimensional space while approximately preserving the overall relationship between the data points. The expert can then easily visualize and analyze this low-dimensional embedding of the original dataset.

D. Chakraborty, S. Raj, and S. K. Jha, “ A Compact 8-bit Adder Design using In-Memory Memristive Computing: Towards Solving the Feynman Grand Prize Challenge ,” in 13th ACM/IEEE International Symposium on Nanoscale Architectures, Newport, USA, 2017, pp. in press.Abstract

We introduce a new compact in-memory computing design for implementing 8-bit addition using eight vertically-stacked nanoscale crossbars of  one-diode one-memristor 1D1M switches. Each crossbar in our design only has 5 rows and 4 columns. Hence, the design may be used to fabricate a compact 8-bit adder that meets the size constraint of  50nm x 50nm x 50nm imposed by the electrical component of the Feynman Grand Prize. The potential availability of sub-5nm nanoscale memristors and single-molecule diode devices coupled with the ability to fabricate high-density nanoscale memristor crossbars suggests that our design may eventually be fabricated to meet the size constraints of the  Feynman Grand Prize.

A. Velasquez and S. K. Jha, “ Computation of Boolean Matrix Chain Products in 3D ReRAM ,” in IEEE International Symposium on Circuits and Systems (ISCAS), Baltimore, MD, 2017, pp. 2643-2646.Abstract

Energy concerns, the infamous memory wall, and the enormous data deluge of the current big-data age have made the integration of processing and memory elements into a very appealing paradigm. In this paper, we focus on a computation-in- memory solution to the problem of multiplying a set of Boolean matrices, also known as Boolean matrix chain multiplication (BMCM). This is a fundamental computational task with applica- tions in graph theory, group testing, data compression, and digital signal processing. In particular, we propose a framework for mapping arbitrary instances of BMCM to a 3-dimensional (3D) crossbar memory architecture consisting of 1-diode 1-resistor (1D1R) structures.

S. Raj, D. Chakraborty, and S. K. Jha, “ In-Memory Flow-Based Stochastic Computing on Memristor Crossbars using Bit-Vector Stochastic Streams ,” in IEEE International Conference on Nanotechnology (IEEE NANO), Pittsburgh, PA, 2017, pp. in press.
D. Chakraborty and S. K. Jha, “ Design of Compact Memristive In-Memory Computing Systems using Model Counting ,” in IEEE International Symposium on Circuits and Systems (ISCAS)., Baltimore, MD, 2017, pp. 2655-2658.Abstract

Crossbars of nanoscale memristors are being fab- ricated to serve as high-density non-volatile memory devices. The flow of current through memristor crossbars has been recently used to perform in-memory computations. However, existing approaches based on decision procedures only scale to the simplest circuits such as one-bit adders and other approaches employing decision diagrams produce large crossbar designs.

In this paper, we present a new method for synthesizing 3 compact combinational circuits using nanoscale crossbars. Our synthesis procedure exploits a symbolic representation of Boolean functions and employs model counting to guide a simulated annealing based search procedure.

D. Chakraborty and S. K. Jha, “ Automated synthesis of compact crossbars for sneak-path based in-memory computing ,” in 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pp. 770–775.Abstract

The rise of data-intensive computational loads has 1) exposed the processor-memory bottleneck in Von Neumann architectures and has reinforced the need for in-memory com- puting using devices such as memristors. Existing literature on computing Boolean formula using sneak-paths in nanoscale memristor crossbars has only focussed on short Boolean formula. There are two open questions: (i) Can one synthesize sneak-path based crossbars for computing large Boolean formula? (ii) What is the size of a memristor crossbar that can compute a given Boolean formula using sneak paths? In this paper, we make progress on both these problems. First, we show that the number of rows and columns required to compute a Boolean formula is at most linear in the size of the Reduced Ordered Binary Decision Diagram representing the Boolean function. Second, we demonstrate how Boolean Decision Diagrams can be used to synthesize nanoscale crossbars that can compute a given Boolean formula using naturally occurring sneak paths. In particular, we synthesize large logical circuits such as 128-bit adders for the first-time using sneak-path based crossbar computing.

S. K. Jha and C. J. Langmead, “ Stochastic computational model parameter synthesis system ”, US Patent: US9558300 B2, 2017.Abstract

A stochastic computational model parameter synthesis system comprising at least one processor capable of executing processor executable code, and a non-transitory computer memory operably coupled with the at least one processor and storing processor executable code, which when executed by processor, causes processor to synthesize at least one parameter of a stochastic computational model to satisfy one or more behavioral specifications of properties observed in a modeled system. The processor generates and searches randomized projections of a first parameter space having n dimensions into one or more second abstract parameter space having d dimensions, where d is less than n, and outputs a signal indicative of a synthesized parameter value to the user.

US Patent App. 13/673,575

2016
A. U. Hassen, B. Chandrasekar, and S. K. Jha, “ Automated synthesis of stochastic computational elements using decision procedures ,” in Circuits and Systems (ISCAS), 2016 IEEE International Symposium on, 2016, pp. 1678–1681.
A. Velasquez, P. Wojciechowski, K. Subramani, S. L. Drager, and S. K. Jha, “ The cardinality-constrained paths problem: Multicast data routing in heterogeneous communication networks ,” in Network Computing and Applications (NCA), 2016 IEEE 15th International Symposium on, 2016, pp. 126–130.
S. K. Jha, D. E. Rodriguez, J. E. Van Nostrand, and A. Velasquez, “ Computation of boolean formulas using sneak paths in crossbar computing ”, US Patent: 9319047, 2016.

US Patent 9,319,047

Z. Alamgir, K. Beckmann, N. Cady, A. Velasquez, and S. K. Jha, “ Flow-based computing on nanoscale crossbars: Design and implementation of full adders ,” in Circuits and Systems (ISCAS), 2016 IEEE International Symposium on, 2016, pp. 1870–1873.
A. Ramanathan, L. L. Pullum, F. Hussain, D. Chakrabarty, and S. K. Jha, “ Integrating symbolic and statistical methods for testing intelligent systems: Applications to machine learning and computer vision ,” in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016, 2016, pp. 786–791.
A. Velasquez and S. K. Jha, “ Parallel boolean matrix multiplication in linear time using rectifying memristors ,” in Circuits and Systems (ISCAS), 2016 IEEE International Symposium on, 2016, pp. 1874–1877.
2015
R. Saha, J. Esparza, S. K. Jha, M. Mukund, and P. S. Thiagarajan, “ Distributed Markov Chains ,” in Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, 2015, pp. 117–134. Publisher's Version
F. Hussain, C. J. Langmead, Q. Mi, J. Dutta-Moscato, Y. Vodovotz, and S. K. Jha, “ Automated parameter estimation for biological models using Bayesian statistical model checking ,” BMC bioinformatics, vol. 16, no. 17, pp. S8, 2015.Abstract

Background: Probabilistic models have gained widespread acceptance in the systems biology community as a useful way to represent complex biological systems. Such models are developed using existing knowledge of the structure and dynamics of the system, experimental observations, and inferences drawn from statistical analysis of empirical data. A key bottleneck in building such models is that some system variables cannot be measured experimentally. These variables are incorporated into the model as numerical parameters. Determining values of these parameters that justify existing experiments and provide reliable predictions when model simulations are performed is a key research problem. Domain experts usually estimate the values of these parameters by fitting the model to experimental data. Model fitting is usually expressed as an optimization problem that requires minimizing a cost-function which measures some notion of distance between the model and the data. This optimization problem is often solved by combining local and global search methods that tend to perform well for the specific application domain. When some prior information about parameters is available, methods such as Bayesian inference are commonly used for parameter learning. Choosing the appropriate parameter search technique requires detailed domain knowledge and insight into the underlying system.

Results: Using an agent-based model of the dynamics of acute inflammation, we demonstrate a novel parameter estimation algorithm by discovering the amount and schedule of doses of bacterial lipopolysaccharide that guarantee a set of observed clinical outcomes with high probability. We synthesized values of twenty-eight unknown parameters such that the parameterized model instantiated with these parameter values satisfies four specifications describing the dynamic behavior of the model.

Conclusions: We have developed a new algorithmic technique for discovering parameters in complex stochastic models of biological systems given behavioral specifications written in a formal mathematical logic. Our algorithm uses Bayesian model checking, sequential hypothesis testing, and stochastic optimization to automatically synthesize parameters of probabilistic biological models.

BEST PAPER AWARD at IEEE ICCABS 2014

A. Velasquez and S. K. Jha, “ Automated synthesis of crossbars for nanoscale computing using formal methods ,” in Nanoscale Architectures (NANOARCH), 2015 IEEE/ACM International Symposium on, 2015, pp. 130–136.Abstract

Since the fabrication of nanoscale memristors by HP Labs in 2008, there has been a renewed interest in the use of crossbars of nanoscale memristors as digital storage and neuromorphic computing devices. However, the same success has not been replicated in the use of crossbars for performing general-purpose computations that can support the existing software infrastructure originally designed for Von Neumann architectures. One of the key challenges facing this technology is the existence of sneak paths. While it has been shown that sneak paths can be used to perform Boolean computations in crossbars, the human mind is not particularly suited to reason about the exponential complexity of sneak paths in crossbars. Hence, the size of the crossbar designs proposed in the literature has been large for practical applications. In this paper, we demonstrate how formal methods can be used to automatically synthesize compact crossbar designs that can be used to evaluate Boolean formula by using the sneak paths phenomena as a design primitive. We show that our automated synthesis technique can be used to generate a state-of-the-art nano-crossbar design for a 1-bit full adder.

A. Velasquez and S. K. Jha, “ Fault-tolerant in-memory crossbar computing using quantified constraint solving ,” in Computer Design (ICCD), 2015 33rd IEEE International Conference on, 2015, pp. 101–108.Abstract

There has been a surge of interest in the effective storage and computation of data using nanoscale crossbars. In this paper, we present a new method for automating the design of fault-tolerant crossbars that can effectively compute Boolean formula. Our approach leverages recent advances in Satisfiability Modulo Theories (SMT) solving for quantified bit-vector formula (QBVF). We demonstrate that our method is well-suited for fault- tolerant computation and can perform Boolean computations despite stuck-open and stuck-closed interconnect defects as well as wire faults. We employ our framework to generate various arithmetic and logical circuits that compute correctly despite the presence of stuck-at faults as well as broken wires.

F. Hussain, et al., “ SANJAY: Automatically synthesizing visualizations of flow cytometry data using decision procedures ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2015 IEEE 5th International Conference on, 2015, pp. 1–1.
2014
A. K. Ghosh, F. Hussain, S. Jha, C. J. Langmead, and S. K. Jha, “Discovering rare behaviours in stochastic differential equations using decision procedures: applications to a minimal cell cycle model,” International Journal of Bioinformatics Research and Applications 2, vol. 10, no. 4-5, pp. 540–558, 2014.
F. Hussain, N. Deo, and S. K. Jha, “Early Adoption: High-Performance Computing for Big Data Introducing parallel programming and big data in the core algorithms curriculum,” in Procceedings of the 4th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar 2014), 2014.
F. Hussain, A. Ramanathan, L. L. Pullum, and S. K. Jha, “ EpiSpec: A formal specification language for parameterized agent-based models against epidemiological ground truth ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on, 2014, pp. 1–6.
A. Velasquez and S. K. Jha, “ Parallel computing using memristive crossbar networks: Nullifying the processor-memory bottleneck ,” in Design & Test Symposium (IDT), 2014 9th International, 2014, pp. 147–152.Abstract

We are quickly reaching an impasse to the number of transistors that can be squeezed onto a single chip. This has led to a scramble for new nanotechnologies and the subsequent emergence of new computing architectures capable of exploiting these nano-devices. The memristor is a promising More-than- Moore device because of its unique ability to store and manipulate data on the same device. In this paper, we propose a flexible architecture of memristive crossbar networks for computing Boolean formulas. Our design nullifies the gap between processor and memory in von Neumann architectures by using the crossbar both for the storage of data and for performing Boolean com- putations. We demonstrate the effectiveness of our approach on practically important computations, including parallel Boolean matrix multiplication.

We are quickly reaching an impasse to the number of transistors that can be squeezed onto a single chip. This has led to a scramble for new nanotechnologies and the subsequent emergence of new computing architectures capable of exploiting these nano-devices. The memristor is a promising More-than- Moore device because of its unique ability to store and manipulate data on the same device. In this paper, we propose a flexible architecture of memristive crossbar networks for computing Boolean formulas. Our design nullifies the gap between processor and memory in von Neumann architectures by using the crossbar both for the storage of data and for performing Boolean com- putations. We demonstrate the effectiveness of our approach on practically important computations, including parallel Boolean matrix multiplication.

F. Hussain, C. J. Langmead, Q. Mi, J. Dutta-Moscato, Y. Vodovotz, and S. K. Jha, “ Parameter discovery for stochastic computational models in systems biology using Bayesian model checking ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on, 2014, pp. 1–2.
F. Hussain, S. K. Jha, S. Jha, and C. J. Langmead, “ Parameter discovery in stochastic biological models using simulated annealing and statistical model checking ,” International Journal of Bioinformatics Research and Applications 2, vol. 10, no. 4-5, pp. 519–539, 2014.
F. Hussain, A. Velasquez, E. Sassano, and S. K. Jha, “ Putting humpty-dumpty together: Mining causal mechanistic biochemical models from big data ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on, 2014, pp. 1–6.
2013
N. Deo and S. K. Jha, “Big-Data-Driven Control Strategies for Complex Networks,” J Inform Tech Softw Eng, vol. 3, pp. e117, 2013.
N. Deo, S. K. Jha, F. Hussain, and M. Vasudevan, “Introducing parallel programming across the undergraduate curriculum through an interdisciplinary course on computational modeling,” in Procceedings of the Third NSF/TCPP Workshop on Parallel and Distributed Computing Education, Boston, MA, 2013.
2012
A. R. Kolli, et al., “ A computational metabolic model of the NG108-15 cell for high content drug screening with electrophysiological readout ,” in Proceedings of the ACM Conference on Bioinformatics, Computational Biology and Biomedicine, 2012, pp. 530–532.
A. K. Ghosh, F. Hussain, S. K. Jha, C. J. Langmead, and S. Jha, “Decision procedure based discovery of rare behaviors in stochastic differential equation models of biological systems,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on, 2012, pp. 1–6.
S. K. Jha and C. J. Langmead, “ Exploring behaviors of stochastic differential equation models of biological systems using change of measures ,” BMC bioinformatics, vol. 13, no. 5, pp. S8, 2012.

BEST PAPER AWARD

F. Hussain, R. G. Dutta, S. K. Jha, C. J. Langmead, and S. Jha, “Parameter discovery for stochastic biological models against temporal behavioral specifications using an sprt based metric for simulated annealing,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on, 2012, pp. 1–6.
S. K. Jha and A. Ramanathan, “ Quantifying uncertainty in epidemiological models ,” in BioMedical Computing (BioMedCom), 2012 ASE/IEEE International Conference on, 2012, pp. 80–85.
S. K. Jha, R. G. Dutta, C. J. Langmead, S. Jha, and E. Sassano, “Synthesis of insulin pump controllers from safety specifications using bayesian model validation,” International journal of bioinformatics research and applications, vol. 8, no. 3-4, pp. 263–285, 2012.
2011
S. K. Jha and G. Sukthankar, “ Modeling and verifying intelligent automotive cyber-physical systems ,” in Proceedings of the NIST/NSF/USCAR Workshop on Developing Dependable and Secure Automotive Cyber-Physical Systems from Components, 2011.
S. Jha, et al., “ Parameter estimation and synthesis for systems biology: New algorithms for nonlinear and stochastic models ,” Journal of critical care, vol. 26, no. 2, pp. e8, 2011.
S. K. Jha and C. J. Langmead, “Poster: Synthesis of biochemical models,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2011 IEEE 1st International Conference on, 2011, pp. 248–248.
S. K. Jha and C. J. Langmead, “ Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement ,” Theoretical Computer Science, vol. 412, no. 21, pp. 2162–2187, 2011.
S. K. Jha, C. J. Langmead, S. Mohalik, and S. Ramesh, “ When to stop verification?: Statistical trade-off between expected loss and simulation cost ,” in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011, 2011, pp. 1–6.
2010
S. K. Jha, “Model validation and discovery for complex stochastic systems,” 2010.
K. Mehra, S. K. Rajamani, A. P. Sistla, and S. K. Jha, “ Object relational map verification system ”, US Patent: US7702695 B2, 2010.

US Patent 7,702,695

2009
S. K. Jha, E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer, and P. Zuliani, “ A bayesian approach to model checking biological systems ,” in International Conference on Computational Methods in Systems Biology, 2009, pp. 218–234.
S. K. Jha, E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer, and P. Zuliani, “Statistical model checking for complex stochastic models in systems biology,” 2009.
C. J. Langmead and S. K. Jha, “ Symbolic approaches for finding control strategies in Boolean networks ,” Journal of Bioinformatics and Computational Biology, vol. 7, no. 02, pp. 323–338, 2009.Abstract

We present algorithms for finding control strategies in Boolean Networks (BN). Our approach uses symbolic techniques from the field of model checking. We show that despite recent hardness-results for finding control policies, a model checking-based approach is often capable of scaling to extremely large and complex models. We demonstrate the effectiveness of our approach by applying it to a BN model of embryogenesis in D. melanogaster with 15,360 Boolean variables.

2008
G. Frehse, S. K. Jha, and B. H. Krogh, “ A counterexample-guided approach to parameter synthesis for linear hybrid automata ,” in International Workshop on Hybrid Systems: Computation and Control, 2008, pp. 187–200.Abstract

Our goal is to find the set of parameters for which a given linear hybrid automaton does not reach a given set of bad states. The problem is known to be semi-solvable (if the algorithm terminates the result is correct) by introducing the parameters as state variables and computing the set of reachable states. This is usually too expensive, how- ever, and in our experiments only possible for very simple systems with few parameters. We propose an adaptation of counterexample-guided abstraction refinement (CEGAR) with which one can obtain an under- approximation of the set of good parameters using linear programming. The adaptation is generic and can be applied on top of any CEGAR method where the counterexamples correspond to paths in the concrete system. For each counterexample, the cost incurred by underapproximat- ing the parameters is polynomial in the number of variables, parameters, and the length of counterexample. We identify a syntactic condition for which the approach is complete in the sense that the underapproxima- tion is empty only if the problem has no solution. Experimental results are provided for two CEGAR methods, a simple discrete version and iterative relaxation abstraction (IRA), both of which show a drastic im- provement in performance compared to standard reachability.

S. K. Jha, “ d-ira: A distributed reachability algorithm for analysis of linear hybrid automata ,” in International Workshop on Hybrid Systems: Computation and Control, 2008, pp. 618–621.Abstract

This paper presents the design of a novel distributed algo- rithm d-IRA for the reachability analysis of linear hybrid automata. Re- cent work on iterative relaxation abstraction (IRA) is leveraged to dis- tribute the reachability problem among multiple computational nodes in a non-redundant manner by performing careful infeasibility analysis of linear programs corresponding to spurious counterexamples. The d-IRA algorithm is resistant to failure of multiple computational nodes. The ex- perimental results provide promising evidence for the possible successful application of this technique.

S. K. Jha and S. Jha, “Random relaxation abstractions for bounded reachability analysis of linear hybrid automata: Distributed randomized abstractions in model checking,” in High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE, 2008, pp. 147–153.
S. Jha and S. K. Jha, “Randomization based probabilistic approach to detect trojan circuits,” in High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE, 2008, pp. 117–124.
E. M. Clarke, J. R. Faeder, C. J. Langmead, L. A. Harris, S. K. Jha, and A. Legay, “ Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway ,” in International Conference on Computational Methods in Systems Biology, 2008, pp. 231–250.Abstract

We present an algorithm, called BioLab, for verifying tem- poral properties of rule-based models of cellular signalling networks.

BioLab models are encoded in the BioNetGen language, and prop- erties are expressed as formulae in probabilistic bounded linear temporal logic. Temporal logic is a formalism for representing and reasoning about propositions qualified in terms of time. Properties are then verified using sequential hypothesis testing on executions generated using stochastic simulation. BioLab is optimal, in the sense that it generates the mini- mum number of executions necessary to verify the given property. Bio- Lab also provides guarantees on the probability of it generating Type-I (i.e., false-positive) and Type-II (i.e., false-negative) errors. Moreover, these error bounds are pre-specified by the user. We demonstrate Bio- Lab by verifying stochastic effects and bistability in the dynamics of the T-cell receptor signaling network.

2007
K. K. Mehra, S. K. Rajamani, A. P. Sistla, and S. K. Jha, “Verification of Object Relational Maps,” in Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, London, England, UK, 2007, pp. 283–292. Publisher's Version
Verification of Object Relational Maps ,” in Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, , London, England, UK, 2007. Publisher's VersionAbstract

Enterprise software systems need to deal with two domi- nant data models. While object oriented languages (such as Java, C#, C++) are the dominant ways to write business logic, relational databases are the dominant ways to store data. Object-Relational (OR) maps are widely used to mediate between these two data models. We present a system to verify correctness of OR maps. We formulate simple correct- ness conditions for OR maps, and convert these conditions to validity of formulas in first order logic. We have built a verification tool called roundtrip that is able to both validate and find errors in OR maps.

C. J. Langmead and S. K. Jha, “ Predicting protein folding kinetics via temporal logic model checking ,” in International Workshop on Algorithms in Bioinformatics, 2007, pp. 252–264.Abstract

We present a novel approach for predicting protein folding kinetics using techniques from the field of model checking. This represents the first time model checking has been applied to a problem in the field of structural biology. The protein’s energy landscape is encoded sym- bolically using Binary Decision Diagrams and related data structures. Questions regarding the kinetics of folding are encoded as formulas in the temporal logic CTL. Model checking algorithms are then used to make quantitative predictions about the kinetics of folding. We show that our approach scales to state spaces as large as 1023 when using exact algo- rithms for model checking. This is at least 14 orders of magnitude larger than the number of configurations considered by comparable techniques. Furthermore, our approach scales to state spaces at least as large as 1032 unique configurations when using approximation algorithms for model checking. We tested our method on 19 test proteins. The quantitative predictions regarding folding rates for these test proteins are in good agreement with experimentally measured values, achieving a correlation coefficient of 0.87.

S. K. Jha, B. H. Krogh, J. E. Weimer, and E. M. Clarke, “ Reachability for linear hybrid automata using iterative relaxation abstraction ,” in International Workshop on Hybrid Systems: Computation and Control, 2007, pp. 287–300.Abstract

Procedures for analysis of linear hybrid automata (LHA) do not scale well with the number of continuous state variables in the model. This paper introduces iterative relaxation abstraction (IRA), a new method for reachability analysis of LHA that aims to improve scal- ability by combining the capabilities of current tools for analysis of low- dimensional LHA with the power of linear programming (LP) for large numbers of constraints and variables. IRA is inspired by the success of counterexample guided abstraction refinement (CEGAR) techniques in verification of discrete systems. On each iteration, a low-dimensional LHA called a relaxation abstraction is constructed using a subset of the continuous variables from the original LHA. Hybrid system reachabil- ity analysis then generates a regular language called the discrete path abstraction representing all possible counterexamples (paths to the bad locations) in the relaxation abstraction. If the discrete path abstraction is non-empty, a particular counterexample is selected and LP infeasibil- ity analysis determines if the counterexample is spurious using the con- straints along the path from the original high-dimensional LHA. If the counterexample is spurious, LP techniques identify an irreducible infeasi- ble subset (IIS) of constraints from which the set of continuous variables is selected for the the construction of the next relaxation abstraction. IRA stops if the discrete path abstraction is empty or a legitimate coun- terexample is found. The effectiveness of the approach is illustrated with an example.

2006
S. Jiang, T. E. Fuhrman, and S. K. Jha, “ Model checking for fault explanation ,” in Decision and Control, 2006 45th IEEE Conference on, 2006, pp. 404–409.Abstract

Model checking is very effective at finding out even subtle faults in system designs. A counterexample is usually generated by model checking algorithms when a system does not satisfy the given specification. However, a counterexample is not always helpful in explaining and isolating faults in a system when the counterexample is very long, which is usually the case for large scale systems. As such, there is a pressing need to develop fault explanation and isolation techniques. In this paper, we present a new approach for the fault explanation and isolation in discrete event systems with LTL (linear-time temporal logic) specifications. The notion of fault seed is introduced to characterize the cause of a fault. The identification of the fault seed is further reduced to a model checking problem. An algorithm is obtained for the fault seed identification. An example is provided to demonstrate the effectiveness of the approach developed.

C. J. Langmead, S. K. Jha, and E. M. Clarke, “ Temporal-logics as query languages for dynamic Bayesian networks: application to D. melanogaster embryo development ,” 2006.Abstract

This paper introduces novel techniques for exact and approximate inference in Dynamic Bayesian Networks (DBNs) based on algorithms, data structures, and formalisms from the field of model checking. Model checking comprises a family of techniques from for formally verifying systems of concurrent reactive processes. We discuss: i) the use of temporal logics as a query language for inference over DBNs; ii) translation of DBNs into probabilistic reactive modules; and iii) the use of symbolic data structures and algorithms for deciding complex stochastic temporal logic formu- las. We demonstrate the effectiveness of these new algorithms by examining the behavior of an enhanced expression model of embryogenesis in D. melanogaster. In particular, we converted an existing deterministic developmental model over a one-dimensional arrays of cells into a stochas- tic model over a two dimensional array of cells. Our results confirm that the rules which govern the one-dimensional model also display wild-type expression patterns in the two-dimensional case within certain parameter bounds.

2005
A. Fehnker, E. Clarke, S. K. Jha, and B. Krogh, “ Refining abstractions of hybrid systems using counterexample fragments ,” in International Workshop on Hybrid Systems: Computation and Control, 2005, pp. 242–257.Abstract

Counterexample guided abstraction refinement, a powerful technique for verifying properties of discrete-state systems [4, 9] has been extended recently to hybrid systems verification [1, 3]. Unlike in discrete systems, however, estab- lishing the successor relation for hybrid systems can be a fairly expensive step since it requires evaluation and overapproximation of the continuous dynamics. In [3] it has been observed that it is often sufficient to consider fragments of counterexamples rather than complete counterexamples. In this paper we further develop the idea of fragments. We extend the notion of cut sets in network flows to cutting sets of fragments in abstractions. Cutting sets of fragments are then uses guide the abstraction refinement in order to prove safety properties for hy- brid systems.

E. Clarke, A. Fehnker, S. K. Jha, and H. Veith, “ Temporal logic model checking ,” in Handbook of Networked and Embedded Control Systems, Springer, 2005, pp. 539–558.Abstract

Errors in safety-critical systems such as embedded controllers may have drastic consequences and can even endanger human life. It is therefore crucially important to verify the correctness of such systems in a logically precise manner during system design itself. This chapter is an introduction to model checking—an automated and practically successful approach for the formal verification of the correctness of hardware and software systems.