Fingerprints are widely used for personal identification due to their singularity and immutability. Fingerprint recognition systems verify the identity of individuals and provide access to highly-secure personal information in various commercial applications. However, with modern advancements in deep learning, fingerprint recognition systems could be attacked, rendering the personal information contained within in a highly vulnerable state. In this paper, we propose a novel approach to attack a transfer learning-based fingerprint recognition system, which is pre-trained on the ImageNet database. For experimental analysis, twelve image recognition models are considered: MobileNetV2, MobileNet, NASNetMobile, DenseNet121, DenseNet169, DenseNet201, Xception, InceptionV3, ResNet50, NASNetLarge, VGG16, and VGG19. Among them, MobileNetV2 is the latest image recognition model, but VGG16 is one of the largest used in current state-of-the-art fingerprint recognition systems. We have attacked this system using our approach on ATVS and CASIA fingerprint datasets. The image quality difference between real and attacked fingerprints calculated using image quality assessment parameters is less than 3.36%. In addition, the core has the same pixel coordinates for real and attacked fingerprints when measured using VeriFinger SDK.

%B International Conference on Biometrics %G eng %0 Conference Paper %B IEEE International Symposium on Circuits and Systems %D 2019 %T Spatially Efficient in-Memory Addition Through Destructive and Non-Destructive Operations %A Benjamin Shaia %A Velasquez, Alvaro %A Submit Kumar Jha %B IEEE International Symposium on Circuits and Systems %I IEEE %C Sapporo, Japan %G eng %0 Conference Paper %B 16th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) %D 2018 %T Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems %A Jha, Susmit %A Raj, Sunny %A Jha, Sumit K. %A Shankar, Natarajan %X

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.

%B 16th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) %I Springer %C Beijing, China %G eng %0 Conference Paper %B ACM Symposium on Parallelism in Algorithms and Architectures %D 2018 %T Parallel Transitive Closure Within 3D Crosspoint Memory %A Velasquez, Alvaro %A Jha, Sumit Kumar %B ACM Symposium on Parallelism in Algorithms and Architectures %I ACM %C Vienna, Austria %G eng %0 Journal Article %J Transactions on Circuits and Systems (TCAS) II %D 2018 %T Free Binary Decision Diagram Based Synthesis of Compact Crossbars for in-Memory Computing of Boolean Functions %A Hassen, Amad Ul %A Chakraborty, Dwaipayan %A Jha, Sumit Kumar %B Transactions on Circuits and Systems (TCAS) II %G eng %0 Conference Proceedings %B IEEE International Conference on Bioinformatics and Biomedicine %D 2018 %T Calibration of Rule-Based Stochastic Biochemical Models using Statistical Model Checking %A Arfeen Khalid %A Jha, Sumit Kumar %X

Computational modeling of biochemical networks assists in understanding the functioning of a biochemical process as well as enables in silico experimentation. However, such models are often stochastic in nature and contain unknown parameters that must be estimated against expert behavioral specifications. In this paper, we present a new statistical model checking approach for calibrating rule-based stochastic biochemical models such that the calibrated model satisfies a given behavioral temporal logic specification. Our approach computes a distribution of aquantitative tightness metric describing how well a specification is satisfied by a parameterized rule-based stochastic biochemical model. Then, sequential selection of the larger of the means of two such distributions is used to guide a simulated annealing based search for the correctly calibrated model that satisfies the given behavioral temporal logic specification. Our experimental results demonstrate the successful calibration of a rule-based T- cell receptor model while achieving a significant speedup in time.

%B IEEE International Conference on Bioinformatics and Biomedicine %C Madrid, Spain %G eng %0 Conference Proceedings %B International Conference on Bioinformatics and Biomedicine (BIBM) %D 2018 %T Calibration of Rule-Based Stochastic Biochemical Models using Statistical Model Checking %A Arfeen Khalid %A Jha, Sumit K %B International Conference on Bioinformatics and Biomedicine (BIBM) %C Madrid, Spain %G eng %0 Conference Paper %B 8th IEEE International Conference on Computational Advances in Bio and medical Sciences (ICCABS) %D 2018 %T Parameter Estimation of Stochastic Biochemical Models using Multiple Hypothesis Testing %A Arfeen Khalid %A Jha, Sumit Kumar %B 8th IEEE International Conference on Computational Advances in Bio and medical Sciences (ICCABS) %I IEEE %G eng %0 Conference Paper %B IEEE International Conference on Computer Design (ICCD) %D 2018 %T 3D Crosspoint Memory as a Parallel Architecture for Computing Network Reachability %A Velasquez, Alvaro %A Jha, Sumit Kumar %XWe 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.

