-
Article
Reluplex: a calculus for reasoning about deep neural networks
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty i...
-
Article
Open AccessAquila enables reference-assisted diploid personal genome assembly and comprehensive variant detection based on linked reads
We introduce Aquila, a new approach to variant discovery in personal genomes, which is critical for uncovering the genetic contributions to health and disease. Aquila uses a reference sequence and linked-read ...
-
Chapter and Conference Paper
The Move Prover
The Libra blockchain is designed to store billions of dollars in assets, so the security of code that executes transactions is important. The Libra blockchain has a new language for implementing transactions, ...
-
Article
Open AccessMebendazole for Differentiation Therapy of Acute Myeloid Leukemia Identified by a Lineage Maturation Index
Accurate assessment of changes in cellular differentiation status in response to drug treatments or genetic perturbations is crucial for understanding tumorigenesis and develo** novel therapeutics for human ...
-
Chapter and Conference Paper
The Marabou Framework for Verification and Analysis of Deep Neural Networks
Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that...
-
Article
Open AccessSystematic discovery of mutation-specific synthetic lethals by mining pan-cancer human primary tumor data
Two genes are synthetically lethal (SL) when defects in both are lethal to a cell but a single defect is non-lethal. SL partners of cancer mutations are of great interest as pharmacological targets; however, i...
-
Article
Open AccessA geographically-diverse collection of 418 human gut microbiome pathway genome databases
Advances in high-throughput sequencing are resha** how we perceive microbial communities inhabiting the human body, with implications for therapeutic interventions. Several large-scale datasets derived from ...
-
Chapter and Conference Paper
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty i...
-
Article
Open AccessThe multiple PDZ domain protein Mpdz/MUPP1 regulates opioid tolerance and opioid-induced hyperalgesia
Opioids are a mainstay for the treatment of chronic pain. Unfortunately, therapy-limiting maladaptations such as loss of treatment effect (tolerance), and paradoxical opioid-induced hyperalgesia (OIH) can occu...
-
Article
Open AccessTowards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach
High-throughput assays such as mass spectrometry have opened up the possibility for large-scale in vivo measurements of the metabolome. This data could potentially be used to estimate kinetic parameters for many ...
-
Chapter and Conference Paper
Model Checking Cell Biology
Mathematical models of real biological systems have predominantly been deterministic or stochastic continuous models. However, there are reasons to believe that at least some processes can be modeled in a “dig...
-
Chapter and Conference Paper
Are Cells Asynchronous Circuits?
Cells do not seem to have “clocks” in the same sense as synchronous sequential digital circuits. But cells must operate extremely reliably in spite of large amounts of noise and environmental variations which ...
-
Article
Open AccessBoolean implication networks derived from large scale, whole genome microarray datasets
We describe a method for extracting Boolean implications (if-then relationships) in very large amounts of gene expression microarray data. A meta-analysis of data from thousands of microarrays for humans, mice...
-
Chapter and Conference Paper
Formal Verification and Biology
The essence of formal verification is the modeling, analysis, and, ultimately, understanding of large reactive systems. How do many parts interact to produce appropriate global behavior? How are properties gua...
-
Chapter
A Retrospective on Murϕ
Murϕ is a formal verification system for finite-state concurrent systems developed as a research project at Stanford University. It has been widely used for many protocols especially for multiprocessor cache cohe...
-
Chapter and Conference Paper
A Decision Procedure for Bit-Vectors and Arrays
STP is a decision procedure for the satisfiability of quantifier-free formulas in the theory of bit-vectors and arrays that has been optimized for large problems encountered in software analysis applications. ...
-
Chapter and Conference Paper
The Pathalyzer: A Tool for Analysis of Signal Transduction Pathways
The Pathalyzer is a program for analyzing large-scale signal transduction networks. Reactions and their substrates and products are represented as transitions and places in a safe Petri net. The user can inter...
-
Chapter and Conference Paper
Multiple Representations of Biological Processes
This paper describes representations of biological processes based on Rewriting Logic and Petri net formalisms and map**s between these representations used in the Pathway Logic Assistant. The map**s are s...
-
Chapter and Conference Paper
An Incremental Heap Canonicalization Algorithm
The most expensive operation in explicit state model checking is the hash computation required to store the explored states in a hash table. One way to reduce this computation is to compute the hash incrementa...
-
Chapter and Conference Paper
Using Interface Refinement to Integrate Formal Verification into the Design Cycle
We present a practical compositional interface refinement methodology which helps to integrate formal verification with the design process. One of the main verification challenges is to keep up with the change...
