Publications

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

 

icrc2017.pdf
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, 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. 

fps2017.pdf
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. 

 

EMSOFT2017_JHA.pdf
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. 

 

adversarialattacksnatural.pdf
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. 

 

ornl_tr_adversarial.pdf
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.

flowcytometry_bmcbioinformatics2017.pdf
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.

feynmangrandprize_nanoarch2017.pdf
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. 

 

3d_reram_iscas_2017.pdf
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. ieeenano2017_JHA.pdf
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. 

 

 

MLnFM_iscas2017.pdf
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. 

 

crossbarsusingformalmethods.pdf
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. nca2016_jha.pdf
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. patent2016_memristorcomputing_jha.pdf

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. iscas2016_flowmemristor_jha_01.pdf
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. date2016_adversarialexample_jha_01.pdf
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. iscas2016_parallel_memristor_jha.pdf
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. 

 

bmcbioinformatics_discovery.pdf

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. 

 

nanoarch-2.pdf
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. 

 

iccd2015.pdf
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. 

 

idt2014.pdf
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.
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. cmsb09_bayesianstatisticalmodelchecking_jha.pdf
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. 

 

2009_jbcb_and_apbc_paper_underlined.pdf
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. 

 

2008_hscc_paper_and_acceptance_underlined.pdf
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. 

 

2008_hscc_paper_and_acceptance_underlined.pdf
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. 

 

2008_cmsb_underlined.pdf
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. 

 

2007_sefm_underlined.pdf
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. 

 

2007_wabi_underlined.pdf
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. 

 

2007_hscc_underlined.pdf
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. 

 

2006_cdc_paper_and_acceptance_underlined.pdf
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. 

 

2006_cmu_research_showcase_underlined.pdf
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. 

 

2006_hscc_underlined.pdf
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. 

 

book2005_underlined.pdf