%B IEEE International Conference on Computer Design (ICCD) %I IEEE %G eng %0 Conference Paper %B 14th IEEE / ACM International Symposium on Nanoscale Architectures (NANOARCH) %D 2018 %T Free BDD based Computer-aided Design of Compact Memristor Crossbars for in-Memory Computing %A Hassen, Amad Ul %A Jha, Sumit Kumar %B 14th IEEE / ACM International Symposium on Nanoscale Architectures (NANOARCH) %I IEEE/ACM %C Athens, Greece %G eng %0 Conference Paper %B 8th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar-18) co-located with the 32nd IEEE International Parallel & Distributed Processing Symposium, %D 2018 %T Predicting Success in Undergraduate Parallel Programming via Probabilistic Causality Analysis %A Raj, Sunny %A Jha, Sumit K %X

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.

%B 8th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar-18) co-located with the 32nd IEEE International Parallel & Distributed Processing Symposium, %I IEEE %C Vancouver, Canada %G eng %0 Conference Paper %B DOE ASCR Workshop on Scientific Machine Learning %D 2018 %T Mathematically Rigorous Verification and Validation of Scientific Machine Learning %A Pullum, Laura L %A Steed, Chad %A Ramanathan, Arvind %A Jha, Sumit K %B DOE ASCR Workshop on Scientific Machine Learning %G eng %0 Conference Paper %B International Symposium on Circuits and Systems (ISCAS) %D 2018 %T Free Binary Decision Diagram Based Synthesis of Compact Crossbars for in-Memory Computing of Boolean Functions %A Hassen, Amad Ul %A Jha, Sumit Kumar %X

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.

%B International Symposium on Circuits and Systems (ISCAS) %I IEEE %C Florence, Italy %G eng %0 Conference Paper %B Design, Automation, and Test in Europe (DATE) %D 2018 %T Fault-Tolerant In-Memory Computing Using Paths-Based Logic and Heterogeneous Components %A Velasquez, Alvaro %A Jha, Sumit K %X

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.

%B Design, Automation, and Test in Europe (DATE) %I IEEE %C Dresden, Germany %G eng %0 Conference Paper %B The 10th International Symposium on Foundations and Practice of Security (FPS 2017) %D 2017 %T SATYA: Defending against Adversarial Attacks using Statistical Hypothesis Testing %A Raj, Sunny %A Jha, Sumit Kumar %A Pullum, Laura L %A Ramanathan, Arvind %X

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.

%B The 10th International Symposium on Foundations and Practice of Security (FPS 2017) %I Springer %C Nancy, France. (BEST PAPER AWARD) %G eng %0 Conference Paper %B IEEE International Conference on Rebooting Computing 2017 %D 2017 %T In-Memory Execution of Compute Kernels using Flow-based Memristive Crossbar Computing %A Chakraborty, Dwaipayan %A Raj, Sunny %A Julio Cesar Gutierrez %A Troyle Thomas %A Jha, Sumit Kumar %X

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.

%B IEEE International Conference on Rebooting Computing 2017 %I IEEE %C Washington D.C. %8 9 November %G eng %0 Conference Paper %B ACM SIGBED International Conference on Embedded Software (EMSOFT) %D 2017 %T Testing Autonomous Cyber-Physical Systems using Fuzzing Features Derived from Convolutional Neural Networks %A Raj, Sunny %A Ramanathan, Arvind %A Pullum, Laura L %A Jha, Sumit Kumar %X

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.

%B ACM SIGBED International Conference on Embedded Software (EMSOFT) %I ACM %C Seoul, South Korea %G eng %0 Conference Paper %B Tenth International Conference on Contemporary Computing %D 2017 %T Adversarial attacks on computer vision algorithms using natural perturbations %A Ramanathan, Arvind %A Pullum, Laura L %A Raj, Sunny %A Husein, Zubir %A Pattanaik, Sumanta %A Jha, Sumit Kumar %X

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.

