Publications

Export 52 results:
Sort by: [ Year  (Desc)]
2016
Hassan, A., and S. K. Jha, "Automated Synthesis of Stochastic Computational Elements using Decision Procedures", IEEE International Symposium on Circuits and Systems (ISCAS), Montreal, Canada, May 22-25, 2016. 1678_2301_b3p-w4_c.pdf
Alamgir, Z., N. Cady, A. Velasquez, and S. K. Jha, "Flow-based Computing on Nanoscale Crossbars: Design and Implementation of Full Adders", IEEE International Symposium on Circuits and Systems (ISCAS)), Montreal, Canada, May 22-25, 2016. 1870_2223_b4l-k2_c.pdf
Velasquez, A., and S. K. Jha, "Parallel Boolean Matrix Multiplication in Linear Time using Rectifying Memristors", IEEE International Symposium on Circuits and Systems (ISCAS), Montreal, Canada, May 22-25, 2016. 1874_1674_b4l-k3_c.pdf
Jha, S. K., D. Rodriguez, J. V. E. Nostrand, and A. Velasquez, Computation of boolean formulas using sneak paths in crossbar computing, : UNIVERSITY OF CENTRAL FLORIDA RESEARCH FOUNDATION, INC., 2016. pat9319047.pdf
Jha, S. K., A. Ramanathan, L. Pullum, F. Hussain, and D. Chakraborty, "Integrating symbolic and statistical methods for testing intelligent systems: Applications to machine learning and computer vision", Design Automation and Test in Europe (DATE), Dresden, Germany, 2016. Abstract0954.pdf

Embedded intelligent systems ranging from tiny implantable biomedical devices to large swarms of autonomous unmanned aerial systems are increasingly becoming pervasive in peoples’ daily lives. While we depend on the flawless functioning of such intelligent systems, and often take their behavioral correctness and safety for granted, it is notoriously difficult to generate test cases that expose subtle errors in the implementations of machine learning algorithms. Hence, the validation of intelligent systems is usually achieved by studying their behavior on representative data sets, using methods such as cross-validation and bootstrapping. In this paper, we present a new testing methodology for studying the correctness of intelligent systems. Our approach uses symbolic decision procedures with statistical hypothesis testing to create a new distance-theoretic abstraction of the k-means clustering algorithm that avoids the need to perform expensive computations of distances between pairs of points in a large space. We demonstrate the success of our method on two prototypical examples: k-means clustering as implemented in the R toolkit and human detection as implemented in the OpenCV library. We employ our technique to identify subtle bugs (such as bit flips) in implementations of the k-means algorithm that are not readily detected by standard methods such as cross-validation. We also use our algorithm to study an implementation of the human detection algorithm built using the OpenCV open-source computer vision library. We show that the OpenCV’s human detection implementation can fail to detect humans in perturbed video frames even when the perturbations are so small that the corresponding frames look identical to the human eye.

2015
Jha, S. K., M. Mukund, R. Saha, and P. S. Thiagarajan, "Distributed Markov Chains", 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2015. Abstractjha_sumit_distributed_markov_chains.pdfpaper_16-2.pdf

n/a

Petkova, A., C. Hughes, N. Deo, and S. K. Jha, "Accelerating the Distributed Simulations of Agent-Based Models using Community Detection (Abstract)", IEEE HPEC, Accepted and presented as a poster: http://www.ieee-hpec.org/2015/copy/agendatext.html but we chose not to publish it on the conference website, 2015. accelerating-distributed-simulations-2.pdf
Hussain, F., C. J. Langmead, Q. Mi, J. Dutta-Muscato, Y. Vodavotz, and S. K. Jha, "Automated parameter estimation for biological models using Bayesian statistical model checking", BMC Bioinformatics, pp. in press, 2015. parameter_estimation_agent_based_models.pdf
Velasquez, A., and S. K. Jha, "Automated Synthesis of Crossbars for Nanoscale Computing using Formal Methods", ACM/IEEE NanoArch, 2015. Abstract

Since the fabrication of nanoscale memristors by HP Labs in 2008, there has been a sustained interest in the use of crossbars of nanoscale memristors for digital storage and neuromorphic computing. However, the same success has not been replicated in the use of crossbars for performing generalpurpose computations that can support the existing software infrastructure originally designed for von Neumann architectures. One of the fundamental challenges facing the exploitation of nanoscale memristor crossbars is the existence of sneak paths. It has been shown that sneak paths can be used to perform Boolean computations in crossbars. However, the human mind can be easily overwhelmed by the large number of sneak paths that may arise in a crossbar. It is not surprising that the size of manually-designed crossbars has been too large for practical applications. In this paper, we demonstrate how formal methods can be used to automatically synthesize compact crossbar designs that employ the sneak paths phenomena as a fundamental design primitive to evaluate Boolean formula.

