Formal Methods

S. Fernandes, S. Raj, E. Ortiz, I. Vintila, and S. K. Jha, “ Directed Adversarial Attacks on Fingerprints using Attributions ,” in International Conference on Biometrics, 2019.Abstract


Fingerprint recognition systems verify the identity of individuals and provide access to secure information in various commercial applications. However, with advancements in artificial intelligence, fingerprint-based security methods are vulnerable to attack. Such a breach has the potential to compromise confidential, private and valuable information. In this paper, we attack a state-of- the-art fingerprint recognition system based on transfer learning. Our approach uses attribution analysis to identify the fingerprint region crucial to correct classification, and then perturbs the fingerprint using error masks derived from a neural network to generate an adversarial fingerprint.

Image quality assessment metrics applied to calculate the difference between the original and perturbed fingerprints include average difference, maximum difference, normalized absolute error, and peak signal to noise ratio. On the ATVS fingerprint dataset, the differences between these values in the original and corresponding perturbed fingerprint images are negligible. Further, the VeriFinger SDK is used to detect the minutiae and perform matching between the original and perturbed fingerprints. The matching score is above 250, which reinforces the fact that there is virtually no loss between the original and perturbed fingerprints.


B. Shaia, A. Velasquez, and S. K. Jha, “ Spatially Efficient in-Memory Addition Through Destructive and Non-Destructive Operations ,” in IEEE International Symposium on Circuits and Systems, Sapporo, Japan, 2019.
S. Jha, S. Raj, S. K. Jha, and N. Shankar, “ Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems ,” in 16th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), Beijing, China, 2018.Abstract


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


A. U. Hassen, D. Chakraborty, and S. K. Jha, “ Free Binary Decision Diagram Based Synthesis of Compact Crossbars for in-Memory Computing of Boolean Functions ,” Transactions on Circuits and Systems (TCAS) II, 2018. TCAS_FlowBasedComputing.pdf
A. Khalid and S. K. Jha, “ Calibration of Rule-Based Stochastic Biochemical Models using Statistical Model Checking ,” IEEE International Conference on Bioinformatics and Biomedicine. 2018.Abstract

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.

A. Khalid and S. K. Jha, “ Calibration of Rule-Based Stochastic Biochemical Models using Statistical Model Checking ,” International Conference on Bioinformatics and Biomedicine (BIBM). 2018.
A. Khalid and S. K. Jha, “ Parameter Estimation of Stochastic Biochemical Models using Multiple Hypothesis Testing ,” in 8th IEEE International Conference on Computational Advances in Bio and medical Sciences (ICCABS), 2018.
S. Raj and S. K. Jha, “ Predicting Success in Undergraduate Parallel Programming via Probabilistic Causality Analysis ,” in 8th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar-18) co-located with the 32nd IEEE International Parallel & Distributed Processing Symposium, Vancouver, Canada, 2018.Abstract


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


L. L. Pullum, C. Steed, A. Ramanathan, and S. K. Jha, “ Mathematically Rigorous Verification and Validation of Scientific Machine Learning ,” in DOE ASCR Workshop on Scientific Machine Learning, 2018.
A. U. Hassen and S. K. Jha, “ Free Binary Decision Diagram Based Synthesis of Compact Crossbars for in-Memory Computing of Boolean Functions ,” in International Symposium on Circuits and Systems (ISCAS), Florence, Italy, 2018.Abstract

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

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


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


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

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



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


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


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


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


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


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


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


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


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

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

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

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




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


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


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


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


F. Hussain, A. Ramanathan, L. L. Pullum, and S. K. Jha, “ EpiSpec: A formal specification language for parameterized agent-based models against epidemiological ground truth ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on, 2014, pp. 1–6.
A. Velasquez and S. K. Jha, “ Parallel computing using memristive crossbar networks: Nullifying the processor-memory bottleneck ,” in Design & Test Symposium (IDT), 2014 9th International, 2014, pp. 147–152.Abstract


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


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


F. Hussain, C. J. Langmead, Q. Mi, J. Dutta-Moscato, Y. Vodovotz, and S. K. Jha, “ Parameter discovery for stochastic computational models in systems biology using Bayesian model checking ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on, 2014, pp. 1–2.
F. Hussain, S. K. Jha, S. Jha, and C. J. Langmead, “ Parameter discovery in stochastic biological models using simulated annealing and statistical model checking ,” International Journal of Bioinformatics Research and Applications 2, vol. 10, no. 4-5, pp. 519–539, 2014.
F. Hussain, A. Velasquez, E. Sassano, and S. K. Jha, “ Putting humpty-dumpty together: Mining causal mechanistic biochemical models from big data ,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2014 IEEE 4th International Conference on, 2014, pp. 1–6.
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.
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.


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. quantifyinguncertainty.pdf
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, “ 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.
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

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


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


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


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


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


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. 


Verification of Object Relational Maps ,” in Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, , London, England, UK, 2007. Publisher's VersionAbstract


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


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


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


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


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


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. 


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


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


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


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