%B Tenth International Conference on Contemporary Computing %C New Delhi, India %P in press %G eng %0 Government Document %D 2017 %T Statistical Hypothesis Testing using CNN Features for Synthesis of Adversarial Counterexamples to Human and Object Detection Vision Systems %A Raj, Sunny %A Jha, Sumit Kumar %A Pullum, Laura L %A Ramanathan, Arvind %X

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.

%B Oak Ridge National Laboratory Technical Report %V ORNL/LTR-2017/118 %G eng %U https://info.ornl.gov/sites/publications/Files/Pub73419.pdf %0 Journal Article %J BMC Bioinformatics %D 2017 %T A theorem proving approach for automatically synthesizing visualizations of flow cytometry data %A Raj, Sunny %A Hussain, Faraz %A Husein, Zubir %A Torosdagli, Neslisah %A Turgut, Damla %A Deo, Narsingh %A Pattanaik, Sumanta %A Chang, Chung-Che (Jeff) %A Jha, Sumit Kumar %X

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.

%B BMC Bioinformatics %V 18 %P 245 %G eng %U http://dx.doi.org/10.1186/s12859-017-1662-4 %N 8 %R 10.1186/s12859-017-1662-4 %0 Conference Paper %B 13th ACM/IEEE International Symposium on Nanoscale Architectures %D 2017 %T A Compact 8-bit Adder Design using In-Memory Memristive Computing: Towards Solving the Feynman Grand Prize Challenge %A Chakraborty, Dwaipayan %A Raj, Sunny %A Jha, Sumit K. %K Nanoscale Computing %XWe 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.

%B 13th ACM/IEEE International Symposium on Nanoscale Architectures %I IEEE/ACM %C Newport, USA %P in press %G eng %0 Conference Paper %B IEEE International Symposium on Circuits and Systems (ISCAS) %D 2017 %T Computation of Boolean Matrix Chain Products in 3D ReRAM %A Velasquez, Alvaro %A Jha, Sumit Kumar %X

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.

%B IEEE International Symposium on Circuits and Systems (ISCAS) %I IEEE %C Baltimore, MD %P 2643-2646 %G eng %0 Conference Paper %B IEEE International Conference on Nanotechnology (IEEE NANO) %D 2017 %T In-Memory Flow-Based Stochastic Computing on Memristor Crossbars using Bit-Vector Stochastic Streams %A Raj, Sunny %A Chakraborty, Dwaipayan %A Jha, Sumit Kumar %B IEEE International Conference on Nanotechnology (IEEE NANO) %I IEEE %C Pittsburgh, PA %P in press %G eng %0 Conference Paper %B IEEE International Symposium on Circuits and Systems (ISCAS). %D 2017 %T Design of Compact Memristive In-Memory Computing Systems using Model Counting %A Chakraborty, Dwaipayan %A Jha, Sumit Kumar %X

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.

%B IEEE International Symposium on Circuits and Systems (ISCAS). %I IEEE %C Baltimore, MD %P 2655-2658 %G eng %0 Conference Paper %B 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE) %D 2017 %T Automated synthesis of compact crossbars for sneak-path based in-memory computing %A Chakraborty, Dwaipayan %A Jha, Sumit Kumar %X

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.

%B 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE) %I IEEE %P 770–775 %G eng %0 Patent %D 2017 %T Stochastic computational model parameter synthesis system %A Jha, Sumit K %A Langmead, Christopher J %X

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.

