# Formal Methods

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

, “
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

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

, “
Mathematically Rigorous Verification and Validation of Scientific Machine Learning
,” in DOE ASCR Workshop on Scientific Machine Learning, 2018.

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

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

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

, “
**BEST PAPER AWARD**

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

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

, “
Adversarial attacks on computer vision algorithms using natural perturbations
,” in Tenth International Conference on Contemporary Computing, New Delhi, India, 2017, pp. in press.Abstract adversarialattacksnatural.pdf

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

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

, “
Stochastic computational model parameter synthesis system
”, US Patent: US9558300 B2, 2017.Abstract

, “US Patent App. 13/673,575

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

, “
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

, “
Automated parameter estimation for biological models using Bayesian statistical model checking
,” BMC bioinformatics, vol. 16, no. 17, pp. S8, 2015.Abstract bmcbioinformatics_discovery.pdf

, “
**BEST PAPER AWARD at IEEE ICCABS 2014**

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

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

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

, “
Parallel computing using memristive crossbar networks: Nullifying the processor-memory bottleneck
,” in Design & Test Symposium (IDT), 2014 9th International, 2014, pp. 147–152.Abstract idt2014.pdf

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

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

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

, “
Exploring behaviors of stochastic differential equation models of biological systems using change of measures
,” BMC bioinformatics, vol. 13, no. 5, pp. S8, 2012.

, “
**BEST PAPER AWARD**

Quantifying uncertainty in epidemiological models
,” in BioMedical Computing (BioMedCom), 2012 ASE/IEEE International Conference on, 2012, pp. 80–85. quantifyinguncertainty.pdf

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

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

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

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

, “
Object relational map verification system
”, US Patent: US7702695 B2, 2010.

, “US Patent 7,702,695

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

, “
Symbolic approaches for finding control strategies in Boolean networks
,” Journal of Bioinformatics and Computational Biology, vol. 7, no. 02, pp. 323–338, 2009.Abstract 2009_jbcb_and_apbc_paper_underlined.pdf

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

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

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

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

Predicting protein folding kinetics via temporal logic model checking
,” in International Workshop on Algorithms in Bioinformatics, 2007, pp. 252–264.Abstract 2007_wabi_underlined.pdf

, “
Reachability for linear hybrid automata using iterative relaxation abstraction
,” in International Workshop on Hybrid Systems: Computation and Control, 2007, pp. 287–300.Abstract 2007_hscc_underlined.pdf

, “
Model checking for fault explanation
,” in Decision and Control, 2006 45th IEEE Conference on, 2006, pp. 404–409.Abstract 2006_cdc_paper_and_acceptance_underlined.pdf

, “
Refining abstractions of hybrid systems using counterexample fragments
,” in International Workshop on Hybrid Systems: Computation and Control, 2005, pp. 242–257.Abstract 2006_hscc_underlined.pdf

, “
Temporal logic model checking
,” in Handbook of Networked and Embedded Control Systems, Springer, 2005, pp. 539–558.Abstract book2005_underlined.pdf

, “