Velasquez, A., and S. K. Jha, "Fault-Tolerant In-Memory Crossbar Computing using Quantified Constraint Solving", 33rd IEEE International Conference on Computer Design (ICCD) 2015, New York City, NY, 2015. Abstractsumitkumarjhaiccd2015.pdf

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.

Velasquez, A., and S. K. Jha, "Parallel Computing using Memristive Crossbar Networks: Nullifying the Processor-Memory Bottleneck", 9th IEEE International Design and Test (IDT 2015), 2015. Abstractidt.pdf

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 computations. We demonstrate the effectiveness of our approach on practically important computations, including parallel Boolean matrix multiplication.

Jha, S. K., "SANJAY: Synthesizing Visualizations of Flow Cytometry Data using Symbolic Decision Procedures", IEEE International Conference on Computational Advances in Bio and Medical Sciences, Miami, FL, pp. Accepted, 2015.
2014
Hussain, F., 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 (Best Paper Award)", Proceedings of the 4th IEEE International Conference on Computational Advances in Bio and Medical Sciences (ICCABS): IEEE, pp. 1–6, June, 2014. Abstracticcabs2014_submission_80.pdf

n/a

Ghosh, A. K., 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, vol. 10, no. 4/5, pp. 540-558, 2014. Abstract

n/a

Hussain, F., 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, vol. 10, no. 4/5, pp. 519-539, 2014. Abstract

n/a

2013
Jha, S. K., and N. Deo, "Discriminative Stochastic Models for Complex Networks Derived from Flow Cytometry Big Data", Forty-Fourth Southeastern International Conference on Combinatorics, Graph Theory, and Computing, Boca Raton, March 4-8, 2013. Abstractcommunity_detection_in_flow_cytometry_networks_deo_jha_petkova.pdf

Flow cytometry measures multiple features of thousands of cells in a sample, and thus produces a massive high-dimensional data set that must be analyzed to decide whether a given patient has cancer or not. Currently, human experts use two-dimensional visualizations of data sets of up to six dimensions and perform this process of discriminating between cancer and normal patients using their own expertise. However, modern flow cytometry machines can produce massive high-dimensional (20 or more) data sets, and their manual analysis quickly becomes infeasible. In this paper, we propose the use of complex network models and their topological properties for discriminating between cancer and normal patients. In particular, each node in the complex network corresponds to the measurements obtained from a single cell and an edge between two nodes exists if the Euclidean distance between them is smaller than a threshold. The evolution of the network through time is derived by studying periodically acquired patient samples. By constructing such complex network models for multiple normal patients, we develop a stochastic generative model that describes the flow cytometry data for normal patients. In particular, topological properties such as number of connected components, edge density, number of clusters, etc. are studied. The goal of the stochastic generative modeling is to capture the natural diversity that occurs in the normal patient population (age, race, gender, BMI), and thereby compute the probability that a given flow cytometry sample does not arise from this stochastic generative model. Rare behavior identification algorithms will then be employed to compute the probability that a given flow cytometry sample indicates the presence of cancer in a patient.

Deo, N., F. Hussain, S. K. Jha, and M. Vasudevan, "Introducing parallel programming across the undergraduate curriculum through an interdisciplinary course on computational modeling", IEEE Technical Committee on Parallel Programming, Boston, MA, July, 2013. Slides
Deo, N., and S. K. Jha, "Big-Data-Driven Control Strategies for Complex Networks", Journal of Information Technology & Software Engineering, 2013. Abstractbigdata-2.pdf

n/a

2012
Kolli, A. R., F. Sommerhage, P. Molnar, J. E. Hood, J. J. Jenkins, F. Hussain, A. K. Ghosh, S. K. Jha, and J. J. Hickman, "A computational metabolic model of the NG108-15 cell for high content drug screening with electrophysiological readout", Proceedings of the ACM Conference on Bioinformatics, Computational Biology and Biomedicine: ACM, pp. 530-532, 2012. Abstract

n/a

Jha, S. K., and C. J. Langmead, "Exploring behaviors of stochastic differential equation models of biological systems using change of measures", BMC bioinformatics, vol. 13, issue Suppl 5: BioMed Central Ltd, pp. S8, 2012. Abstract

n/a