%7 United States of America %I Google Patents %V US9558300 B2 %G eng %N U.S Patent and Trademark Office %& US %0 Conference Paper %B Circuits and Systems (ISCAS), 2016 IEEE International Symposium on %D 2016 %T Automated synthesis of stochastic computational elements using decision procedures %A Hassen, Amad Ul %A Chandrasekar, Brigadesh %A Jha, Sumit Kumar %B Circuits and Systems (ISCAS), 2016 IEEE International Symposium on %I IEEE %P 1678–1681 %G eng %0 Conference Paper %B Network Computing and Applications (NCA), 2016 IEEE 15th International Symposium on %D 2016 %T The cardinality-constrained paths problem: Multicast data routing in heterogeneous communication networks %A Velasquez, Alvaro %A Wojciechowski, Piotr %A Subramani, K %A Drager, Steven L %A Jha, Sumit Kumar %B Network Computing and Applications (NCA), 2016 IEEE 15th International Symposium on %I IEEE %P 126–130 %G eng %0 Patent %D 2016 %T Computation of boolean formulas using sneak paths in crossbar computing %A Jha, Sumit Kumar %A Rodriguez, Dilia E %A Van Nostrand, Joseph E %A Velasquez, Alvaro %7 United States of America %V 9319047 %G eng %N U.S Patent and Trademark Office %& US %0 Conference Paper %B Circuits and Systems (ISCAS), 2016 IEEE International Symposium on %D 2016 %T Flow-based computing on nanoscale crossbars: Design and implementation of full adders %A Alamgir, Zahiruddin %A Beckmann, Karsten %A Cady, Nathaniel %A Velasquez, Alvaro %A Jha, Sumit Kumar %B Circuits and Systems (ISCAS), 2016 IEEE International Symposium on %I IEEE %P 1870–1873 %G eng %0 Conference Paper %B Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016 %D 2016 %T Integrating symbolic and statistical methods for testing intelligent systems: Applications to machine learning and computer vision %A Ramanathan, Arvind %A Pullum, Laura L %A Hussain, Faraz %A Chakrabarty, Dwaipayan %A Jha, Sumit Kumar %B Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016 %I IEEE %P 786–791 %G eng %0 Conference Paper %B Circuits and Systems (ISCAS), 2016 IEEE International Symposium on %D 2016 %T Parallel boolean matrix multiplication in linear time using rectifying memristors %A Velasquez, Alvaro %A Jha, Sumit Kumar %B Circuits and Systems (ISCAS), 2016 IEEE International Symposium on %I IEEE %P 1874–1877 %G eng %0 Conference Paper %B Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings %D 2015 %T Distributed Markov Chains %A Ratul Saha %A Javier Esparza %A Jha, Sumit Kumar %A Madhavan Mukund %A P. S. Thiagarajan %B Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings %P 117–134 %G eng %U https://doi.org/10.1007/978-3-662-46081-8_7 %R 10.1007/978-3-662-46081-8_7 %0 Journal Article %J BMC bioinformatics %D 2015 %T Automated parameter estimation for biological models using Bayesian statistical model checking %A Hussain, Faraz %A Langmead, Christopher J %A Mi, Qi %A Dutta-Moscato, Joyeeta %A Vodovotz, Yoram %A Jha, Sumit K %X

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.

%B BMC bioinformatics %I BioMed Central %V 16 %P S8 %G eng %N 17 %0 Conference Paper %B Nanoscale Architectures (NANOARCH), 2015 IEEE/ACM International Symposium on %D 2015 %T Automated synthesis of crossbars for nanoscale computing using formal methods %A Velasquez, Alvaro %A Jha, Sumit Kumar %X

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.

%B Nanoscale Architectures (NANOARCH), 2015 IEEE/ACM International Symposium on %I IEEE %P 130–136 %G eng %0 Conference Paper %B Computer Design (ICCD), 2015 33rd IEEE International Conference on %D 2015 %T Fault-tolerant in-memory crossbar computing using quantified constraint solving %A Velasquez, Alvaro %A Jha, Sumit Kumar %X

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.

%B Computer Design (ICCD), 2015 33rd IEEE International Conference on %I IEEE %P 101–108 %G eng %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2015 IEEE 5th International Conference on %D 2015 %T SANJAY: Automatically synthesizing visualizations of flow cytometry data using decision procedures %A Hussain, Faraz %A Husein, Zubir %A Torosdagli, Neslisah %A Deo, Narsingh %A Pattanaik, Sumanta %A Chang, Chung-Che %A Jha, Sumit Kumar %B Computational Advances in Bio and Medical Sciences (ICCABS), 2015 IEEE 5th International Conference on %I IEEE %P 1–1 %G eng %0 Journal Article %J International Journal of Bioinformatics Research and Applications 2 %D 2014 %T Discovering rare behaviours in stochastic differential equations using decision procedures: applications to a minimal cell cycle model %A Ghosh, Arup Kumar %A Hussain, Faraz %A Jha, Susmit %A Langmead, Christopher J %A Jha, Sumit Kumar %B International Journal of Bioinformatics Research and Applications 2 %I Inderscience Publishers Ltd %V 10 %P 540–558 %G eng %N 4-5 %0 Conference Paper %B Procceedings of the 4th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar 2014) %D 2014 %T Early Adoption: High-Performance Computing for Big Data Introducing parallel programming and big data in the core algorithms curriculum %A Hussain, Faraz %A Deo, Narsingh %A Jha, Sumit K %B Procceedings of the 4th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar 2014) %G eng %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on %D 2014 %T EpiSpec: A formal specification language for parameterized agent-based models against epidemiological ground truth %A Hussain, Faraz %A Ramanathan, Arvind %A Pullum, Laura L %A Jha, Sumit K %B Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on %I IEEE %P 1–6 %G eng %0 Conference Paper %B Design & Test Symposium (IDT), 2014 9th International %D 2014 %T Parallel computing using memristive crossbar networks: Nullifying the processor-memory bottleneck %A Velasquez, Alvaro %A Jha, Sumit Kumar %X

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.

