# Publications

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.

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

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

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

, “
A Compact 8-bit Adder Design using In-Memory Memristive Computing: Towards Solving the Feynman Grand Prize Challenge
,” in 13th ACM/IEEE International Symposium on Nanoscale Architectures, Newport, USA, 2017, pp. in press.Abstract feynmangrandprize_nanoarch2017.pdf

, “
Computation of Boolean Matrix Chain Products in 3D ReRAM
,” in IEEE International Symposium on Circuits and Systems (ISCAS), Baltimore, MD, 2017, pp. 2643-2646.Abstract 3d_reram_iscas_2017.pdf

, “
In-Memory Flow-Based Stochastic Computing on Memristor Crossbars using Bit-Vector Stochastic Streams
,” in IEEE International Conference on Nanotechnology (IEEE NANO), Pittsburgh, PA, 2017, pp. in press. ieeenano2017_JHA.pdf

, “
Design of Compact Memristive In-Memory Computing Systems using Model Counting
,” in IEEE International Symposium on Circuits and Systems (ISCAS)., Baltimore, MD, 2017, pp. 2655-2658.Abstract MLnFM_iscas2017.pdf

, “
Automated synthesis of compact crossbars for sneak-path based in-memory computing
,” in 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pp. 770–775.Abstract crossbarsusingformalmethods.pdf

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

, “US Patent App. 13/673,575

Automated synthesis of stochastic computational elements using decision procedures
,” in Circuits and Systems (ISCAS), 2016 IEEE International Symposium on, 2016, pp. 1678–1681.

, “
The cardinality-constrained paths problem: Multicast data routing in heterogeneous communication networks
,” in Network Computing and Applications (NCA), 2016 IEEE 15th International Symposium on, 2016, pp. 126–130. nca2016_jha.pdf

, “
Computation of boolean formulas using sneak paths in crossbar computing
”, US Patent: 9319047, 2016. patent2016_memristorcomputing_jha.pdf

, “US Patent 9,319,047

Flow-based computing on nanoscale crossbars: Design and implementation of full adders
,” in Circuits and Systems (ISCAS), 2016 IEEE International Symposium on, 2016, pp. 1870–1873. iscas2016_flowmemristor_jha_01.pdf

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

, “
Parallel boolean matrix multiplication in linear time using rectifying memristors
,” in Circuits and Systems (ISCAS), 2016 IEEE International Symposium on, 2016, pp. 1874–1877. iscas2016_parallel_memristor_jha.pdf

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

, “
SANJAY: Automatically synthesizing visualizations of flow cytometry data using decision procedures
,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2015 IEEE 5th International Conference on, 2015, pp. 1–1.

, “ Discovering rare behaviours in stochastic differential equations using decision procedures: applications to a minimal cell cycle model,” International Journal of Bioinformatics Research and Applications 2, vol. 10, no. 4-5, pp. 540–558, 2014.

, “ Early Adoption: High-Performance Computing for Big Data Introducing parallel programming and big data in the core algorithms curriculum,” in Procceedings of the 4th NSF/TCPP Workshop on Parallel and Distributed Computing Education (EduPar 2014), 2014.

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

, “ Big-Data-Driven Control Strategies for Complex Networks,” J Inform Tech Softw Eng, vol. 3, pp. e117, 2013.

, “ Introducing parallel programming across the undergraduate curriculum through an interdisciplinary course on computational modeling,” in Procceedings of the Third NSF/TCPP Workshop on Parallel and Distributed Computing Education, Boston, MA, 2013.

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

, “ Decision procedure based discovery of rare behaviors in stochastic differential equation models of biological systems,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on, 2012, pp. 1–6.

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

Parameter discovery for stochastic biological models against temporal behavioral specifications using an sprt based metric for simulated annealing,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2012 IEEE 2nd International Conference on, 2012, pp. 1–6.

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

, “ Synthesis of insulin pump controllers from safety specifications using bayesian model validation,” International journal of bioinformatics research and applications, vol. 8, no. 3-4, pp. 263–285, 2012.

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

, “ Poster: Synthesis of biochemical models,” in Computational Advances in Bio and Medical Sciences (ICCABS), 2011 IEEE 1st International Conference on, 2011, pp. 248–248.

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

, “ Random relaxation abstractions for bounded reachability analysis of linear hybrid automata: Distributed randomized abstractions in model checking,” in High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE, 2008, pp. 147–153.

, “ Randomization based probabilistic approach to detect trojan circuits,” in High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE, 2008, pp. 117–124.

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

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

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

, “