College of Sciences

Permanent URI for this communityhttps://hdl.handle.net/20.500.12588/256

Browse

Now showing 1 - 20 of 432

A Computational Approach to Explore the Interaction of Semisynthetic Nitrogenous Heterocyclic Compounds with the SARS-CoV-2 Main Protease
(2020-12-27) Llanes, Alejandro; Cruz, Héctor; Nguyen, Viet D.; Larionov, Oleg V.; Fernández, Patricia L.
In the context of the ongoing coronavirus disease 2019 (COVID-19) pandemic, numerous attempts have been made to discover new potential antiviral molecules against its causative agent, SARS-CoV-2, many of which focus on its main protease (Mpro). We hereby used two approaches based on molecular docking simulation to explore the interaction of four libraries of semisynthetic nitrogenous heterocyclic compounds with Mpro. Libraries L1 and L2 contain 52 synthetic derivatives of the natural compound 2-propylquinoline, whereas libraries L3 and L4 contain 65 compounds synthesized using the natural compound physostigmine as a precursor. Validation through redocking suggested that the rigid receptor and flexible receptor approaches used for docking were suitable to model the interaction of this type of compounds with the target protein, although the flexible approach seemed to provide a more realistic representation of interactions within the active site. Using empirical energy score thresholds, we selected 58 compounds from the four libraries with the most favorable energy estimates. Globally, favorable estimates were obtained for molecules with two or more substituents, putatively accommodating in three or more subsites within the Mpro active site. Our results pave the way for further experimental evaluation of the selected compounds as potential antiviral agents against SARS-CoV-2.
A Customized Human Mitochondrial DNA Database (hMITO DB v1.0) for Rapid Sequence Analysis, Haplotyping and Geo-Mapping
(2023-08-31) Shen-Gunther, Jane; Gunther, Rutger S.; Cai, Hong; Wang, Yufeng
The field of mitochondrial genomics has advanced rapidly and has revolutionized disciplines such as molecular anthropology, population genetics, and medical genetics/oncogenetics. However, mtDNA next-generation sequencing (NGS) analysis for matrilineal haplotyping and phylogeographic inference remains hindered by the lack of a consolidated mitogenome database and an efficient bioinformatics pipeline. To address this, we developed a customized human mitogenome database (hMITO DB) embedded in a CLC Genomics workflow for read mapping, variant analysis, haplotyping, and geo-mapping. The database was constructed from 4286 mitogenomes. The macro-haplogroup (A to Z) distribution and representative phylogenetic tree were found to be consistent with published literature. The hMITO DB automated workflow was tested using mtDNA-NGS sequences derived from Pap smears and cervical cancer cell lines. The auto-generated read mapping, variants track, and table of haplotypes and geo-origins were completed in 15 min for 47 samples. The mtDNA workflow proved to be a rapid, efficient, and accurate means of sequence analysis for translational mitogenomics.
A Customized Monkeypox Virus Genomic Database (MPXV DB v1.0) for Rapid Sequence Analysis and Phylogenomic Discoveries in CLC Microbial Genomics
(2022-12-22) Shen-Gunther, Jane; Cai, Hong; Wang, Yufeng
Monkeypox has been a neglected, zoonotic tropical disease for over 50 years. Since the 2022 global outbreak, hundreds of human clinical samples have been subjected to next-generation sequencing (NGS) worldwide with raw data deposited in public repositories. However, sequence analysis for in-depth investigation of viral evolution remains hindered by the lack of a curated, whole genome Monkeypox virus (MPXV) database (DB) and efficient bioinformatics pipelines. To address this, we developed a customized MPXV DB for integration with "ready-to-use" workflows in the CLC Microbial Genomics Module for whole genomic and metagenomic analysis. After database construction (218 MPXV genomes), whole genome alignment, pairwise comparison, and evolutionary analysis of all genomes were analyzed to autogenerate tabular outputs and visual displays (collective runtime: 16 min). The clinical utility of the MPXV DB was demonstrated by using a Chimpanzee fecal, hybrid-capture NGS dataset (publicly available) for metagenomic, phylogenomic, and viral/host integration analysis. The clinically relevant MPXV DB embedded in CLC workflows proved to be a rapid method of sequence analysis useful for phylogenomic exploration and a wide range of applications in translational science.
A De Novo Sequence Variant in Barrier-to-Autointegration Factor Is Associated with Dominant Motor Neuronopathy
(2023-03-09) Marcelot, Agathe; Rodriguez-Tirado, Felipe; Cuniasse, Philippe; Joiner, Mei-ling; Miron, Simona; Soshnev, Alexey A.; Fang, Mimi; Pufall, Miles A.; Mathews, Katherine D.; Moore, Steven A.; Zinn-Justin, Sophie; Geyer, Pamela K.
Barrier-to-autointegration factor (BAF) is an essential component of the nuclear lamina. Encoded by BANF1, this DNA binding protein contributes to the regulation of gene expression, cell cycle progression, and nuclear integrity. A rare recessive BAF variant, Ala12Thr, causes the premature aging syndrome, Néstor–Guillermo progeria syndrome (NGPS). Here, we report the first dominant pathogenic BAF variant, Gly16Arg, identified in a patient presenting with progressive neuromuscular weakness. Although disease variants carry nearby amino acid substitutions, cellular and biochemical properties are distinct. In contrast to NGPS, Gly16Arg patient fibroblasts show modest changes in nuclear lamina structure and increases in repressive marks associated with heterochromatin. Structural studies reveal that the Gly16Arg substitution introduces a salt bridge between BAF monomers, reducing the conformation ensemble available to BAF. We show that this structural change increases the double-stranded DNA binding affinity of BAF Gly16Arg. Together, our findings suggest that BAF Gly16Arg has an increased chromatin occupancy that leads to epigenetic changes and impacts nuclear functions. These observations provide a new example of how a missense mutation can change a protein conformational equilibrium to cause a dominant disease and extend our understanding of mechanisms by which BAF function impacts human health.
A Federated Model for Scheduling in Wide-Area Systems
(UTSA Department of Computer Science, 1996-02-06) Weissman, Jon B.; Grimshaw, Andrew S.
In this paper a model for scheduling in wide-area systems is described. The model is federated and utilizes a collection of local site schedulers that control the use of their resources. The wide-area scheduler consults the local site schedulers to obtain candidate machine schedules. A set of issues and challenges inherent to wide-area scheduling are also described and the proposed model is shown to address many of these problems. A distributed algorithm for wide-area scheduling is presented and relies upon information made available about the resource needs of user jobs. The wide-area scheduler will be implemented in Legion, a wide-area computing system developed at the University of Virginia.
A Framework for Composing Noninterferent Languages
(UTSA Department of Computer Science, 2013-09) Gampe, Andreas; von Ronne, Jeffery
Software is frequently implemented using multiple specialized languages for different tasks. Security type systems, one technique to secure software, have previously only been studied for programs written entirely in a single language. We present a framework that facilitates reasoning over composite languages. In it, guarantees of sufficiently related component languages can be lifted to the composed language. This can significantly lower the burden necessary to certify that such composite programs are safe. Our simple but powerful approach relies, at its core, on computability and security-level separability. Besides non-interference, we also show how the framework can accommodate notions of declassification. To demonstrate the applicability of this framework, we show that a standard secure while language from the literature satisfies all necessary requirements of a composition host, and sketch how to securely embed an expressive fragment of SQL.
A Genetic Algorithm Using Triplet Nucleotide Encoding and DNA Reproduction Operations for Unconstrained Optimization Problems
(2017-06-30) Zang, Wenke; Zhang, Weining; Zhang, Wenqian; Liu, Xiyu
As one of the evolutionary heuristics methods, genetic algorithms (GAs) have shown a promising ability to solve complex optimization problems. However, existing GAs still have difficulties in finding the global optimum and avoiding premature convergence. To further improve the search efficiency and convergence rate of evolution algorithms, inspired by the mechanism of biological DNA genetic information and evolution, we present a new genetic algorithm, called GA-TNE+DRO, which uses a novel triplet nucleotide coding scheme to encode potential solutions and a set of new genetic operators to search for globally optimal solutions. The coding scheme represents potential solutions as a sequence of triplet nucleotides and the DNA reproduction operations mimic the DNA reproduction process more vividly than existing DNA-GAs. We compared our algorithm with several existing GA and DNA-based GA algorithms using a benchmark of eight unconstrained optimization functions. Our experimental results show that the proposed algorithm can converge to solutions much closer to the global optimal solutions in a much lower number of iterations than the existing algorithms. A complexity analysis also shows that our algorithm is computationally more efficient than the existing algorithms.
A Kernel-Based Intuitionistic Fuzzy C-Means Clustering Using a DNA Genetic Algorithm for Magnetic Resonance Image Segmentation
(2017-10-27) Zang, Wenke; Zhang, Weining; Zhang, Wenqian; Liu, Xiyu
MRI segmentation is critically important for clinical study and diagnosis. Existing methods based on soft clustering have several drawbacks, including low accuracy in the presence of image noise and artifacts, and high computational cost. In this paper, we introduce a new formulation of the MRI segmentation problem as a kernel-based intuitionistic fuzzy C-means (KIFCM) clustering problem and propose a new DNA-based genetic algorithm to obtain the optimal KIFCM clustering. While this algorithm searches the solution space for the optimal model parameters, it also obtains the optimal clustering, therefore the optimal MRI segmentation. We perform empirical study by comparing our method with six state-of-the-art soft clustering methods using a set of UCI (University of California, Irvine) datasets and a set of synthetic and clinic MRI datasets. The preliminary results show that our method outperforms other methods in both the clustering metrics and the computational efficiency.
A Logical Framework for Sequence Diagram with Combined Fragments
(UTSA Department of Computer Science, 2011-11) Shen, Hui; Robinson, Mark; Niu, Jianwei
Graphical representations of scenarios, such as UML Sequence Diagrams and Message Sequence Charts, serve as a well-accepted means for modeling the interactions among software systems and their environment through the exchange of messages. The Combined Fragments of UML Sequence Diagram permit various types of control flow among messages (e.g., interleaving and branching) to express an aggregation of multiple traces encompassing complex and concurrent behaviors. However, Combined Fragments increase the difficulty of Sequence Diagram comprehension and analysis. This paper introduces an approach to formalizing the semantics of Sequence Diagrams with Combined Fragments in terms of Linear Temporal Logic (LTL) templates. In all the templates, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the semantics of basic Sequence Diagram, all the Combined Fragments, and nested Combined Fragments. Moreover, the formalization enables us to leverage the analytical powers of automated decision procedures for LTL formulas to determine if a collection of Sequence Diagrams is consistent, safe, and deadlock-free.
A Low Cost, Edge Computing, All-Sky Imager for Cloud Tracking and Intra-Hour Irradiance Forecasting
(2017-03-23) Richardson, Walter; Krishnaswami, Hariharan; Vega, Rolando; Cervantes, Michael
With increasing use of photovoltaic (PV) power generation by utilities and their residential customers, the need for accurate intra-hour and day-ahead solar irradiance forecasting has become critical. This paper details the development of a low cost all-sky imaging system and an intra-hour cloud motion prediction methodology that produces minutes-ahead irradiance forecasts. The SkyImager is designed around a Raspberry Pi single board computer (SBC) with a fully programmable, high resolution Pi Camera, housed in a durable all-weather enclosure. Our software is written in Python 2.7 and utilizes the open source computer vision package OpenCV. The SkyImager can be configured for different operational environments and network designs, from a standalone edge computing model to a fully integrated node in a distributed, cloud-computing based micro-grid. Preliminary results are presented using the imager on site at the National Renewable Energy Laboratory (NREL) in Golden, CO, USA during the fall of 2015 under a variety of cloud conditions.
A Multimodal Appraisal of Zaha Hadid's Glasgow Riverside Museum—Criticism, Performance Evaluation, and Habitability
(2023-01-09) Salama, Ashraf M.; Salingaros, Nikos A.; MacLean, Laura
High-profile projects promoted by governments, local municipalities, and the media do not always meet program requirements or user expectations. The Riverside Museum in Glasgow by Zaha Hadid Architects, which has generated significant discussion in the media, is used to test this claim. A multimodal inquiry adopts three factors: criticism, performance evaluation, and habitability. Results from this method are then correlated with visual attention scans using software from 3M Corporation to map unconscious user engagement. A wide spectrum of tools is employed, including a walking tour assessment procedure, contemplation of selected settings, navigational mapping, and assessing user emotional experiences. Key aspects of the design and spatial qualities of this museum are compared with an analysis of critical writings on how the project was portrayed in the media. Further, we examine socio-spatial practices, selected behavioral phenomena, and the emotional experiences that ensue from users' interaction with the building and its immediate context. The findings suggest design shortcomings and, more worrisome, that spatial qualities relevant to users' experiences do not seem to have been met. In going beyond the usual method of analysis, we apply new techniques of eye-tracking simulations, which verify results obtained by more traditional means. An in-depth analysis suggests the need for better compatibility between the imagined design ideas and the actual spatial environments in use.
A Network-Based Approach for Improving Annotation of Transcription Factor Functions and Binding Sites in Arabidopsis thaliana
(2023-01-21) Najnin, Tanzira; Saimon, Sakhawat Hossain; Sunter, Garry; Ruan, Jianhua
Transcription factors are an integral component of the cellular machinery responsible for regulating many biological processes, and they recognize distinct DNA sequence patterns as well as internal/external signals to mediate target gene expression. The functional roles of an individual transcription factor can be traced back to the functions of its target genes. While such functional associations can be inferred through the use of binding evidence from high-throughput sequencing technologies available today, including chromatin immunoprecipitation sequencing, such experiments can be resource-consuming. On the other hand, exploratory analysis driven by computational techniques can alleviate this burden by narrowing the search scope, but the results are often deemed low-quality or non-specific by biologists. In this paper, we introduce a data-driven, statistics-based strategy to predict novel functional associations for transcription factors in the model plant Arabidopsis thaliana. To achieve this, we leverage one of the largest available gene expression compendia to build a genome-wide transcriptional regulatory network and infer regulatory relationships among transcription factors and their targets. We then use this network to build a pool of likely downstream targets for each transcription factor and query each target pool for functionally enriched gene ontology terms. The results exhibited sufficient statistical significance to annotate most of the transcription factors in Arabidopsis with highly specific biological processes. We also perform DNA binding motif discovery for transcription factors based on their target pool. We show that the predicted functions and motifs strongly agree with curated databases constructed from experimental evidence. In addition, statistical analysis of the network revealed interesting patterns and connections between network topology and system-level transcriptional regulation properties. We believe that the methods demonstrated in this work can be extended to other species to improve the annotation of transcription factors and understand transcriptional regulation on a system level.
A New Digital Lake Bathymetry Model Using the Step-Wise Water Recession Method to Generate 3D Lake Bathymetric Maps Based on DEMs
(2019-05-31) Zhu, Siyu; Liu, Baojian; Wan, Wei; Xie, Hongjie; Fang, Yu; Chen, Xi; Li, Huan; Fang, Weizhen; Zhang, Guoqing; Tao, Mingwei; Hong, Yang
The availability of lake bathymetry maps is imperative for estimating lake water volumes and their variability, which is a sensitive indicator of climate. It is difficult, if not impossible, to obtain bathymetric measurements from all of the thousands of lakes across the globe due to costly labor and/or harsh topographic regions. In this study, we develop a new digital lake bathymetry model (DLBM) using the step-wise water recession method (WRM) to generate 3-dimensional lake bathymetric maps based on the digital elevation model (DEM) alone, with two assumptions: (1) typically, the lake's bathymetry is formed and shaped by geological processes similar to those that shaped the surrounding landmasses, and (2) the agent rate of water (the thickness of the sedimentary deposit proportional to the lake water depth) is uniform. Lake Ontario and Lake Namco are used as examples to demonstrate the development, calibration, and refinement of the model. Compared to some other methods, the estimated 3D bathymetric maps using the proposed DLBM could overcome the discontinuity problem to adopt the complex topography of lake boundaries. This study provides a mathematically robust yet cost-effective approach for estimating lake volumes and their changes in regions lacking field measurements of bathymetry, for example, the remote Tibetan Plateau, which contains thousands of lakes.
A random walk based approach for improving protein-protein interaction network and protein complex prediction
(UTSA Department of Computer Science, 2011-12) Lei, Chengwei; Ruan, Jianhua
Motivation: Recent advances in high-throughput technology have dramatically increased the availability of protein-protein interaction (PPI) data and stimulated the development of many methods for predicting protein complexes, which are important in understanding the functional organization of PPI networks. However, automated protein complex prediction from PPI data alone is significantly hindered by the high level of noise, sparseness, and highly skewed degree distribution of PPI networks. Here we present a novel network topology-based algorithm to remove spurious interactions and recover missing ones by computational predictions, and to increase the accuracy of protein complex prediction by reducing the impact of hub nodes. The key idea of our algorithm is that two proteins sharing some high-order topological similarities, which are measured by a novel random walk-based procedure, are likely interacting with each other and may belong to the same protein complex. Results: Applying our algorithm to a yeast PPI network, we found that the interactions in the reconstructed network have higher biological relevance than in the original network, assessed by multiple types of information, including gene ontology, gene expression, essentiality, conservation between species, and known protein complexes. Comparison with existing methods shows that the network reconstructed by our method has the highest quality. Using two independent graph clustering algorithms, we found that the reconstructed network has resulted in significantly improved prediction accuracy of protein complexes. Furthermore, our method is applicable to PPI networks obtained with different experimental systems such as affinity purification, Y2H, and PCA, and evidence shows that the predicted edges are likely bona fide physical interactions.
A randomized steiner tree approach for biomarker discovery and classification of breast cancer metastasis
(UTSA Department of Computer Science, 2011-12) Jahid, Md. Jamiul; Ruan, Jianhua
Motivation: DNA microarray has become an important tool to help identify biomarker genes for improving the prognosis of metastatic breast cancer - a leading cause of cancer-related deaths in women worldwide. Recently, pathway-level relationships between genes have been increasingly used to build more robust classification models which also can provide useful biological insights. Due to the unavailability of complete pathways, protein-protein interaction (PPI) network is becoming more popular to researcher and opens a way to investigate the developmental process of breast cancer. Here, a network-based method is proposed to combine microarray gene expression profiles and PPI network for biomarker discovery for breast cancer metastasis. The key idea is to identify a small number of genes to connect differentially expressed genes into a single component in a PPI network; these intermediate genes contain important information about the pathways involved in metastasis and have a high probability of being biomarkers. Results: We applied this approach on three breast cancer microarray datasets, and identified significant numbers of well-known biomarker genes for breast cancer metastasis. Those selected genes are enriched with biological processes and pathways related to carcinogenic process, and, importantly, have higher stability across different datasets than in previous studies. Furthermore, those genes significantly increased cross-data classification accuracy in breast cancer metastasis. The randomized Steiner tree based approach described here is a new way to discover biomarker genes for breast cancer, and improves the prediction accuracy of metastasis. The analysis is limited here only to breast cancer, but can be easily applied to other diseases.
A Review on Applications of Remote Sensing and Geographic Information Systems (GIS) in Water Resources and Flood Risk Management
(2018-05-07) Wang, Xianwei; Xie, Hongjie
Water is one of the most critical natural resources that maintain the ecosystem and support people's daily life. Pressures on water resources and disaster management are rising primarily due to the unequal spatial and temporal distribution of water resources and pollution, and also partially due to our poor knowledge about the distribution of water resources and poor management of their usage. Remote sensing provides critical data for mapping water resources, measuring hydrological fluxes, monitoring drought and flooding inundation, while geographic information systems (GIS) provide the best tools for water resources, drought and flood risk management. This special issue presents the best practices, cutting-edge technologies and applications of remote sensing, GIS and hydrological models for water resource mapping, satellite rainfall measurements, runoff simulation, water body and flood inundation mapping, and risk management. The latest technologies applied include 3D surface model analysis and visualization of glaciers, unmanned aerial vehicle (UAV) video image classification for turfgrass mapping and irrigation planning, ground penetration radar for soil moisture estimation, the Tropical Rainfall Measuring Mission (TRMM) and the Global Precipitation Measurement (GPM) satellite rainfall measurements, storm hyetography analysis, rainfall runoff and urban flooding simulation, and satellite radar and optical image classification for urban water bodies and flooding inundation. The application of those technologies is expected to greatly relieve the pressures on water resources and allow better mitigation of and adaptation to the disastrous impact of droughts and flooding.
A Review on Interpretable and Explainable Artificial Intelligence in Hydroclimatic Applications
(2022-04-11) Başağaoğlu, Hakan; Chakraborty, Debaditya; Lago, Cesar Do; Gutierrez, Lilianna; Şahinli, Mehmet Arif; Giacomoni, Marcio; Furl, Chad; Mirchi, Ali; Moriasi, Daniel N.; Şengör, Sema Sevinç
This review focuses on the use of Interpretable Artificial Intelligence (IAI) and eXplainable Artificial Intelligence (XAI) models for data imputations and numerical or categorical hydroclimatic predictions from nonlinearly combined multidimensional predictors. The AI models considered in this paper involve Extreme Gradient Boosting, Light Gradient Boosting, Categorical Boosting, Extremely Randomized Trees, and Random Forest. These AI models can transform into XAI models when they are coupled with the explanatory methods such as the Shapley additive explanations and local interpretable model-agnostic explanations. The review highlights that the IAI models are capable of unveiling the rationale behind the predictions while XAI models are capable of discovering new knowledge and justifying AI-based results, which are critical for enhanced accountability of AI-driven predictions. The review also elaborates the importance of domain knowledge and interventional IAI modeling, potential advantages and disadvantages of hybrid IAI and non-IAI predictive modeling, unequivocal importance of balanced data in categorical decisions, and the choice and performance of IAI versus physics-based modeling. The review concludes with a proposed XAI framework to enhance the interpretability and explainability of AI models for hydroclimatic applications.
A Robust Personalized Classification Method for Breast Cancer Metastasis Prediction
(2022-10-29) Adnan, Nahim; Najnin, Tanzira; Ruan, Jianhua
Accurate prediction of breast cancer metastasis in the early stages of cancer diagnosis is crucial to reduce cancer-related deaths. With the availability of gene expression datasets, many machine-learning models have been proposed to predict breast cancer metastasis using thousands of genes simultaneously. However, the prediction accuracy of the models using gene expression often suffers from the diverse molecular characteristics across different datasets. Additionally, breast cancer is known to have many subtypes, which hinders the performance of the models aimed at all subtypes. To overcome the heterogeneous nature of breast cancer, we propose a method to obtain personalized classifiers that are trained on subsets of patients selected using the similarities between training and testing patients. Results on multiple independent datasets showed that our proposed approach significantly improved prediction accuracy compared to the models trained on the complete training dataset and models trained on specific cancer subtypes. Our results also showed that personalized classifiers trained on positively and negatively correlated patients outperformed classifiers trained only on positively correlated patients, highlighting the importance of selecting proper patient subsets for constructing personalized classifiers. Additionally, our proposed approach obtained more robust features than the other models and identified different features for different patients, making it a promising tool for designing personalized medicine for cancer patients.
A Self-Supervised Learning Framework for Classifying Microarray Gene Expression Data
(UTSA Department of Computer Science, 2006-10) Lu, Yijuan; Tian, Qi; Liu, Feng; Sanchez, Maribel; Wang, Yufeng
It is important to develop computational methods that can effectively resolve two intrinsic problems in microarray data: high dimensionality and small sample size. In this paper, we propose a self-supervised learning framework for classifying microarray gene expression data using Kernel Discriminant-EM (KDEM) algorithm. This framework applies self-supervised learning techniques in an optimal nonlinear discriminating subspace. It efficiently utilizes a large set of unlabeled data to compensate for the insufficiency of a small set of labeled data and it extends linear algorithm in DEM to kernel algorithm to handle nonlinearly separable data in a lower dimensional space. Extensive experiments on the Plasmodium falciparum expression profiles show the promising performance of the approach.
A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination
(UTSA Department of Computer Science, 2008-06) Niedzielski, David; Gampe, Andreas; von Ronne, Jeffery; Psarris, Kleanthis
The Java programming language requires that out-of-bounds array accesses produce runtime exceptions. In general, this requires a dynamic bounds check each time an array element is accessed. However, if it can be proven that the array index does not exceed the bounds of the array, then the bounds check can be eliminated. We present a new algorithm based on extended Static Single Assignment (eSSA) form that builds a directed, weighted inequality graph representing control flow qualified, linear constraints among program variables derived from program statements. Our system then employs a customized depth-first search exploration algorithm to reason about relationships among variables, and provides a verifiable proof of its conclusions. This proof can be passed to and verified by a runtime system to minimize the run time performance impact of this analysis. Our system is novel in several respects. It takes into consideration both control flow and data flow when analyzing the constraint system; it handles general linear inequalities instead of simple difference constraints; and it provides verifiable proofs for its claims. We present experimental results which demonstrate that this method eliminates more bounds checks, and when combined with runtime verification, results in a lower runtime cost than prior work. Overall, this method improves performance by up to about 10% on the reported benchmarks.

Browse

Browsing College of Sciences by Title