%B Design & Test Symposium (IDT), 2014 9th International %I IEEE %P 147–152 %G eng %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on %D 2014 %T Parameter discovery for stochastic computational models in systems biology using Bayesian model checking %A Hussain, Faraz %A Langmead, Christopher J %A Mi, Qi %A Dutta-Moscato, Joyeeta %A Vodovotz, Yoram %A Jha, Sumit K %B Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on %I IEEE %P 1–2 %G eng %0 Journal Article %J International Journal of Bioinformatics Research and Applications 2 %D 2014 %T Parameter discovery in stochastic biological models using simulated annealing and statistical model checking %A Hussain, Faraz %A Jha, Sumit K %A Jha, Susmit %A Langmead, Christopher J %B International Journal of Bioinformatics Research and Applications 2 %I Inderscience Publishers Ltd %V 10 %P 519–539 %G eng %N 4-5 %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on %D 2014 %T Putting humpty-dumpty together: Mining causal mechanistic biochemical models from big data %A Hussain, Faraz %A Velasquez, Alvaro %A Sassano, Emily %A Jha, Sumit Kumar %B Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on %I IEEE %P 1–6 %G eng %0 Journal Article %J J Inform Tech Softw Eng %D 2013 %T Big-Data-Driven Control Strategies for Complex Networks %A Deo, N %A Jha, SK %B J Inform Tech Softw Eng %V 3 %P e117 %G eng %0 Conference Paper %B Procceedings of the Third NSF/TCPP Workshop on Parallel and Distributed Computing Education, Boston, MA %D 2013 %T Introducing parallel programming across the undergraduate curriculum through an interdisciplinary course on computational modeling %A Deo, Narsingh %A Jha, SK %A Hussain, F %A Vasudevan, Mahadevan %B Procceedings of the Third NSF/TCPP Workshop on Parallel and Distributed Computing Education, Boston, MA %I Citeseer %G eng %0 Conference Paper %B Proceedings of the ACM Conference on Bioinformatics, Computational Biology and Biomedicine %D 2012 %T A computational metabolic model of the NG108-15 cell for high content drug screening with electrophysiological readout %A Kolli, Aditya Reddy %A Sommerhage, Frank %A Molnar, Peter %A Hood, Jonathan E %A Jenkins, Jerry J %A Hussain, Faraz %A Ghosh, Arup K %A Jha, Sumit Kumar %A Hickman, James J %B Proceedings of the ACM Conference on Bioinformatics, Computational Biology and Biomedicine %I ACM %P 530–532 %G eng %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on %D 2012 %T Decision procedure based discovery of rare behaviors in stochastic differential equation models of biological systems %A Ghosh, Arup K %A Hussain, Faraz %A Jha, Sumit K %A Langmead, Christopher J %A Jha, Susmit %B Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on %I IEEE %P 1–6 %G eng %0 Journal Article %J BMC bioinformatics %D 2012 %T Exploring behaviors of stochastic differential equation models of biological systems using change of measures %A Jha, Sumit Kumar %A Langmead, Christopher James %B BMC bioinformatics %I BioMed Central %V 13 %P S8 %G eng %N 5 %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on %D 2012 %T Parameter discovery for stochastic biological models against temporal behavioral specifications using an sprt based metric for simulated annealing %A Hussain, Faraz %A Dutta, Raj Gautam %A Jha, Sumit Kumar %A Langmead, Christopher James %A Jha, Susmit %B Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on %I IEEE %P 1–6 %G eng %0 Conference Paper %B BioMedical Computing (BioMedCom), 2012 ASE/IEEE International Conference on %D 2012 %T Quantifying uncertainty in epidemiological models %A Jha, Sumit K %A Ramanathan, Arvind %B BioMedical Computing (BioMedCom), 2012 ASE/IEEE International Conference on %I IEEE %P 80–85 %G eng %0 Journal Article %J International journal of bioinformatics research and applications %D 2012 %T Synthesis of insulin pump controllers from safety specifications using bayesian model validation %A Jha, Sumit Kumar %A Dutta, Raj Gautam %A Langmead, Christopher J %A Jha, Susmit %A Sassano, Emily %B International journal of bioinformatics research and applications %I Inderscience Publishers Ltd %V 8 %P 263–285 %G eng %N 3-4 %0 Conference Paper %B Proceedings of the NIST/NSF/USCAR Workshop on Developing Dependable and Secure Automotive Cyber-Physical Systems from Components %D 2011 %T Modeling and verifying intelligent automotive cyber-physical systems %A Jha, Sumit Kumar %A Sukthankar, Gita %B Proceedings of the NIST/NSF/USCAR Workshop on Developing Dependable and Secure Automotive Cyber-Physical Systems from Components %G eng %0 Journal Article %J Journal of critical care %D 2011 %T Parameter estimation and synthesis for systems biology: New algorithms for nonlinear and stochastic models %A Jha, Sumit %A Donze, Alexandre %A Khandpur, Rupinder %A Dutta-Moscato, Joyeeta %A Mi, Qi %A Vodovotz, Yoram %A Clermont, Gilles %A Langmead, Christopher %B Journal of critical care %I WB Saunders %V 26 %P e8 %G eng %N 2 %0 Conference Paper %B Computational Advances in Bio and Medical Sciences (ICCABS), 2011 IEEE 1st International Conference on %D 2011 %T Poster: Synthesis of biochemical models %A Jha, Sumit Kumar %A Langmead, Christopher James %B Computational Advances in Bio and Medical Sciences (ICCABS), 2011 IEEE 1st International Conference on %I IEEE %P 248–248 %G eng %0 Journal Article %J Theoretical Computer Science %D 2011 %T Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement %A Jha, Sumit Kumar %A Langmead, Christopher James %B Theoretical Computer Science %I Elsevier %V 412 %P 2162–2187 %G eng %N 21 %0 Conference Paper %B Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011 %D 2011 %T When to stop verification?: Statistical trade-off between expected loss and simulation cost %A Jha, Sumit Kumar %A Langmead, Christopher James %A Mohalik, Swarup %A Ramesh, Sethu %B Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011 %I IEEE %P 1–6 %G eng %0 Journal Article %D 2010 %T Model validation and discovery for complex stochastic systems %A Jha, Sumit Kumar %G eng %0 Patent %D 2010 %T Object relational map verification system %A Mehra, Krishna %A Rajamani, Sriram K %A Sistla, Aravinda P %A Jha, Sumit K %7 United States of America %I Google Patents %V US7702695 B2 %G eng %N U.S Patent and Trademark Office %& US %0 Conference Paper %B International Conference on Computational Methods in Systems Biology %D 2009 %T A bayesian approach to model checking biological systems %A Jha, Sumit K %A Clarke, Edmund M %A Langmead, Christopher J %A Legay, Axel %A Platzer, André %A Zuliani, Paolo %B International Conference on Computational Methods in Systems Biology %I Springer Berlin Heidelberg %P 218–234 %G eng %0 Journal Article %D 2009 %T Statistical model checking for complex stochastic models in systems biology %A Jha, Sumit Kumar %A Clarke, Edmund M %A Langmead, Christopher J %A Legay, Axel %A Platzer, Andre %A Zuliani, Paolo %G eng %0 Journal Article %J Journal of Bioinformatics and Computational Biology %D 2009 %T Symbolic approaches for finding control strategies in Boolean networks %A Langmead, Christopher James %A Jha, Sumit Kumar %X

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.