Ghosh, A. K., 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", Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on: IEEE, pp. 1-6, 2012. Abstract
n/a
Hussain, F., 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", Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on: IEEE, pp. 1-6, 2012. Abstract
n/a
Jha, S. K., and A. Ramanathan, "Quantifying Uncertainty in Epidemiological Models", BioMedical Computing (BioMedCom), 2012 ASE/IEEE International Conference on: IEEE, pp. 80-85, 2012. Abstract
n/a
Jha, S. K., 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, issue 3: Inderscience Publishers, pp. 263-285, 2012. Abstract
n/a
2011
Jha, S. K., and C. J. Langmead, "Exploring behaviors of sde models of biological systems using change of measures", Computational Advances in Bio and Medical Sciences (ICCABS), 2011 IEEE 1st International Conference on: IEEE, pp. 111-116, 2011. Abstract
n/a
Jha, S. K., and G. Sukthankar, "Modeling and Verifying Intelligent Automotive Cyber-Physical Systems", Proceedings of the NIST/NSF/USCAR Workshop on Developing Dependable and Secure Automotive Cyber-Physical Systems from Components, 2011. Abstract
n/a
Jha, S., A. Donze, R. Khandpur, J. Dutta-Moscato, Q. Mi, Y. Vodovotz, G. Clermont, and C. Langmead, "Parameter estimation and synthesis for systems biology: New algorithms for nonlinear and stochastic models", Journal of critical care, vol. 26, issue 2: WB Saunders, pp. e8, 2011. Abstract
n/a
Jha, S. K., and C. J. Langmead, "Poster: Synthesis of biochemical models", Computational Advances in Bio and Medical Sciences (ICCABS), 2011 IEEE 1st International Conference on: IEEE, pp. 248-248, 2011. Abstract
n/a
Jha, S. K., 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, issue 21: Elsevier, pp. 2162-2187, 2011. Abstract
n/a
Jha, S. K., C. J. Langmead, S. Mohalik, and S. Ramesh, "When to stop verification?: Statistical trade-off between expected loss and simulation cost", Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011: IEEE, pp. 1-6, 2011. Abstract
n/a
2010
Mehra, K., S. K. Rajamani, A. P. Sistla, and S. K. Jha, Object relational map verification system, : Google Patents, 2010. Abstract
n/a
2009
Jha, S. K., E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer, and P. Zuliani, "A bayesian approach to model checking biological systems", Computational Methods in Systems Biology: Springer Berlin Heidelberg, pp. 218-234, 2009. Abstract
n/a
Jha, S. K., E. M. Clarke, C. J. Langmead, A. Legay, A. Platzer, and P. Zuliani, Statistical Model Checking for Complex Stochastic Models in Systems Biology, , 2009. Abstract
n/a
Langmead, C. J., and S. K. Jha, "Symbolic approaches for finding control strategies in Boolean networks", Journal of Bioinformatics and Computational Biology, vol. 7, issue 02: Imperial College Press, pp. 323-338, 2009. Abstract
n/a
2008
Frehse, G., S. K. Jha, and B. H. Krogh, "A counterexample-guided approach to parameter synthesis for linear hybrid automata", Hybrid Systems: Computation and Control: Springer Berlin Heidelberg, pp. 187-200, 2008. Abstract
n/a
Jha, S. K., "d-ira: A distributed reachability algorithm for analysis of linear hybrid automata", Hybrid Systems: Computation and Control: Springer Berlin Heidelberg, pp. 618-621, 2008. Abstract
n/a
Jha, S. K., and S. Jha, "Random Relaxation Abstractions for Bounded Reachability Analysis of Linear Hybrid Automata: Distributed Randomized Abstractions in Model Checking", High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE: IEEE, pp. 147-153, 2008. Abstract
n/a
Jha, S., and S. K. Jha, "Randomization based probabilistic approach to detect trojan circuits", High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE: IEEE, pp. 117-124, 2008. Abstract
n/a
Clarke, E. M., 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", Computational Methods in Systems Biology: Springer Berlin Heidelberg, pp. 231-250, 2008. Abstract
n/a
2007
Langmead, C. J., and S. K. Jha, "Predicting protein folding kinetics via temporal logic model checking", Algorithms in Bioinformatics: Springer Berlin Heidelberg, pp. 252-264, 2007. Abstract
n/a
Jha, S. K., B. H. Krogh, J. E. Weimer, and E. M. Clarke, "Reachability for linear hybrid automata using iterative relaxation abstraction", Hybrid Systems: Computation and Control: Springer Berlin Heidelberg, pp. 287-300, 2007. Abstract
n/a
Li, X., S. Jha Aanand, and L. Bu, "Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming", Electronic Notes in Theoretical Computer Science, vol. 174, issue 3: Elsevier, pp. 57-70, 2007. Abstract
n/a
Mehra, K. K., S. K. Rajamani, S. K. Jha, and A. P. Sistla, "Verification of object relational maps", Software Engineering and Formal Methods, 2007. SEFM 2007. Fifth IEEE International Conference on: IEEE, pp. 283-292, 2007. Abstract
n/a
2006
Jiang, S., T. E. Fuhrman, and S. K. Jha, "Model checking for fault explanation", Decision and Control, 2006 45th IEEE Conference on: IEEE, pp. 404-409, 2006. Abstract
n/a
2005
Fehnker, A., E. Clarke, S. K. Jha, and B. Krogh, "Refining abstractions of hybrid systems using counterexample fragments", Hybrid Systems: Computation and Control: Springer Berlin Heidelberg, pp. 242-257, 2005. Abstract
n/a
Clarke, E., A. Fehnker, S. K. Jha, and H. Veith, "Temporal logic model checking", Handbook of Networked and Embedded Control Systems: Birkhäuser Boston, pp. 539-558, 2005. Abstract
n/a