%B Journal of Bioinformatics and Computational Biology %I Imperial College Press %V 7 %P 323–338 %G eng %N 02 %0 Conference Paper %B International Workshop on Hybrid Systems: Computation and Control %D 2008 %T A counterexample-guided approach to parameter synthesis for linear hybrid automata %A Frehse, Goran %A Jha, Sumit Kumar %A Krogh, Bruce H %X

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.

%B International Workshop on Hybrid Systems: Computation and Control %I Springer Berlin Heidelberg %P 187–200 %G eng %0 Conference Paper %B International Workshop on Hybrid Systems: Computation and Control %D 2008 %T d-ira: A distributed reachability algorithm for analysis of linear hybrid automata %A Jha, Sumit Kumar %X

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.

%B International Workshop on Hybrid Systems: Computation and Control %I Springer Berlin Heidelberg %P 618–621 %G eng %0 Conference Paper %B High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE %D 2008 %T Random relaxation abstractions for bounded reachability analysis of linear hybrid automata: Distributed randomized abstractions in model checking %A Jha, Sumit Kumar %A Jha, Susmit %B High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE %I IEEE %P 147–153 %G eng %0 Conference Paper %B High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE %D 2008 %T Randomization based probabilistic approach to detect trojan circuits %A Jha, Susmit %A Jha, Sumit Kumar %B High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE %I IEEE %P 117–124 %G eng %0 Conference Paper %B International Conference on Computational Methods in Systems Biology %D 2008 %T Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway %A Clarke, Edmund M %A Faeder, James R %A Langmead, Christopher J %A Harris, Leonard A %A Jha, Sumit Kumar %A Legay, Axel %X

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.

%B International Conference on Computational Methods in Systems Biology %I Springer Berlin Heidelberg %P 231–250 %G eng %0 Conference Paper %B Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, %D 2007 %T Verification of Object Relational Maps %X

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.

%B Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, %I IEEE Computer Society %C London, England, UK %@ 978-0-7695-2884-7 %G eng %U http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4343908 %0 Conference Paper %B Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, London, England, UK %D 2007 %T Verification of Object Relational Maps %A Krishna K. Mehra %A Sriram K. Rajamani %A A. Prasad Sistla %A Jha, Sumit Kumar %B Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, London, England, UK %P 283–292 %G eng %U https://doi.org/10.1109/SEFM.2007.45 %R 10.1109/SEFM.2007.45 %0 Conference Paper %B International Workshop on Algorithms in Bioinformatics %D 2007 %T Predicting protein folding kinetics via temporal logic model checking %A Langmead, Christopher James %A Jha, Sumit Kumar %X

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.

%B International Workshop on Algorithms in Bioinformatics %I Springer Berlin Heidelberg %P 252–264 %G eng %0 Conference Paper %B International Workshop on Hybrid Systems: Computation and Control %D 2007 %T Reachability for linear hybrid automata using iterative relaxation abstraction %A Jha, Sumit K %A Krogh, Bruce H %A Weimer, James E %A Clarke, Edmund M %X

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.

%B International Workshop on Hybrid Systems: Computation and Control %I Springer Berlin Heidelberg %P 287–300 %G eng %0 Conference Paper %B Decision and Control, 2006 45th IEEE Conference on %D 2006 %T Model checking for fault explanation %A Jiang, Shengbing %A Fuhrman, Thomas E %A Jha, Sumit K %X

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.

%B Decision and Control, 2006 45th IEEE Conference on %I IEEE %P 404–409 %G eng %0 Journal Article %D 2006 %T Temporal-logics as query languages for dynamic Bayesian networks: application to D. melanogaster embryo development %A Langmead, Christopher J %A Jha, Sumit Kumar %A Clarke, Edmund M %X

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.

%G eng %0 Conference Paper %B International Workshop on Hybrid Systems: Computation and Control %D 2005 %T Refining abstractions of hybrid systems using counterexample fragments %A Fehnker, Ansgar %A Clarke, Edmund %A Jha, Sumit Kumar %A Krogh, Bruce %X

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.

%B International Workshop on Hybrid Systems: Computation and Control %I Springer Berlin Heidelberg %P 242–257 %G eng %0 Book Section %B Handbook of Networked and Embedded Control Systems %D 2005 %T Temporal logic model checking %A Clarke, Edmund %A Fehnker, Ansgar %A Jha, Sumit Kumar %A Veith, Helmut %X

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.

%B Handbook of Networked and Embedded Control Systems %I Springer %P 539–558 %G eng