David Dill
Donald E. Knuth Professor in the School of Engineering, Emeritus
Computer Science
Bio
Dill has interests in the theory and application of formal verification techniques to system designs, which encompass hardware, protocols, and software and in computational systems biology. He has also done research in asynchronous circuit verification and synthesis, and in verification methods for hard real-time systems.
He retired in 2017 and is no longer taking new students. He is collaborating with researchers at Stanford and elsewhere.
Honors & Awards
-
Member, National Academy of Engineering (2013)
-
Fellow, American Academy of Arts and Sciences (2013)
-
Fellow, IEEE
-
Fellow, ACM
-
Pioneer Award, Electronic Frontier Foundation
-
CAV Award for developing the Reluplex algorithm, for verifying real-world deep neural networks., International Conference on Computer-Aided Verification (2024)
-
CAV Award for pioneering contributions satisfiability modulo theories (SMT)., International Conference on Computer-Aided Verification (2021)
-
Alonzo Church Award for outstanding contributions to logic., ACM SIGLOG, EATCS, EACSL, and KGS (2016)
-
CAV Award for fundamental contributions to the theory of real-time systems verification., International Conference on Computer-Aided Verification (2008)
Program Affiliations
-
Symbolic Systems Program
Professional Education
-
PhD, Carnegie Mellon (1987)
Current Research and Scholarly Interests
Secure and reliable blockchain technology at Facebook.
2023-24 Courses
-
Independent Studies (16)
- Advanced Reading and Research
CS 499 (Aut, Win, Spr, Sum) - Advanced Reading and Research
CS 499P (Aut, Win, Spr, Sum) - Biomedical Informatics Teaching Methods
BIOMEDIN 290 (Win, Spr, Sum) - Curricular Practical Training
CS 390A (Aut, Win, Spr, Sum) - Curricular Practical Training
CS 390B (Aut, Win, Spr, Sum) - Curricular Practical Training
CS 390C (Aut, Win, Spr, Sum) - Directed Reading and Research
BIOMEDIN 299 (Aut, Win, Spr, Sum) - Independent Project
CS 399 (Aut, Win, Spr, Sum) - Independent Project
CS 399P (Aut, Win, Spr, Sum) - Independent Work
CS 199 (Aut, Win, Spr, Sum) - Independent Work
CS 199P (Aut, Win, Spr, Sum) - Medical Scholars Research
BIOMEDIN 370 (Aut, Win, Spr, Sum) - Part-time Curricular Practical Training
CS 390D (Aut, Win) - Programming Service Project
CS 192 (Aut, Win, Spr, Sum) - Senior Project
CS 191 (Aut, Win, Spr, Sum) - Writing Intensive Senior Research Project
CS 191W (Aut, Win, Spr)
- Advanced Reading and Research
Graduate and Fellowship Programs
-
Biomedical Data Science (Phd Program)
All Publications
-
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences
JOURNAL OF AUTOMATED REASONING
2023; 67 (3)
View details for DOI 10.1007/s10817-023-09682-2
View details for Web of Science ID 001067178200001
-
Reasoning About Vectors Using an SMT Theory of Sequences
SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 125-143
View details for DOI 10.1007/978-3-031-10769-6_9
View details for Web of Science ID 000876376400009
-
Reluplex: a calculus for reasoning about deep neural networks
FORMAL METHODS IN SYSTEM DESIGN
2021
View details for DOI 10.1007/s10703-021-00363-7
View details for Web of Science ID 000668847200001
-
Aquila_stLFR: diploid genome assembly based structural variant calling package for stLFR linked-reads.
Bioinformatics advances
2021; 1 (1): vbab007
Abstract
Identifying structural variants (SVs) is critical in health and disease, however, detecting them remains a challenge. Several linked-read sequencing technologies, including 10X Genomics, TELL-Seq and single tube long fragment read (stLFR), have been recently developed as cost-effective approaches to reconstruct multi-megabase haplotypes (phase blocks) from sequence data of a single sample. These technologies provide an optimal sequencing platform to characterize SVs, though few computational algorithms can utilize them. Thus, we developed Aquila_stLFR, an approach that resolves SVs through haplotype-based assembly of stLFR linked-reads.Aquila_stLFR first partitions long fragment reads into two haplotype-specific blocks with the assistance of the high-quality reference genome, by taking advantage of the potential phasing ability of the linked-read itself. Each haplotype is then assembled independently, to achieve a complete diploid assembly to finally reconstruct the genome-wide SVs. We benchmarked Aquila_stLFR on a well-studied sample, NA24385, and showed Aquila_stLFR can detect medium to large size deletions (50 bp-10 kb) with high sensitivity and medium-size insertions (50 bp-1 kb) with high specificity.Source code and documentation are available on https://github.com/maiziex/Aquila_stLFR.Supplementary data are available at Bioinformatics Advances online.
View details for DOI 10.1093/bioadv/vbab007
View details for PubMedID 36700103
View details for PubMedCentralID PMC9710574
-
Aquila enables reference-assisted diploid personal genome assembly and comprehensive variant detection based on linked reads.
Nature communications
2021; 12 (1): 1077
Abstract
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 data to generate a high quality diploid genome assembly, from which it then comprehensively detects and phases personal genetic variation. The contigs of the assemblies from our libraries cover >95% of the human reference genome, with over 98% of that in a diploid state. Thus, the assemblies support detection and accurate genotyping of the most prevalent types of human genetic variation, including single nucleotide polymorphisms (SNPs), small insertions and deletions (small indels), and structural variants (SVs), in all but the most difficult regions. All heterozygous variants are phased in blocks that can approach arm-level length. The final output of Aquila is a diploid and phased personal genome sequence, and a phased Variant Call Format (VCF) file that also contains homozygous and a few unphased heterozygous variants. Aquila represents a cost-effective approach that can be applied to cohorts for variation discovery or association studies, or to single individuals with rare phenotypes that could be caused by SVs or compound heterozygosity.
View details for DOI 10.1038/s41467-021-21395-x
View details for PubMedID 33597536
-
The m6A RNA demethylase FTO is a HIF-independent synthetic lethal partner with the VHL tumor suppressor.
Proceedings of the National Academy of Sciences of the United States of America
2020
Abstract
Loss of the von Hippel-Lindau (VHL) tumor suppressor is a hallmark feature of renal clear cell carcinoma. VHL inactivation results in the constitutive activation of the hypoxia-inducible factors (HIFs) HIF-1 and HIF-2 and their downstream targets, including the proangiogenic factors VEGF and PDGF. However, antiangiogenic agents and HIF-2 inhibitors have limited efficacy in cancer therapy due to the development of resistance. Here we employed an innovative computational platform, Mining of Synthetic Lethals (MiSL), to identify synthetic lethal interactions with the loss of VHL through analysis of primary tumor genomic and transcriptomic data. Using this approach, we identified a synthetic lethal interaction between VHL and the m6A RNA demethylase FTO in renal cell carcinoma. MiSL identified FTO as a synthetic lethal partner of VHL because deletions of FTO are mutually exclusive with VHL loss in pan cancer datasets. Moreover, FTO expression is increased in VHL-deficient ccRCC tumors compared to normal adjacent tissue. Genetic inactivation of FTO using multiple orthogonal approaches revealed that FTO inhibition selectively reduces the growth and survival of VHL-deficient cells in vitro and in vivo. Notably, FTO inhibition reduced the survival of both HIF wild type and HIF-deficient tumors, identifying FTO as an HIF-independent vulnerability of VHL-deficient cancers. Integrated analysis of transcriptome-wide m6A-seq and mRNA-seq analysis identified the glutamine transporter SLC1A5 as an FTO target that promotes metabolic reprogramming and survival of VHL-deficient ccRCC cells. These findings identify FTO as a potential HIF-independent therapeutic target for the treatment of VHL-deficient renal cell carcinoma.
View details for DOI 10.1073/pnas.2000516117
View details for PubMedID 32817424
-
The Move Prover
SPRINGER INTERNATIONAL PUBLISHING AG. 2020: 137-150
View details for DOI 10.1007/978-3-030-53288-8_7
View details for Web of Science ID 000695276000007
-
Mebendazole for Differentiation Therapy of Acute Myeloid Leukemia Identified by a Lineage Maturation Index.
Scientific reports
2019; 9 (1): 16775
Abstract
Accurate assessment of changes in cellular differentiation status in response to drug treatments or genetic perturbations is crucial for understanding tumorigenesis and developing novel therapeutics for human cancer. We have developed a novel computational approach, the Lineage Maturation Index (LMI), to define the changes in differentiation state of hematopoietic malignancies based on their gene expression profiles. We have confirmed that the LMI approach can detect known changes of differentiation state in both normal and malignant hematopoietic cells. To discover novel differentiation therapies, we applied this approach to analyze the gene expression profiles of HL-60 leukemia cells treated with a small molecule drug library. Among multiple drugs that significantly increased the LMIs, we identified mebendazole, an anti-helminthic clinically used for decades with no known significant toxicity. We tested the differentiation activity of mebendazole using primary leukemia blast cells isolated from human acute myeloid leukemia (AML) patients. We determined that treatment with mebendazole induces dramatic differentiation of leukemia blast cells as shown by cellular morphology and cell surface markers. Furthermore, mebendazole treatment significantly extended the survival of leukemia-bearing mice in a xenograft model. These findings suggest that mebendazole may be utilized as a low toxicity therapeutic for human acute myeloid leukemia and confirm the LMI approach as a robust tool for the discovery of novel differentiation therapies for cancer.
View details for DOI 10.1038/s41598-019-53290-3
View details for PubMedID 31727951
-
The Marabou Framework for Verification and Analysis of Deep Neural Networks
SPRINGER INTERNATIONAL PUBLISHING AG. 2019: 443–52
View details for DOI 10.1007/978-3-030-25540-4_26
View details for Web of Science ID 000491468000026
-
IDH1 Mutant AML Is Susceptible to Targeting De Novo Lipid Synthesis Independent of 2-Hydroxyglutarate and Has a Distinct Metabolic Profile from IDH2 Mutant AML
AMER SOC HEMATOLOGY. 2018
View details for DOI 10.1182/blood-2018-99-115040
View details for Web of Science ID 000454837601149
-
Systematic discovery of mutation-specific synthetic lethals by mining pan-cancer human primary tumor data.
Nature communications
2017; 8: 15580-?
Abstract
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, identifying them by cell line-based methods is challenging. Here we develop MiSL (Mining Synthetic Lethals), an algorithm that mines pan-cancer human primary tumour data to identify mutation-specific SL partners for specific cancers. We apply MiSL to 12 different cancers and predict 145,891 SL partners for 3,120 mutations, including known mutation-specific SL partners. Comparisons with functional screens show that MiSL predictions are enriched for SLs in multiple cancers. We extensively validate a SL interaction identified by MiSL between the IDH1 mutation and ACACA in leukaemia using gene targeting and patient-derived xenografts. Furthermore, we apply MiSL to pinpoint genetic biomarkers for drug sensitivity. These results demonstrate that MiSL can accelerate precision oncology by identifying mutation-specific targets and biomarkers.
View details for DOI 10.1038/ncomms15580
View details for PubMedID 28561042
-
Systematic discovery of mutation-specific synthetic lethals by mining pan-cancer human primary tumor data.
Nature communications
2017; 8: 15580-?
Abstract
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, identifying them by cell line-based methods is challenging. Here we develop MiSL (Mining Synthetic Lethals), an algorithm that mines pan-cancer human primary tumour data to identify mutation-specific SL partners for specific cancers. We apply MiSL to 12 different cancers and predict 145,891 SL partners for 3,120 mutations, including known mutation-specific SL partners. Comparisons with functional screens show that MiSL predictions are enriched for SLs in multiple cancers. We extensively validate a SL interaction identified by MiSL between the IDH1 mutation and ACACA in leukaemia using gene targeting and patient-derived xenografts. Furthermore, we apply MiSL to pinpoint genetic biomarkers for drug sensitivity. These results demonstrate that MiSL can accelerate precision oncology by identifying mutation-specific targets and biomarkers.
View details for DOI 10.1038/ncomms15580
View details for PubMedID 28561042
-
A geographically-diverse collection of 418 human gut microbiome pathway genome databases
SCIENTIFIC DATA
2017; 4
Abstract
Advances in high-throughput sequencing are reshaping how we perceive microbial communities inhabiting the human body, with implications for therapeutic interventions. Several large-scale datasets derived from hundreds of human microbiome samples sourced from multiple studies are now publicly available. However, idiosyncratic data processing methods between studies introduce systematic differences that confound comparative analyses. To overcome these challenges, we developed GutCyc, a compendium of environmental pathway genome databases (ePGDBs) constructed from 418 assembled human microbiome datasets using MetaPathways, enabling reproducible functional metagenomic annotation. We also generated metabolic network reconstructions for each metagenome using the Pathway Tools software, empowering researchers and clinicians interested in visualizing and interpreting metabolic pathways encoded by the human gut microbiome. For the first time, GutCyc provides consistent annotations and metabolic pathway predictions, making possible comparative community analyses between health and disease states in inflammatory bowel disease, Crohn's disease, and type 2 diabetes. GutCyc data products are searchable online, or may be downloaded and explored locally using MetaPathways and Pathway Tools.
View details for DOI 10.1038/sdata.2017.35
View details for PubMedID 28398290
-
Our Elections Are Not Secure
SCIENTIFIC AMERICAN
2017; 316 (3): 12
View details for DOI 10.1038/scientificamerican0317-12
View details for Web of Science ID 000399228200011
View details for PubMedID 28207717
-
Towards Proving the Adversarial Robustness of Deep Neural Networks
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
2017: 19–26
View details for DOI 10.4204/EPTCS.257.3
View details for Web of Science ID 000439354100004
-
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 97–117
View details for DOI 10.1007/978-3-319-63387-9_5
View details for Web of Science ID 000432196400005
-
Isocitrate Dehydrogenase 1 Mutant Cancers Are Metabolically Vulnerable to Inhibition of Acetyl CoA Carboxylase Via a 2-Hydroxyglutarate Independent Mechanism
AMER SOC HEMATOLOGY. 2016
View details for Web of Science ID 000394446802035
-
Cell cycle progression in Caulobacter requires a nucleoid-associated protein with high AT sequence recognition
PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA
2016; 113 (40): E5952-E5961
Abstract
Faithful cell cycle progression in the dimorphic bacterium Caulobacter crescentus requires spatiotemporal regulation of gene expression and cell pole differentiation. We discovered an essential DNA-associated protein, GapR, that is required for Caulobacter growth and asymmetric division. GapR interacts with adenine and thymine (AT)-rich chromosomal loci, associates with the promoter regions of cell cycle-regulated genes, and shares hundreds of recognition sites in common with known master regulators of cell cycle-dependent gene expression. GapR target loci are especially enriched in binding sites for the transcription factors GcrA and CtrA and overlap with nearly all of the binding sites for MucR1, a regulator that controls the establishment of swarmer cell fate. Despite constitutive synthesis, GapR accumulates preferentially in the swarmer compartment of the predivisional cell. Homologs of GapR, which are ubiquitous among the α-proteobacteria and are encoded on multiple bacteriophage genomes, also accumulate in the predivisional cell swarmer compartment when expressed in Caulobacter The Escherichia coli nucleoid-associated protein H-NS, like GapR, selectively associates with AT-rich DNA, yet it does not localize preferentially to the swarmer compartment when expressed exogenously in Caulobacter, suggesting that recognition of AT-rich DNA is not sufficient for the asymmetric accumulation of GapR. Further, GapR does not silence the expression of H-NS target genes when expressed in E. coli, suggesting that GapR and H-NS have distinct functions. We propose that Caulobacter has co-opted a nucleoid-associated protein with high AT recognition to serve as a mediator of cell cycle progression.
View details for DOI 10.1073/pnas.1612579113
View details for Web of Science ID 000384528900022
View details for PubMedID 27647925
View details for PubMedCentralID PMC5056096
-
A Pharmacogenetic Discovery: Cystamine Protects Against Haloperidol-Induced Toxicity and Ischemic Brain Injury
GENETICS
2016; 203 (1): 599-?
Abstract
Haloperidol is an effective antipsychotic agent, but it causes Parkinsonian-like extrapyramidal symptoms in the majority of treated subjects. To address this treatment-limiting toxicity, we analyzed a murine genetic model of haloperidol-induced toxicity (HIT). Analysis of a panel of consomic strains indicated that a genetic factor on chromosome 10 had a significant effect on susceptibility to HIT. We analyzed a whole-genome SNP database to identify allelic variants that were uniquely present on chromosome 10 in the strain that was previously shown to exhibit the highest level of susceptibility to HIT. This analysis implicated allelic variation within pantetheinase genes (Vnn1 and Vnn3), which we propose impaired the biosynthesis of cysteamine, could affect susceptibility to HIT. We demonstrate that administration of cystamine, which is rapidly metabolized to cysteamine, could completely prevent HIT in the murine model. Many of the haloperidol-induced gene expression changes in the striatum of the susceptible strain were reversed by cystamine coadministration. Since cystamine administration has previously been shown to have other neuroprotective actions, we investigated whether cystamine administration could have a broader neuroprotective effect. Cystamine administration caused a 23% reduction in infarct volume after experimentally induced cerebral ischemia. Characterization of this novel pharmacogenetic factor for HIT has identified a new approach for preventing the treatment-limiting toxicity of an antipsychotic agent, which could also be used to reduce the extent of brain damage after stroke.
View details for DOI 10.1534/genetics.115.184648
View details for PubMedID 26993135
-
The multiple PDZ domain protein Mpdz/MUPP1 regulates opioid tolerance and opioid-induced hyperalgesia
BMC GENOMICS
2016; 17
Abstract
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 occur. The objective of this study was to identify genes responsible for opioid tolerance and OIH.These studies used a well-established model of ascending morphine administration to induce tolerance, OIH and other opioid maladaptations in 23 strains of inbred mice. Genome-wide computational genetic mapping was then applied to the data in combination with a false discovery rate filter. Transgenic mice, gene expression experiments and immunoprecipitation assays were used to confirm the functional roles of the most strongly linked gene. The behavioral data processed using computational genetic mapping and false discovery rate filtering provided several strongly linked biologically plausible gene associations. The strongest of these was the highly polymorphic Mpdz gene coding for the post-synaptic scaffolding protein Mpdz/MUPP1. Heterozygous Mpdz +/- mice displayed reduced opioid tolerance and OIH. Mpdz gene expression and Mpdz/MUPP1 protein levels were lower in the spinal cords of low-adapting 129S1/Svlm mice than in high-adapting C57BL/6 mice. Morphine did not alter Mpdz expression levels. In addition, association of Mpdz/MUPP1 with its known binding partner CaMKII did not differ between these high- and low-adapting strains.The degrees of maladaptive changes in response to repeated administration of morphine vary greatly across inbred strains of mice. Variants of the multiple PDZ domain gene Mpdz may contribute to the observed inter-strain variability in tolerance and OIH by virtue of changes in the level of their expression.
View details for DOI 10.1186/s12864-016-2634-1
View details for PubMedID 27129385
-
CauloBrowser: A systems biology resource for Caulobacter crescentus.
Nucleic acids research
2016; 44 (D1): D640-5
Abstract
Caulobacter crescentus is a premier model organism for studying the molecular basis of cellular asymmetry. The Caulobacter community has generated a wealth of high-throughput spatiotemporal databases including data from gene expression profiling experiments (microarrays, RNA-seq, ChIP-seq, ribosome profiling, LC-ms proteomics), gene essentiality studies (Tn-seq), genome wide protein localization studies, and global chromosome methylation analyses (SMRT sequencing). A major challenge involves the integration of these diverse data sets into one comprehensive community resource. To address this need, we have generated CauloBrowser (www.caulobrowser.org), an online resource for Caulobacter studies. This site provides a user-friendly interface for quickly searching genes of interest and downloading genome-wide results. Search results about individual genes are displayed as tables, graphs of time resolved expression profiles, and schematics of protein localization throughout the cell cycle. In addition, the site provides a genome viewer that enables customizable visualization of all published high-throughput genomic data. The depth and diversity of data sets collected by the Caulobacter community makes CauloBrowser a unique and valuable systems biology resource.
View details for DOI 10.1093/nar/gkv1050
View details for PubMedID 26476443
View details for PubMedCentralID PMC4702786
-
CauloBrowser: A systems biology resource for Caulobacter crescentus.
Nucleic acids research
2016; 44 (D1): D640-5
Abstract
Caulobacter crescentus is a premier model organism for studying the molecular basis of cellular asymmetry. The Caulobacter community has generated a wealth of high-throughput spatiotemporal databases including data from gene expression profiling experiments (microarrays, RNA-seq, ChIP-seq, ribosome profiling, LC-ms proteomics), gene essentiality studies (Tn-seq), genome wide protein localization studies, and global chromosome methylation analyses (SMRT sequencing). A major challenge involves the integration of these diverse data sets into one comprehensive community resource. To address this need, we have generated CauloBrowser (www.caulobrowser.org), an online resource for Caulobacter studies. This site provides a user-friendly interface for quickly searching genes of interest and downloading genome-wide results. Search results about individual genes are displayed as tables, graphs of time resolved expression profiles, and schematics of protein localization throughout the cell cycle. In addition, the site provides a genome viewer that enables customizable visualization of all published high-throughput genomic data. The depth and diversity of data sets collected by the Caulobacter community makes CauloBrowser a unique and valuable systems biology resource.
View details for DOI 10.1093/nar/gkv1050
View details for PubMedID 26476443
View details for PubMedCentralID PMC4702786
-
Deciphering Cancer Biology using Boolean Methods
IEEE. 2016: 150–54
View details for Web of Science ID 000389035600022
-
Boolean Implication Mining for Synthetic Lethal Interactions in AML Identifies Acetyl-CoA Carboxylase As a Synthetic Lethal Partner of the IDH1 mutation
AMER SOC HEMATOLOGY. 2015
View details for Web of Science ID 000368019004204
-
Discovery of differentiation therapeutics using a systems biology approach
AMER ASSOC CANCER RESEARCH. 2015
View details for DOI 10.1158/1538-7445.TRANSCAGEN-A2-35
View details for Web of Science ID 000370972600082
-
A systems biology approach for the discovery of differentiation therapeutics
AMER ASSOC CANCER RESEARCH. 2015
View details for DOI 10.1158/1538-7445.COMPSYSBIO-B2-12
View details for Web of Science ID 000370971000059
-
Deciphering the cancer methylome with Boolean implications to find novel drivers of aberrant DNA methylation and actionable drug targets
AMER ASSOC CANCER RESEARCH. 2015
View details for DOI 10.1158/1538-7445.COMPSYSBIO-B2-20
View details for Web of Science ID 000370971000065
-
Towards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach
BMC SYSTEMS BIOLOGY
2015; 9
Abstract
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 metabolic reactions. However, high-throughput in vivo measurements have special properties that are not taken into account in existing methods for estimating kinetic parameters, including significant relative errors in measurements of metabolite concentrations and reaction rates, and reactions with multiple substrates and products, which are sometimes reversible. A new method is needed to estimate kinetic parameters taking into account these factors.A new method, InVEst (In Vivo Estimation), is described for estimating reaction kinetic parameters, which addresses the specific challenges of in vivo data. InVEst uses maximum likelihood estimation based on a model where all measurements have relative errors. Simulations show that InVEst produces accurate estimates for a reversible enzymatic reaction with multiple reactants and products, that estimated parameters can be used to predict the effects of genetic variants, and that InVEst is more accurate than general least squares and graphic methods on data with relative errors. InVEst uses the bootstrap method to evaluate the accuracy of its estimates.InVEst addresses several challenges of in vivo data, which are not taken into account by existing methods. When data have relative errors, InVEst produces more accurate and robust estimates. InVEst also provides useful information about estimation accuracy using bootstrapping. It has potential applications of quantifying the effects of genetic variants, inference of the target of a mutation or drug treatment and improving flux estimation.
View details for DOI 10.1186/s12918-015-0214-7
View details for Web of Science ID 000362397100001
View details for PubMedID 26437964
View details for PubMedCentralID PMC4595320
-
The role of Abcb5 alleles in susceptibility to haloperidol-induced toxicity in mice and humans.
PLoS medicine
2015; 12 (2)
Abstract
We know very little about the genetic factors affecting susceptibility to drug-induced central nervous system (CNS) toxicities, and this has limited our ability to optimally utilize existing drugs or to develop new drugs for CNS disorders. For example, haloperidol is a potent dopamine antagonist that is used to treat psychotic disorders, but 50% of treated patients develop characteristic extrapyramidal symptoms caused by haloperidol-induced toxicity (HIT), which limits its clinical utility. We do not have any information about the genetic factors affecting this drug-induced toxicity. HIT in humans is directly mirrored in a murine genetic model, where inbred mouse strains are differentially susceptible to HIT. Therefore, we genetically analyzed this murine model and performed a translational human genetic association study.A whole genome SNP database and computational genetic mapping were used to analyze the murine genetic model of HIT. Guided by the mouse genetic analysis, we demonstrate that genetic variation within an ABC-drug efflux transporter (Abcb5) affected susceptibility to HIT. In situ hybridization results reveal that Abcb5 is expressed in brain capillaries, and by cerebellar Purkinje cells. We also analyzed chromosome substitution strains, imaged haloperidol abundance in brain tissue sections and directly measured haloperidol (and its metabolite) levels in brain, and characterized Abcb5 knockout mice. Our results demonstrate that Abcb5 is part of the blood-brain barrier; it affects susceptibility to HIT by altering the brain concentration of haloperidol. Moreover, a genetic association study in a haloperidol-treated human cohort indicates that human ABCB5 alleles had a time-dependent effect on susceptibility to individual and combined measures of HIT. Abcb5 alleles are pharmacogenetic factors that affect susceptibility to HIT, but it is likely that additional pharmacogenetic susceptibility factors will be discovered.ABCB5 alleles alter susceptibility to HIT in mouse and humans. This discovery leads to a new model that (at least in part) explains inter-individual differences in susceptibility to a drug-induced CNS toxicity.
View details for DOI 10.1371/journal.pmed.1001782
View details for PubMedID 25647612
-
The role of abcb5 alleles in susceptibility to haloperidol-induced toxicity in mice and humans.
PLoS medicine
2015; 12 (2): e1001782
Abstract
We know very little about the genetic factors affecting susceptibility to drug-induced central nervous system (CNS) toxicities, and this has limited our ability to optimally utilize existing drugs or to develop new drugs for CNS disorders. For example, haloperidol is a potent dopamine antagonist that is used to treat psychotic disorders, but 50% of treated patients develop characteristic extrapyramidal symptoms caused by haloperidol-induced toxicity (HIT), which limits its clinical utility. We do not have any information about the genetic factors affecting this drug-induced toxicity. HIT in humans is directly mirrored in a murine genetic model, where inbred mouse strains are differentially susceptible to HIT. Therefore, we genetically analyzed this murine model and performed a translational human genetic association study.A whole genome SNP database and computational genetic mapping were used to analyze the murine genetic model of HIT. Guided by the mouse genetic analysis, we demonstrate that genetic variation within an ABC-drug efflux transporter (Abcb5) affected susceptibility to HIT. In situ hybridization results reveal that Abcb5 is expressed in brain capillaries, and by cerebellar Purkinje cells. We also analyzed chromosome substitution strains, imaged haloperidol abundance in brain tissue sections and directly measured haloperidol (and its metabolite) levels in brain, and characterized Abcb5 knockout mice. Our results demonstrate that Abcb5 is part of the blood-brain barrier; it affects susceptibility to HIT by altering the brain concentration of haloperidol. Moreover, a genetic association study in a haloperidol-treated human cohort indicates that human ABCB5 alleles had a time-dependent effect on susceptibility to individual and combined measures of HIT. Abcb5 alleles are pharmacogenetic factors that affect susceptibility to HIT, but it is likely that additional pharmacogenetic susceptibility factors will be discovered.ABCB5 alleles alter susceptibility to HIT in mouse and humans. This discovery leads to a new model that (at least in part) explains inter-individual differences in susceptibility to a drug-induced CNS toxicity.
View details for DOI 10.1371/journal.pmed.1001782
View details for PubMedID 25647612
View details for PubMedCentralID PMC4315575
-
Mutant WT1 is associated with DNA hypermethylation of PRC2 targets in AML and responds to EZH2 inhibition.
Blood
2015; 125 (2): 316-326
Abstract
Acute myeloid leukemia (AML) is associated with deregulation of DNA methylation; however, many cases do not bear mutations in known regulators of CpG methylation. We found that mutations in WT1, IDH2, and CEBPA were strongly linked to DNA hypermethylation in AML using a novel integrative analysis of TCGA data based on Boolean implications, if-then rules that identify all individual CpG sites that are hypermethylated in the presence of a mutation. Introduction of mutant WT1 (WT1mut) into wildtype AML cells induced DNA hypermethylation, confirming mutant WT1 to be causally associated with DNA hypermethylation. Methylated genes in WT1mut primary patient samples were highly enriched for polycomb repressor complex 2 (PRC2) targets, implicating PRC2 dysregulation in WT1mut leukemogenesis. We found that PRC2 target genes were aberrantly repressed in WT1mut AML, and that expression of mutant WT1 in CD34+ cord blood cells induced myeloid differentiation block. Treatment of WT1mut AML cells with shRNA or pharmacologic PRC2/EZH2 inhibitors promoted myeloid differentiation, suggesting EZH2 inhibitors may be active in this AML subtype. Our results highlight a strong association between mutant WT1 and DNA hypermethylation in AML, and demonstrate that Boolean implications can be used to decipher mutation-specific methylation patterns that may lead to therapeutic insights.
View details for DOI 10.1182/blood-2014-03-566018
View details for PubMedID 25398938
-
The global regulatory architecture of transcription during the Caulobacter cell cycle.
PLoS genetics
2015; 11 (1)
Abstract
Each Caulobacter cell cycle involves differentiation and an asymmetric cell division driven by a cyclical regulatory circuit comprised of four transcription factors (TFs) and a DNA methyltransferase. Using a modified global 5' RACE protocol, we globally mapped transcription start sites (TSSs) at base-pair resolution, measured their transcription levels at multiple times in the cell cycle, and identified their transcription factor binding sites. Out of 2726 TSSs, 586 were shown to be cell cycle-regulated and we identified 529 binding sites for the cell cycle master regulators. Twenty-three percent of the cell cycle-regulated promoters were found to be under the combinatorial control of two or more of the global regulators. Previously unknown features of the core cell cycle circuit were identified, including 107 antisense TSSs which exhibit cell cycle-control, and 241 genes with multiple TSSs whose transcription levels often exhibited different cell cycle timing. Cumulatively, this study uncovered novel new layers of transcriptional regulation mediating the bacterial cell cycle.
View details for DOI 10.1371/journal.pgen.1004831
View details for PubMedID 25569173
View details for PubMedCentralID PMC4287350
-
Towards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach.
BMC systems biology
2015; 9: 66-?
Abstract
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 metabolic reactions. However, high-throughput in vivo measurements have special properties that are not taken into account in existing methods for estimating kinetic parameters, including significant relative errors in measurements of metabolite concentrations and reaction rates, and reactions with multiple substrates and products, which are sometimes reversible. A new method is needed to estimate kinetic parameters taking into account these factors.A new method, InVEst (In Vivo Estimation), is described for estimating reaction kinetic parameters, which addresses the specific challenges of in vivo data. InVEst uses maximum likelihood estimation based on a model where all measurements have relative errors. Simulations show that InVEst produces accurate estimates for a reversible enzymatic reaction with multiple reactants and products, that estimated parameters can be used to predict the effects of genetic variants, and that InVEst is more accurate than general least squares and graphic methods on data with relative errors. InVEst uses the bootstrap method to evaluate the accuracy of its estimates.InVEst addresses several challenges of in vivo data, which are not taken into account by existing methods. When data have relative errors, InVEst produces more accurate and robust estimates. InVEst also provides useful information about estimation accuracy using bootstrapping. It has potential applications of quantifying the effects of genetic variants, inference of the target of a mutation or drug treatment and improving flux estimation.
View details for DOI 10.1186/s12918-015-0214-7
View details for PubMedID 26437964
View details for PubMedCentralID PMC4595320
-
The Global Regulatory Architecture of Transcription during the Caulobacter Cell Cycle.
PLoS genetics
2015; 11 (1)
View details for DOI 10.1371/journal.pgen.1004831
View details for PubMedID 25569173
-
Leukemia Cell Differentiation upon Targeted Therapy Revealed By a Systems Biology Approach
AMER SOC HEMATOLOGY. 2014
View details for Web of Science ID 000349242708179
-
MYC through miR-17-92 Suppresses Specific Target Genes to Maintain Survival, Autonomous Proliferation, and a Neoplastic State.
Cancer cell
2014; 26 (2): 262-272
Abstract
The MYC oncogene regulates gene expression through multiple mechanisms, and its overexpression culminates in tumorigenesis. MYC inactivation reverses turmorigenesis through the loss of distinguishing features of cancer, including autonomous proliferation and survival. Here we report that MYC via miR-17-92 maintains a neoplastic state through the suppression of chromatin regulatory genes Sin3b, Hbp1, Suv420h1, and Btg1, as well as the apoptosis regulator Bim. The enforced expression of miR-17-92 prevents MYC suppression from inducing proliferative arrest, senescence, and apoptosis and abrogates sustained tumor regression. Knockdown of the five miR-17-92 target genes blocks senescence and apoptosis while it modestly delays proliferative arrest, thus partially recapitulating miR-17-92 function. We conclude that MYC, via miR-17-92, maintains a neoplastic state by suppressing specific target genes.
View details for DOI 10.1016/j.ccr.2014.06.014
View details for PubMedID 25117713
-
Automated identification of stratifying signatures in cellular subpopulations
PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA
2014; 111 (26): E2770-E2777
Abstract
Elucidation and examination of cellular subpopulations that display condition-specific behavior can play a critical contributory role in understanding disease mechanism, as well as provide a focal point for development of diagnostic criteria linking such a mechanism to clinical prognosis. Despite recent advancements in single-cell measurement technologies, the identification of relevant cell subsets through manual efforts remains standard practice. As new technologies such as mass cytometry increase the parameterization of single-cell measurements, the scalability and subjectivity inherent in manual analyses slows both analysis and progress. We therefore developed Citrus (cluster identification, characterization, and regression), a data-driven approach for the identification of stratifying subpopulations in multidimensional cytometry datasets. The methodology of Citrus is demonstrated through the identification of known and unexpected pathway responses in a dataset of stimulated peripheral blood mononuclear cells measured by mass cytometry. Additionally, the performance of Citrus is compared with that of existing methods through the analysis of several publicly available datasets. As the complexity of flow cytometry datasets continues to increase, methods such as Citrus will be needed to aid investigators in the performance of unbiased--and potentially more thorough--correlation-based mining and inspection of cell subsets nested within high-dimensional datasets.
View details for DOI 10.1073/pnas.1408792111
View details for Web of Science ID 000338118900020
View details for PubMedCentralID PMC4084463
-
Automated identification of stratifying signatures in cellular subpopulations.
Proceedings of the National Academy of Sciences of the United States of America
2014; 111 (26): E2770-7
Abstract
Elucidation and examination of cellular subpopulations that display condition-specific behavior can play a critical contributory role in understanding disease mechanism, as well as provide a focal point for development of diagnostic criteria linking such a mechanism to clinical prognosis. Despite recent advancements in single-cell measurement technologies, the identification of relevant cell subsets through manual efforts remains standard practice. As new technologies such as mass cytometry increase the parameterization of single-cell measurements, the scalability and subjectivity inherent in manual analyses slows both analysis and progress. We therefore developed Citrus (cluster identification, characterization, and regression), a data-driven approach for the identification of stratifying subpopulations in multidimensional cytometry datasets. The methodology of Citrus is demonstrated through the identification of known and unexpected pathway responses in a dataset of stimulated peripheral blood mononuclear cells measured by mass cytometry. Additionally, the performance of Citrus is compared with that of existing methods through the analysis of several publicly available datasets. As the complexity of flow cytometry datasets continues to increase, methods such as Citrus will be needed to aid investigators in the performance of unbiased--and potentially more thorough--correlation-based mining and inspection of cell subsets nested within high-dimensional datasets.
View details for DOI 10.1073/pnas.1408792111
View details for PubMedID 24979804
-
Mining TCGA data using Boolean implications.
PloS one
2014; 9 (7)
Abstract
Boolean implications (if-then rules) provide a conceptually simple, uniform and highly scalable way to find associations between pairs of random variables. In this paper, we propose to use Boolean implications to find relationships between variables of different data types (mutation, copy number alteration, DNA methylation and gene expression) from the glioblastoma (GBM) and ovarian serous cystadenoma (OV) data sets from The Cancer Genome Atlas (TCGA). We find hundreds of thousands of Boolean implications from these data sets. A direct comparison of the relationships found by Boolean implications and those found by commonly used methods for mining associations show that existing methods would miss relationships found by Boolean implications. Furthermore, many relationships exposed by Boolean implications reflect important aspects of cancer biology. Examples of our findings include cis relationships between copy number alteration, DNA methylation and expression of genes, a new hierarchy of mutations and recurrent copy number alterations, loss-of-heterozygosity of well-known tumor suppressors, and the hypermethylation phenotype associated with IDH1 mutations in GBM. The Boolean implication results used in the paper can be accessed at http://crookneck.stanford.edu/microarray/TCGANetworks/.
View details for DOI 10.1371/journal.pone.0102119
View details for PubMedID 25054200
View details for PubMedCentralID PMC4108374
-
Mining TCGA Data Using Boolean Implications.
PloS one
2014; 9 (7)
View details for DOI 10.1371/journal.pone.0102119
View details for PubMedID 25054200
-
Liquid chromatography/mass spectrometry methods for measuring dipeptide abundance in non-small-cell lung cancer.
Rapid communications in mass spectrometry : RCM
2013; 27 (18): 2091-2098
Abstract
Metabolomic profiling is a promising methodology of identifying candidate biomarkers for disease detection and monitoring. Although lung cancer is among the leading causes of cancer-related mortality worldwide, the lung tumor metabolome has not been fully characterized.We utilized a targeted metabolomic approach to analyze discrete groups of related metabolites. We adopted a dansyl [5-(dimethylamino)-1-naphthalene sulfonamide] derivatization with liquid chromatography/mass spectrometry (LC/MS) to analyze changes of metabolites from paired tumor and normal lung tissues. Identification of dansylated dipeptides was confirmed with synthetic standards. A systematic analysis of retention times was required to reliably identify isobaric dipeptides. We validated our findings in a separate sample cohort.We produced a database of the LC retention times and MS/MS spectra of 361 dansyl dipeptides. Interpretation of the spectra is presented. Using this standard data, we identified a total of 279 dipeptides in lung tumor tissue. The abundance of 90 dipeptides was selectively increased in lung tumor tissue compared to normal tissue. In a second set of validation tissues, 12 dipeptides were selectively increased.A systematic evaluation of certain metabolite classes in lung tumors may identify promising disease-specific metabolites. Our database of all possible dipeptides will facilitate ongoing translational applications of metabolomic profiling as it relates to lung cancer. Copyright © 2013 John Wiley & Sons, Ltd.
View details for DOI 10.1002/rcm.6656
View details for PubMedID 23943330
-
Identification of drug targets by chemogenomic and metabolomic profiling in yeast
PHARMACOGENETICS AND GENOMICS
2012; 22 (12): 877-886
Abstract
To advance our understanding of disease biology, the characterization of the molecular target for clinically proven or new drugs is very important. Because of its simplicity and the availability of strains with individual deletions in all of its genes, chemogenomic profiling in yeast has been used to identify drug targets. As measurement of drug-induced changes in cellular metabolites can yield considerable information about the effects of a drug, we investigated whether combining chemogenomic and metabolomic profiling in yeast could improve the characterization of drug targets.We used chemogenomic and metabolomic profiling in yeast to characterize the target for five drugs acting on two biologically important pathways. A novel computational method that uses a curated metabolic network was also developed, and it was used to identify the genes that are likely to be responsible for the metabolomic differences found.The combination of metabolomic and chemogenomic profiling, along with data analyses carried out using a novel computational method, could robustly identify the enzymes targeted by five drugs. Moreover, this novel computational method has the potential to identify genes that are causative of metabolomic differences or drug targets.
View details for DOI 10.1097/FPC.0b013e32835aa888
View details for Web of Science ID 000311031800006
View details for PubMedID 23076370
-
Computational genetic discoveries that could improve perioperative medicine
CURRENT OPINION IN ANESTHESIOLOGY
2012; 25 (4): 428-433
Abstract
The review examines the rationale and translational utility of computational genetic studies using murine models of biomedical traits.Computational genetic mapping studies have identified the genetic basis for biomedical trait differences in 16 different murine models, including several that are of importance to perioperative medicine.The results have generated new treatments for alleviating incisional pain and narcotic drug withdrawal symptoms, which are now in clinical trials. A recent study identified allelic differences affecting chronic pain responses in mice and humans, which may enable a new 'personalized' approach to treating chronic pain.
View details for DOI 10.1097/ACO.0b013e32835561f9
View details for PubMedID 22647490
-
Gene Expression Commons: An Open Platform for Absolute Gene Expression Profiling
PLOS ONE
2012; 7 (7)
Abstract
Gene expression profiling using microarrays has been limited to comparisons of gene expression between small numbers of samples within individual experiments. However, the unknown and variable sensitivities of each probeset have rendered the absolute expression of any given gene nearly impossible to estimate. We have overcome this limitation by using a very large number (>10,000) of varied microarray data as a common reference, so that statistical attributes of each probeset, such as the dynamic range and threshold between low and high expression, can be reliably discovered through meta-analysis. This strategy is implemented in a web-based platform named "Gene Expression Commons" (https://gexc.stanford.edu/) which contains data of 39 distinct highly purified mouse hematopoietic stem/progenitor/differentiated cell populations covering almost the entire hematopoietic system. Since the Gene Expression Commons is designed as an open platform, investigators can explore the expression level of any gene, search by expression patterns of interest, submit their own microarray data, and design their own working models representing biological relationship among samples.
View details for DOI 10.1371/journal.pone.0040321
View details for Web of Science ID 000306548900020
View details for PubMedID 22815738
View details for PubMedCentralID PMC3399844
-
Cd14 SNPs regulate the innate immune response
MOLECULAR IMMUNOLOGY
2012; 51 (2): 112-127
Abstract
CD14 is a monocytic differentiation antigen that regulates innate immune responses to pathogens. Here, we show that murine Cd14 SNPs regulate the length of Cd14 mRNA and CD14 protein translation efficiency, and consequently the basal level of soluble CD14 (sCD14) and type I IFN production by murine macrophages. This has substantial downstream consequences for the innate immune response; the level of expression of at least 40 IFN-responsive murine genes was altered by this mechanism. We also observed that there was substantial variation in the length of human CD14 mRNAs and in their translation efficiency. sCD14 increased cytokine production by human dendritic cells (DCs), and sCD14-primed DCs augmented human CD4T cell proliferation. These findings may provide a mechanism for exploring the complex relationship between CD14 SNPs, serum sCD14 levels, and susceptibility to human infectious and allergic diseases.
View details for DOI 10.1016/j.molimm.2012.02.112
View details for Web of Science ID 000304687500002
View details for PubMedID 22445606
View details for PubMedCentralID PMC3341513
-
A better prognosis for genetic association studies in mice
TRENDS IN GENETICS
2012; 28 (2): 62-69
Abstract
Although inbred mouse strains have been the premier model organism used in biomedical research, multiple studies and analyses have indicated that genome-wide association studies (GWAS) cannot be productively performed using inbred mouse strains. However, there is one type of GWAS in mice that has successfully identified the genetic basis for many biomedical traits of interest: haplotype-based computational genetic mapping (HBCGM). Here, we describe how the methodological basis for a HBCGM study significantly differs from that of a conventional murine GWAS, and how an integrative analysis of its output within the context of other 'omic' information can enable genetic discovery. Consideration of these factors will substantially improve the prognosis for the utility of murine genetic association studies for biomedical discovery.
View details for DOI 10.1016/j.tig.2011.10.006
View details for Web of Science ID 000300532200002
View details for PubMedID 22118772
View details for PubMedCentralID PMC3268904
- Cd14 SNPs regulate the innate immune response Molecular Immunology 2012; 2 (51): 112–127
- Computational genetic discoveries that could improve perioperative medicine Current Opinion in Anesthesiology 2012
- Gene Expression Commons: an open platform for absolute gene expression profiliing PLoS One 2012; 7
- A better prognosis for genetic association studies in mice Trends in Genetics 2012; 2 (28): 62–69
- Identification of drug targets by chemogenomic and metabolomic profiling in yeast. Pharmacogenetic Genomics 2012
-
Next-Generation Computational Genetic Analysis: Multiple Complement Alleles Control Survival after Candida albicans Infection
INFECTION AND IMMUNITY
2011; 79 (11): 4472-4479
Abstract
Candida albicans is a fungal pathogen that causes severe disseminated infections that can be lethal in immunocompromised patients. Genetic factors are known to alter the initial susceptibility to and severity of C. albicans infection. We developed a next-generation computational genetic mapping program with advanced features to identify genetic factors affecting survival in a murine genetic model of hematogenous C. albicans infection. This computational tool was used to analyze the median survival data after inbred mouse strains were infected with C. albicans, which provides a useful experimental model for identification of host susceptibility factors. The computational analysis indicated that genetic variation within early classical complement pathway components (C1q, C1r, and C1s) could affect survival. Consistent with the computational results, serum C1 binding to this pathogen was strongly affected by C1rs alleles, as was survival of chromosome substitution strains. These results led to a combinatorial, conditional genetic model, involving an interaction between C5 and C1r/s alleles, which accurately predicted survival after infection. Beyond applicability to infectious disease, this information could increase our understanding of the genetic factors affecting susceptibility to autoimmune and neurodegenerative diseases.
View details for DOI 10.1128/IAI.05666-11
View details for Web of Science ID 000296352400018
View details for PubMedID 21875959
View details for PubMedCentralID PMC3257944
-
Are Cells Asynchronous Circuits? (Invited Talk)
12th International Conference on Verification, Model Checking, and Abstract Interpretation
SPRINGER-VERLAG BERLIN. 2011: 1–1
View details for Web of Science ID 000297039800001
- Next-generation computational genetic analysis: Multiple complement alleles control survival after candida albicans infection Infection and Immunity 2011; 11 (79): 4472–4479
-
The Role of Interleukin-1 in Wound Biology. Part II: In Vivo and Human Translational Studies
ANESTHESIA AND ANALGESIA
2010; 111 (6): 1534-1542
Abstract
In the accompanying paper, we demonstrate that genetic variation within Nalp1 could contribute to interstrain differences in wound chemokine production through altering the amount of interleukin (IL)-1 produced. We further investigate the role of IL-1 in incisional wound biology and its effect on wound chemokine production in vivo and whether this mechanism could be active in human subjects.A well-characterized murine model of incisional wounding was used to assess the in vivo role of IL-1 in wound biology. The amount of 7 different cytokines/chemokines produced within an experimentally induced skin incision on a mouse paw and the nociceptive response was analyzed in mice treated with an IL-1 inhibitor. We also investigated whether human IL-1β or IL-1α stimulated the production of chemokines by primary human keratinocytes in vitro, and whether there was a correlation between IL-1β and chemokine levels in 2 experimental human wound paradigms.Administration of an IL-1 receptor antagonist to mice decreased the nociceptive response to an incisional wound, and reduced the production of multiple inflammatory mediators, including keratinocyte-derived chemokine (KC) and macrophage inhibitory protein (MIP)-1α, within the wounds. IL-1α and IL-1β stimulated IL-8 and GRO-α (human homologues of murine keratinocyte-derived chemokine) production by primary human keratinocytes in vitro. IL-1β levels were highly correlated with IL-8 in human surgical wounds, and at cutaneous sites of human ultraviolet B-induced sunburn injury.IL-1 plays a major role in regulating inflammatory mediator production in wounds through a novel mechanism; by stimulating the production of multiple cytokines and chemokines, it impacts clinically important aspects of wound biology. These data suggest that administration of an IL-1 receptor antagonist within the perioperative period could decrease postsurgical wound pain.
View details for DOI 10.1213/ANE.0b013e3181f691eb
View details for PubMedID 20889944
-
The Role of Interleukin-1 in Wound Biology. Part I: Murine In Silico and In Vitro Experimental Analysis
ANESTHESIA AND ANALGESIA
2010; 111 (6): 1525-1533
Abstract
Wound healing is a multistep, complex process that involves the coordinated action of multiple cell types. Conflicting results have been obtained when conventional methods have been used to study wound biology. Therefore, we analyzed the wound response in a mouse genetic model.We analyzed inflammatory mediators produced within incisional wounds induced in 16 inbred mouse strains. Computational haplotype-based genetic analysis of inter-strain differences in the level of production of 2 chemokines in wounds was performed. An in vitro experimental analysis system was developed to investigate whether interleukin (IL)-1 could affect chemokine production by 2 different types of cells that are present within wounds.The level of 2 chemokines, keratinocyte-derived chemokine (KC) and macrophage inflammatory protein 1α, exhibited very large (75- and 463-fold, respectively) interstrain differences within wound tissue across this inbred strain panel. Genetic variation within Nalp1, an inflammasome component that regulates IL-1 production, correlated with the interstrain differences in KC and macrophage inhibitory protein 1α production. Consistent with the genetic correlation, IL-1β was shown to stimulate KC production by murine keratinocyte and fibroblast cell lines in vitro.Genetic variation within Nalp1 could contribute to interstrain differences in wound chemokine production by altering the amount of IL-1 produced.
View details for DOI 10.1213/ANE.0b013e3181f5ef5a
View details for PubMedID 20889942
-
Towards Program Optimization through Automated Analysis of Numerical Precision.
Proceedings of the ... CGO : International Symposium on Code Generation and Optimization. International Symposium on Code Generation and Optimization
2010; 2010: 230-237
Abstract
Reducing the arithmetic precision of a computation has real performance implications, including increased speed, decreased power consumption, and a smaller memory footprint. For some architectures, e.g., GPUs, there can be such a large performance difference that using reduced precision is effectively a requirement. The tradeoff is that the accuracy of the computation will be compromised. In this paper we describe a proof assistant and associated static analysis techniques for efficiently bounding numerical and precision-related errors. The programmer/compiler can use these bounds to numerically verify and optimize an application for different input and machine configurations. We present several case study applications that demonstrate the effectiveness of these techniques and the performance benefits that can be achieved with rigorous precision analysis.
View details for DOI 10.1145/1772954.1772987
View details for PubMedID 28804690
View details for PubMedCentralID PMC5552069
-
MiDReG: A method of mining developmentally regulated genes using Boolean implications
PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA
2010; 107 (13): 5732-5737
Abstract
We present a method termed mining developmentally regulated genes (MiDReG) to predict genes whose expression is either activated or repressed as precursor cells differentiate. MiDReG does not require gene expression data from intermediate stages of development. MiDReG is based on the gene expression patterns between the initial and terminal stages of the differentiation pathway, coupled with "if-then" rules (Boolean implications) mined from large-scale microarray databases. MiDReG uses two gene expression-based seed conditions that mark the initial and the terminal stages of a given differentiation pathway and combines the statistically inferred Boolean implications from these seed conditions to identify the relevant genes. The method was validated by applying it to B-cell development. The algorithm predicted 62 genes that are expressed after the KIT+ progenitor cell stage and remain expressed through CD19+ and AICDA+ germinal center B cells. qRT-PCR of 14 of these genes on sorted B-cell progenitors confirmed that the expression of 10 genes is indeed stably established during B-cell differentiation. Review of the published literature of knockout mice revealed that of the predicted genes, 63.4% have defects in B-cell differentiation and function and 22% have a role in the B cell according to other experiments, and the remaining 14.6% are not characterized. Therefore, our method identified novel gene candidates for future examination of their role in B-cell development. These data demonstrate the power of MiDReG in predicting functionally important intermediate genes in a given developmental pathway that is defined by a mutually exclusive gene expression pattern.
View details for DOI 10.1073/pnas.0913635107
View details for PubMedID 20231483
-
Timing Robustness in the Budding and Fission Yeast Cell Cycles
PLOS ONE
2010; 5 (2)
Abstract
Robustness of biological models has emerged as an important principle in systems biology. Many past analyses of Boolean models update all pending changes in signals simultaneously (i.e., synchronously), making it impossible to consider robustness to variations in timing that result from noise and different environmental conditions. We checked previously published mathematical models of the cell cycles of budding and fission yeast for robustness to timing variations by constructing Boolean models and analyzing them using model-checking software for the property of speed independence. Surprisingly, the models are nearly, but not totally, speed-independent. In some cases, examination of timing problems discovered in the analysis exposes apparent inaccuracies in the model. Biologically justified revisions to the model eliminate the timing problems. Furthermore, in silico random mutations in the regulatory interactions of a speed-independent Boolean model are shown to be unlikely to preserve speed independence, even in models that are otherwise functional, providing evidence for selection pressure to maintain timing robustness. Multiple cell cycle models exhibit strong robustness to timing variation, apparently due to evolutionary pressure. Thus, timing robustness can be a basis for generating testable hypotheses and can focus attention on aspects of a model that may need refinement.
View details for DOI 10.1371/journal.pone.0008906
View details for Web of Science ID 000274209700002
View details for PubMedID 20126540
View details for PubMedCentralID PMC2813865
- The role of interleukin-1 in wound biology. part i: murine in silico and in vitro experimental analysis Anesthesia & Analgesia 2010; 6 (111): 1525–1533
- Timing robustness in the budding and fission yeast cell cycles PLoS ONE 2010; 2 (5): e8906
- The role of interleukin-1 in wound biology. part ii: in vivo and human translational studies Anesthesia & nalgesia 2010; 6 (111): 1534–1542
- Gene expression changes induced by genistein in the prostate cancer cell line lncap Open Prostate Cancer J 2010; 3: 86–98
-
Ly6d marks the earliest stage of B-cell specification and identifies the branchpoint between B-cell and T-cell development
GENES & DEVELOPMENT
2009; 23 (20): 2376-2381
Abstract
Common lymphoid progenitors (CLPs) clonally produce both B- and T-cell lineages, but have little myeloid potential in vivo. However, some studies claim that the upstream lymphoid-primed multipotent progenitor (LMPP) is the thymic seeding population, and suggest that CLPs are primarily B-cell-restricted. To identify surface proteins that distinguish functional CLPs from B-cell progenitors, we used a new computational method of Mining Developmentally Regulated Genes (MiDReG). We identified Ly6d, which divides CLPs into two distinct populations: one that retains full in vivo lymphoid potential and produces more thymocytes at early timepoints than LMPP, and another that behaves essentially as a B-cell progenitor.
View details for DOI 10.1101/gad.1836009
View details for PubMedID 19833765
-
Identification of the branchopoint between B and T cell development through MiDReG
AMER ASSOC IMMUNOLOGISTS. 2009
View details for Web of Science ID 000209763603052
-
Temporal Changes in Gene Expression Induced by Sulforaphane in Human Prostate Cancer Cells
PROSTATE
2009; 69 (2): 181-190
Abstract
Prostate cancer is thought to arise as a result of oxidative stresses and induction of antioxidant electrophile defense (phase 2) enzymes has been proposed as a prostate cancer prevention strategy. The isothiocyanate sulforaphane, derived from cruciferous vegetables like broccoli, potently induces surrogate markers of phase 2 enzyme activity in prostate cells in vitro and in vivo. To better understand the temporal effects of sulforaphane and broccoli sprouts on gene expression in prostate cells, we carried out comprehensive transcriptome analysis using cDNA microarrays.Transcripts significantly modulated by sulforaphane over time were identified using StepMiner analysis. Ingenuity Pathway Analysis (IPA) was used to identify biological pathways, networks, and functions significantly altered by sulforaphane treatment.StepMiner and IPA revealed significant changes in many transcripts associated with cell growth and cell cycle, as well as a significant number associated with cellular response to oxidative damage and stress. Comparison to an existing dataset suggested that sulforaphane blocked cell growth by inducing G2/M arrest. Cell growth assays and flow cytometry analysis confirmed that sulforaphane inhibited cell growth and induced cell cycle arrest.Our data suggest that in prostate cells sulforaphane primarily induces cellular defenses and inhibits cell growth by causing G2/M phase arrest. Furthermore, based on the striking similarities in the gene expression patterns induced across experiments in these cells, sulforaphane appears to be the primary bioactive compound present in broccoli sprouts, suggesting that broccoli sprouts can serve as a suitable source for sulforaphane in intervention trials.
View details for DOI 10.1002/pros.20869
View details for Web of Science ID 000262701200008
View details for PubMedID 18973173
View details for PubMedCentralID PMC2612096
- Temporal changes in gene expression induced by sulforaphane in human prostate cancer cells The Prostate 2009; 2 (69): 181–90
- Ly6d marks the earliest stage of b-cell specification and identifies the branchpoint between b-cell and t-cell development Genes and Development 2009; 20 (23): 2376–2381
-
EXE: Automatically Generating Inputs of Death
13th ACM Conference on Computer and Communications Security
ASSOC COMPUTING MACHINERY. 2008
View details for DOI 10.1145/1455518.1455522
View details for Web of Science ID 000263100000004
-
Point/Counterpoint The U. S. Should Ban Paperless Electronic Voting Machines
COMMUNICATIONS OF THE ACM
2008; 51 (10): 29-30
View details for DOI 10.1145/1400181.1400192
View details for Web of Science ID 000259930000019
-
Architecture and inherent robustness of a bacterial cell-cycle control system
PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA
2008; 105 (32): 11340-11345
Abstract
A closed-loop control system drives progression of the coupled stalked and swarmer cell cycles of the bacterium Caulobacter crescentus in a near-mechanical step-like fashion. The cell-cycle control has a cyclical genetic circuit composed of four regulatory proteins with tight coupling to processive chromosome replication and cell division subsystems. We report a hybrid simulation of the coupled cell-cycle control system, including asymmetric cell division and responses to external starvation signals, that replicates mRNA and protein concentration patterns and is consistent with observed mutant phenotypes. An asynchronous sequential digital circuit model equivalent to the validated simulation model was created. Formal model-checking analysis of the digital circuit showed that the cell-cycle control is robust to intrinsic stochastic variations in reaction rates and nutrient supply, and that it reliably stops and restarts to accommodate nutrient starvation. Model checking also showed that mechanisms involving methylation-state changes in regulatory promoter regions during DNA replication increase the robustness of the cell-cycle control. The hybrid cell-cycle simulation implementation is inherently extensible and provides a promising approach for development of whole-cell behavioral models that can replicate the observed functionality of the cell and its responses to changing environmental conditions.
View details for DOI 10.1073/pnas.0805258105
View details for Web of Science ID 000258560700056
View details for PubMedID 18685108
View details for PubMedCentralID PMC2516238
-
Genomic and proteomic analysis reveals a threshold level of MYC required for tumor maintenance
CANCER RESEARCH
2008; 68 (13): 5132-5142
Abstract
MYC overexpression has been implicated in the pathogenesis of most types of human cancers. MYC is likely to contribute to tumorigenesis by its effects on global gene expression. Previously, we have shown that the loss of MYC overexpression is sufficient to reverse tumorigenesis. Here, we show that there is a precise threshold level of MYC expression required for maintaining the tumor phenotype, whereupon there is a switch from a gene expression program of proliferation to a state of proliferative arrest and apoptosis. Oligonucleotide microarray analysis and quantitative PCR were used to identify changes in expression in 3,921 genes, of which 2,348 were down-regulated and 1,573 were up-regulated. Critical changes in gene expression occurred at or near the MYC threshold, including genes implicated in the regulation of the G(1)-S and G(2)-M cell cycle checkpoints and death receptor/apoptosis signaling. Using two-dimensional protein analysis followed by mass spectrometry, phospho-flow fluorescence-activated cell sorting, and antibody arrays, we also identified changes at the protein level that contributed to MYC-dependent tumor regression. Proteins involved in mRNA translation decreased below threshold levels of MYC. Thus, at the MYC threshold, there is a loss of its ability to maintain tumorigenesis, with associated shifts in gene and protein expression that reestablish cell cycle checkpoints, halt protein translation, and promote apoptosis.
View details for DOI 10.1158/0008-5472.CAN-07-6192
View details for PubMedID 18593912
-
Combined Analysis of Murine and Human Microarrays and ChIP Analysis Reveals Genes Associated with the Ability of MYC To Maintain Tumorigenesis
PLOS GENETICS
2008; 4 (6)
Abstract
The MYC oncogene has been implicated in the regulation of up to thousands of genes involved in many cellular programs including proliferation, growth, differentiation, self-renewal, and apoptosis. MYC is thought to induce cancer through an exaggerated effect on these physiologic programs. Which of these genes are responsible for the ability of MYC to initiate and/or maintain tumorigenesis is not clear. Previously, we have shown that upon brief MYC inactivation, some tumors undergo sustained regression. Here we demonstrate that upon MYC inactivation there are global permanent changes in gene expression detected by microarray analysis. By applying StepMiner analysis, we identified genes whose expression most strongly correlated with the ability of MYC to induce a neoplastic state. Notably, genes were identified that exhibited permanent changes in mRNA expression upon MYC inactivation. Importantly, permanent changes in gene expression could be shown by chromatin immunoprecipitation (ChIP) to be associated with permanent changes in the ability of MYC to bind to the promoter regions. Our list of candidate genes associated with tumor maintenance was further refined by comparing our analysis with other published results to generate a gene signature associated with MYC-induced tumorigenesis in mice. To validate the role of gene signatures associated with MYC in human tumorigenesis, we examined the expression of human homologs in 273 published human lymphoma microarray datasets in Affymetrix U133A format. One large functional group of these genes included the ribosomal structural proteins. In addition, we identified a group of genes involved in a diverse array of cellular functions including: BZW2, H2AFY, SFRS3, NAP1L1, NOLA2, UBE2D2, CCNG1, LIFR, FABP3, and EDG1. Hence, through our analysis of gene expression in murine tumor models and human lymphomas, we have identified a novel gene signature correlated with the ability of MYC to maintain tumorigenesis.
View details for DOI 10.1371/journal.pgen.1000090
View details for Web of Science ID 000260410300026
View details for PubMedID 18535662
View details for PubMedCentralID PMC2390767
-
Boolean implication networks derived from large scale, whole genome microarray datasets
GENOME BIOLOGY
2008; 9 (10)
Abstract
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, and fruit flies finds millions of implication relationships between genes that would be missed by other methods. These relationships capture gender differences, tissue differences, development, and differentiation. New relationships are discovered that are preserved across all three species.
View details for PubMedID 18973690
- Boolean implication networks derived from large scale, whole genome microarray datasets Genome Biology 2008; 10 (9): R157
- Architecture and inherent robustness of a bacterial cell-cycle control system Proceedings of the National Academy of Sciences 2008; 32 (105): 11340–11345
- EXE: automatically generating inputs of death. ACM Transactions on Information and System Security 2008; 2 (12)
- Combined analysis of murine and human microarrays and chip analysis reveals genes associated with the ability of myc to maintain tumorigenesis. PLoS Genetics 2008; 6 (4)
- Genomic and proteomic analysis reveals a threshold level of myc required for tumor maintenance Cancer Research 2008; 13 (68): 5132
-
Automatic Formal Verification of Block Cipher Implementations
8th International Conference on Formal Methods in Computer-Aided Design
IEEE. 2008: 45–51
View details for Web of Science ID 000265244800006
-
A retrospective on Mur phi
Symposium on 25 Years of Model Checking (25MC)
SPRINGER-VERLAG BERLIN. 2008: 77–88
View details for Web of Science ID 000257623600005
-
Extracting binary signals from microarray time-course data
NUCLEIC ACIDS RESEARCH
2007; 35 (11): 3705-3712
Abstract
This article presents a new method for analyzing microarray time courses by identifying genes that undergo abrupt transitions in expression level, and the time at which the transitions occur. The algorithm matches the sequence of expression levels for each gene against temporal patterns having one or two transitions between two expression levels. The algorithm reports a P-value for the matching pattern of each gene, and a global false discovery rate can also be computed. After matching, genes can be sorted by the direction and time of transitions. Genes can be partitioned into sets based on the direction and time of change for further analysis, such as comparison with Gene Ontology annotations or binding site motifs. The method is evaluated on simulated and actual time-course data. On microarray data for budding yeast, it is shown that the groups of genes that change in similar ways and at similar times have significant and relevant Gene Ontology annotations.
View details for DOI 10.1093/nar/gkm284
View details for PubMedID 17517782
-
The Pathalyzer: A tool for analysis of signal transduction pathways
Joint Annual Workshop on Systems Biology and on Regulatory Genomics
SPRINGER-VERLAG BERLIN. 2007: 11–22
View details for Web of Science ID 000244806900002
- A retrospective on murφ In 25 years of Model Checking, volume 4925 of Lecture Notes in Computer Science 2007: 1
- Extracting boolean signals from microarray time course data. Nucleic Acids Research 2007; 11 (35): 3705–3712
-
A decision procedure for bit-vectors and arrays
19th International Conference on Computer Aided Verification
SPRINGER-VERLAG BERLIN. 2007: 519–531
View details for Web of Science ID 000248222700049
- Multiple representations of biological processes. Transactions on Computational Systems Biology 2006: 221–245
-
Multiple representations of biological processes
4th International Conference on Computational Methods in Systems Biology
SPRINGER-VERLAG BERLIN. 2006: 221–245
View details for Web of Science ID 000244723500010
-
A refinement method for validity checking of quantified first-order formulas in hardware verification
6th International Conference on Formal Methods in Computer Aided Design
IEEE COMPUTER SOC. 2006: 145–152
View details for Web of Science ID 000243594800019
-
A Practical Approach to Partial Functions in CVC Lite
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
2005; 125 (3): 13–23
View details for DOI 10.1016/j.entcs.2004.06.064
View details for Web of Science ID 000214005200003
- The pathway logic assistant 2005
- Evaluation of voting systems. Commun. ACM 2004; 11 (47): 144
-
A partitioning methodology for BDD-based verification
5th International Conference on Formal Methods in Computer-Aided Design (FMCAD)
SPRINGER-VERLAG BERLIN. 2004: 399–413
View details for Web of Science ID 000225877900028
- A practical approach to partial functions in CVC Lite. 2004
- A partitioning methodology for bdd-based verification 2004
- Guest editors' introduction: E-voting security. IEEE Security and Privacy 2004; 1 (2)
- A proof-producing boolean search engine. 2003
-
Using formal specifications for functional validation of hardware designs
IEEE DESIGN & TEST OF COMPUTERS
2002; 19 (4): 96-106
View details for Web of Science ID 000176582000014
-
Efficient algorithms for approximate time separation of events
SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES
2002; 27: 129-162
View details for Web of Science ID 000177265700002
-
Formal verification of out-of-order execution with incremental flushing
FORMAL METHODS IN SYSTEM DESIGN
2002; 20 (2): 139-158
View details for Web of Science ID 000173803400002
-
Counter-example based predicate discovery in predicate abstraction
4th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2002)
SPRINGER-VERLAG BERLIN. 2002: 19–32
View details for Web of Science ID 000182825700002
- CVC: a Cooperating Validity Checker. 2002
- Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. edited by Brinksma, E., Larsen, K. G. 2002
- Using formal specifications for functional validation of hardware designs IEEE Design & Test of Computers 2002; 4 (19): 96–106
-
Deriving a simulation input generator and a coverage metric from a formal specification
39th Design Automation Conference
ASSOC COMPUTING MACHINERY. 2002: 801–806
View details for Web of Science ID 000177213300141
-
Deciding Presburger arithmetic by model checking and comparisons with other methods
4th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2002)
SPRINGER-VERLAG BERLIN. 2002: 171–186
View details for Web of Science ID 000182825700011
-
Parallelizing the Mur phi verifier
9th International Conference on Computer-Aided Verification (CAV 97)
SPRINGER. 2001: 117–29
View details for Web of Science ID 000167827700003
-
A decision procedure for an extensional theory of arrays
16th Annual IEEE Symposium on Logic in Computer Science
IEEE COMPUTER SOC. 2001: 29–37
View details for Web of Science ID 000170688700004
-
Successive approximation of abstract transition relations
16th Annual IEEE Symposium on Logic in Computer Science
IEEE COMPUTER SOC. 2001: 51–58
View details for Web of Science ID 000170688700006
-
A simple method for extracting models from protocol code
28th Annual International Symposium on Computer Architecture
IEEE COMPUTER SOC. 2001: 192–203
View details for Web of Science ID 000170768200017
-
Automatic checking of aggregation abstractions through state enumeration
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
2000; 19 (10): 1202-1210
View details for Web of Science ID 000089953200010
-
Counterexample-guided choice of projections in approximate symbolic model checking
IEEE/ACM International Conference on Computer Aided Design (ICCAD-2000)
IEEE. 2000: 115–119
View details for Web of Science ID 000166023200020
-
Reliable verification using symbolic simulation with scalar values
37th Annual Design Automation Conference (DAC)
ASSOC COMPUTING MACHINERY. 2000: 124–129
View details for Web of Science ID 000166739300025
-
Java model checking
15th IEEE International Conference on Automated Software Engineering (ASE 2000)
IEEE COMPUTER SOC. 2000: 253–256
View details for Web of Science ID 000089913800027
-
Symbolic simulation with approximate values
3rd International Conference on Formal Methods in Computer-Aided Design
SPRINGER-VERLAG BERLIN. 2000: 470–485
View details for Web of Science ID 000174608800028
-
A framework for cooperating decision procedures
17th International Conference on Automated Deduction (CADE-17)
SPRINGER-VERLAG BERLIN. 2000: 79–98
View details for Web of Science ID 000166717300006
-
Monitor-based formal specification of PCI
3rd International Conference on Formal Methods in Computer-Aided Design
SPRINGER-VERLAG BERLIN. 2000: 335–353
View details for Web of Science ID 000174608800020
-
Timing analysis of asynchronous systems using time separation of events
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
1999; 18 (8): 1061-1076
View details for Web of Science ID 000081585500001
-
Verifying systems with replicated components in Mur phi
FORMAL METHODS IN SYSTEM DESIGN
1999; 14 (3): 273-310
View details for Web of Science ID 000080735800004
-
Min-max timing analysis and an application to asynchronous circuits
PROCEEDINGS OF THE IEEE
1999; 87 (2): 332-346
View details for Web of Science ID 000078216900011
-
An executable specification and verifier for relaxed memory order
IEEE TRANSACTIONS ON COMPUTERS
1999; 48 (2): 227-235
View details for Web of Science ID 000079060200015
-
Automatic synthesis of extended burst-mode circuits: Part II (automatic synthesis)
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
1999; 18 (2): 118-132
View details for Web of Science ID 000078407000003
-
Automatic synthesis of extended burst-mode circuits: Part I (specification and hazard-free implementations)
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
1999; 18 (2): 101-117
View details for Web of Science ID 000078407000002
- Verifying systems with replicated components in Murφ. Formal Methods in System Design 1999; 3 (14): 41–75
- Experience with predicate abstraction. 1999
- Automatic synthesis of extended burst-mode circuits: Part I (specification and hazard-free implementations). IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 1999; 2 (18): 101–117
- Improved approximate reachability using auxiliary state variables. 1999
- Automatic synthesis of extended burst-mode circuits: Part II (specification and hazard-free implementations). IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 1999; 2 (18): 118–132
- An executable specification, analyzer and verifier for RMO (relaxed memory order). IEEE Transactions on Computers 1999; 2 (48): 227–335
- Timing analysis of asynchronous systems using time separation of events. IEEE Transactions on Computer-Aided Design 1999; 8 (18): 1061–1076
-
BDD-based synthesis of extended burst-mode controllers
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
1998; 17 (9): 782-792
View details for Web of Science ID 000076096100004
-
Verification of cache coherence protocols by aggregation of distributed transactions
8th Annual ACM Symposium on Parallel Algorithms and Architectures
SPRINGER. 1998: 355–76
View details for Web of Science ID 000074349800003
-
What's between simulation and formal verification? (Extended abstract)
35th Design Automation Conference
ASSOC COMPUTING MACHINERY. 1998: 328–329
View details for Web of Science ID 000077273700058
- Reducing manual abstraction in formal verification of out-of-order execution. edited by Gopalakrishnan, G., Windley, P. 1998
- Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems 1998; 4 (31): 355–376
- Bdd-based synthesis of extended burst-mode controllers. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 1998; 9 (17): 782–792
- Formally verifying data and control with weak reachability invariants. edited by Gopalakrishnan, G., Windley, P. 1998
- Checking properties of safety critical specifications using efficient decision procedures. 1998
-
Verification by approximate forward and backward reachability
IEEE/ACM International Conference on Computer-Aided Design
ASSOC COMPUTING MACHINERY. 1998: 366–370
View details for Web of Science ID 000077729800056
-
Static analysis to identify invariants in RSML specifications
5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 98)
SPRINGER-VERLAG BERLIN. 1998: 133–142
View details for Web of Science ID 000082522000013
-
Approximate reachability with BDDs using overlapping projections
35th Design Automation Conference
ASSOC COMPUTING MACHINERY. 1998: 451–456
View details for Web of Science ID 000077273700081
-
Validation with guided search of the state space
35th Design Automation Conference
ASSOC COMPUTING MACHINERY. 1998: 599–604
View details for Web of Science ID 000077273700108
-
Using magnetic disk instead of main memory in the Mur phi verifier
10th International Conference on Computer-Aided Verification (CAV 98)
SPRINGER-VERLAG BERLIN. 1998: 172–183
View details for Web of Science ID 000083172700018
-
A decision procedure for bit-vector arithmetic
35th Design Automation Conference
ASSOC COMPUTING MACHINERY. 1998: 522–527
View details for Web of Science ID 000077273700094
-
Format verification of out-of-order execution using incremental flushing
10th International Conference on Computer-Aided Verification (CAV 98)
SPRINGER-VERLAG BERLIN. 1998: 98–109
View details for Web of Science ID 000083172700012
-
Practical timing analysis of asynchronous circuits using time separation of events
IEEE Custom Integrated Circuits Conference
IEEE. 1998: 455–458
View details for Web of Science ID 000075218500094
-
Timing analysis for extended burst-mode circuits
3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems
I E E E, COMPUTER SOC PRESS. 1997: 101–111
View details for Web of Science ID A1997BH63Q00010
-
More accurate polynomial-time min-max timing simulation
3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems
I E E E, COMPUTER SOC PRESS. 1997: 112–123
View details for Web of Science ID A1997BH63Q00011
-
Parallelizing the Mur phi verifier
9th International Conference on Computer-Aided Verification (CAV 97)
SPRINGER-VERLAG BERLIN. 1997: 256–267
View details for Web of Science ID 000075410600026
-
Approximate algorithms for time separation of events
1997 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 97)
I E E E, COMPUTER SOC PRESS. 1997: 190–194
View details for Web of Science ID A1997BK01U00030
-
Better verification through symmetry
FORMAL METHODS IN SYSTEM DESIGN
1996; 9 (1-2): 41-75
View details for Web of Science ID A1996VE93600003
-
Automatic generation of invariants in processor verification
1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 96)
SPRINGER-VERLAG BERLIN. 1996: 377–388
View details for Web of Science ID 000073935500027
- Verification of flash cache coherence protocol by aggregation of distributed actions. 1996
- Combining state space caching and hash compaction. In Methoden des Entwurfs und der Verifikation digitaler Systeme, 4. GI/ITG/GME Workshop 1996
- Formal methods: state of the art and future directions. ACM Computing Surveys 1996; 4 (28): 626–43
- Protocol verification by aggregation of distributed transactions. 1996
- A new scheme for memory-efficient probabilistic verification. 1996
- Automata-theoretic verification of real-time systems. Formal Methods for Real-time Computing, number 5 in Trends in Software edited by Heitmeyer, C., Mandrioli, D. 1996: 55–81
- Protocol verification by aggregation of distributed actions. 1996
-
State reduction using reversible rules
33rd Design Automation Conference
ASSOC COMPUTING MACHINERY. 1996: 564–567
View details for Web of Science ID A1996BF92A00112
- The murφ verification system. 1996
- Combining state space caching and hash compaction. 1996
- Better verification through symmetry. Formal Methods in System Design 1996; 1–2 (9): 41–75
-
Validity checking for combinations of theories with equality
1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 96)
SPRINGER-VERLAG BERLIN. 1996: 187–201
View details for Web of Science ID 000073935500013
-
Self-consistency checking
1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 96)
SPRINGER-VERLAG BERLIN. 1996: 159–171
View details for Web of Science ID 000073935500011
-
EXACT 2-LEVEL MINIMIZATION OF HAZARD-FREE LOGIC WITH MULTIPLE-INPUT CHANGES
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
1995; 14 (8): 986-997
View details for Web of Science ID A1995RL43500007
-
Verification of real-time systems by successive over and under approximation
7th Conference on Computer Aided Verification (CAV 95)
SPRINGER-VERLAG BERLIN. 1995: 409–422
View details for Web of Science ID A1995BF02S00032
-
A high-performance asynchronous SCSI controller
International Conference on Computer Design - VLSI in Computers and Processors (ICCD 95)
IEEE COMPUTER SOC. 1995: 44–49
View details for Web of Science ID A1995BE54G00007
- Exact two-level minimization of hazard-free logic with multiple-input changes. IEEE Transactions on Computer-Aided Design of Integrated Circuits 1995; 8 (14): 986–997
- A high-performance asynchronous SCSI controller. 1995
-
Improved probabilistic verification by hash compaction
IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 95)
SPRINGER-VERLAG BERLIN. 1995: 206–224
View details for Web of Science ID A1995BF24P00013
-
Automatic verification of the SCI cache coherence protocol
IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 95)
SPRINGER-VERLAG BERLIN. 1995: 21–34
View details for Web of Science ID A1995BF24P00002
-
Architecture validation for processors
22nd Annual International Symposium on Computer Architecture
ASSOC COMPUTING MACHINERY. 1995: 404–413
View details for Web of Science ID A1995BE13F00036
- A theory of timed automata. Theoretical Computer Science 1995; 126: 183–235
-
Efficient validity checking for processor verification
1995 IEEE/ACM International Conference on Computer-Aided Design
I E E E, COMPUTER SOC PRESS. 1995: 2–6
View details for Web of Science ID A1995BE64G00001
-
A THEORY OF TIMED AUTOMATA
THEORETICAL COMPUTER SCIENCE
1994; 126 (2): 183-235
View details for Web of Science ID A1994NH36400002
-
SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
1994; 13 (4): 401-424
View details for Web of Science ID A1994NC80000001
-
SELF-TIMED LOGIC USING CURRENT-SENSING COMPLETION DETECTION (CSCD)
JOURNAL OF VLSI SIGNAL PROCESSING
1994; 7 (1-2): 7-16
View details for Web of Science ID A1994NA69100002
-
NEW TECHNIQUES FOR EFFICIENT VERIFICATION WITH IMPLICITLY CONJOINED BDDS
31st Design Automation Conference
ASSOC COMPUTING MACHINERY. 1994: 276–282
View details for Web of Science ID A1994BC03E00046
-
PERFORMANCE-DRIVEN SYNTHESIS OF ASYNCHRONOUS CONTROLLERS
1994 IEEE/ACM International Conference on Computer-Aided Design
IEEE COMPUTER SOC. 1994: 550–557
View details for Web of Science ID A1994BC25F00088
- Conference on Computer-Aided Veri cation, of Lecture Notes in Computer Science edited by Dill, D. L. 1994
- Performance-driven synthesis of asynchronous controllers. 1994
- Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits 1994; 4 (13): 401–424
- Automatic verification of pipelined microprocessor control. edited by Dill, D. L. 1994
- Self-timed logic using current sensing completion detection (CSCD). Journal of VLSI Signal Processing 1994; 1–2 (7): 7–16
-
THE DESIGN OF A HIGH-PERFORMANCE CACHE CONTROLLER - A CASE-STUDY IN ASYNCHRONOUS SYNTHESIS
INTEGRATION-THE VLSI JOURNAL
1993; 15 (3): 241-262
View details for Web of Science ID A1993MK62900002
-
MODEL-CHECKING IN DENSE REAL-TIME
INFORMATION AND COMPUTATION
1993; 104 (1): 2-34
View details for Web of Science ID A1993LD49200001
-
FORMAL SPECIFICATION OF ABSTRACT MEMORY MODELS
Symposium on Research on Integrated Systems
M I T PRESS. 1993: 38–52
View details for Web of Science ID A1993BA02Q00003
-
EFFICIENT VERIFICATION OF SYMMETRICAL CONCURRENT SYSTEMS
1993 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN : VLSI IN COMPUTERS AND PROCESSES
I E E E, COMPUTER SOC PRESS. 1993: 230–234
View details for Web of Science ID A1993BZ24U00041
- Efficient verification of bdds using implicitly conjoined invariants. 1993
- Higher-level specification and verification with BDDs. 1993
- Automatic technology mapping for generalized fundamental-mode asynchronous designs 1993
- Automatic technology mapping for generalized fundamental-mode asynchronous designs. Technical Report CSL-TR-93-580, Stanford University Computer Systems Laboratory 1993
- Practical generalizations of asynchronous state machines. 1993
- The design of a high-performance cache controller: a case study in asynchronous synthesis. Integration: the VLSI Journal 1993; 3 (15): 241–262
-
UNIFYING SYNCHRONOUS ASYNCHRONOUS STATE MACHINE SYNTHESIS
1993 IEEE/ACM International Conference on Computer-Aided Design
I E E E, COMPUTER SOC PRESS. 1993: 255–260
View details for Web of Science ID A1993BA39Z00044
-
AUTOMATIC TECHNOLOGY MAPPING FOR GENERALIZED FUNDAMENTAL-MODE ASYNCHRONOUS DESIGNS
30TH DESIGN AUTOMATION CONF
ASSOC COMPUTING MACHINERY. 1993: 61–67
View details for Web of Science ID A1993BY90U00011
- Model-Checking for Real-Time Systems. Information and Computation 1993; 1 (104): 2–34
- Reducing BDD size by exploiting functional dependencies. 1993
- Efficient verification of symmetric concurrent systems. 1993
-
BETTER VERIFICATION THROUGH SYMMETRY
IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications (CHDL 93)
ELSEVIER SCIENCE BV. 1993: 97–111
View details for Web of Science ID A1993BZ97A00008
-
MODELING HIERARCHICAL COMBINATIONAL-CIRCUITS
1993 IEEE/ACM International Conference on Computer-Aided Design
I E E E, COMPUTER SOC PRESS. 1993: 612–617
View details for Web of Science ID A1993BA39Z00101
-
SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND
5TH SYMP ON LOGIC IN COMPUTER SCIENCE
ACADEMIC PRESS INC JNL-COMP SUBSCRIPTIONS. 1992: 142–70
View details for Web of Science ID A1992JA06100002
- Verification with real-time COSPAN. 1992
-
ALGORITHMS FOR INTERFACE TIMING VERIFICATION
1992 IEEE INTERNATIONAL CONF ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS ( ICCD 92 )
I E E E, COMPUTER SOC PRESS. 1992: 48–51
View details for Web of Science ID A1992BY76C00009
-
MINIMIZATION OF TIMED TRANSITION-SYSTEMS
3RD INTERNATIONAL CONF ON CONCURRENCY THEORY
SPRINGER-VERLAG BERLIN. 1992: 340–354
View details for Web of Science ID A1992BY27A00025
-
CHECKING FOR LANGUAGE INCLUSION USING SIMULATION PREORDERS
3RD INTERNATIONAL WORKSHOP ON COMPUTER AIDED VERIFICATION ( CAV 91 )
SPRINGER-VERLAG BERLIN. 1992: 255–265
View details for Web of Science ID A1992BX63T00026
-
SYNTHESIS OF 3D ASYNCHRONOUS STATE MACHINES
1992 IEEE INTERNATIONAL CONF ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS ( ICCD 92 )
I E E E, COMPUTER SOC PRESS. 1992: 346–350
View details for Web of Science ID A1992BY76C00068
-
PRACTICAL ASYNCHRONOUS CONTROLLER-DESIGN
1992 IEEE INTERNATIONAL CONF ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS ( ICCD 92 )
I E E E, COMPUTER SOC PRESS. 1992: 341–345
View details for Web of Science ID A1992BY76C00067
-
AN IMPLEMENTATION OF 3 ALGORITHMS FOR TIMING VERIFICATION BASED ON AUTOMATA EMPTINESS
CONF ON REAL-TIME SYSTEMS SYMP
I E E E, COMPUTER SOC PRESS. 1992: 157–166
View details for Web of Science ID A1992BY08D00015
- Synthesis of 3D asynchronous state machines. 1992
- Protocol verification as a hardware design aid. 1992
- Practical asynchronous controller design. 1992
- Algorithms for interface timing verification. 1992
- Specification and automatic verification of self-timed queues Formal Methods in Systems Design 1992; 1 (1): 29–62
- Automatic synthesis of 3D asynchronous state machines. 1992
- The theory of timed automata. In Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science REX Workshop, Mook, The Netherlands. 1992: 45–73
- Practical generalizations of asynchronous state machines. Technical Report CSL-TR-92-544, Computer Systems Laboratory, Stanford University 1992
- Formal Verification of Cache Systems using Refinement Relations. Formal Methods in Systems Design 1992; 4 (1): 355–383
- An Implementation of Three Algorithms for Timing Veri cation Based on Automata Emptiness. 1992
- Verifying automata specifications of probabilistic real-time systems. In Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science REX Workshop, Mook, The Netherlands. 1992: 28–44
- Symbolic model checking: 1020 states and beyond. Information and Computation 1992; 2 (98): 142–170
-
VERIFYING AUTOMATA SPECIFICATIONS OF PROBABILISTIC REAL-TIME SYSTEMS
REX WORKSHOP ON REAL-TIME : THEORY IN PRACTICE
SPRINGER VERLAG. 1992: 28–44
View details for Web of Science ID A1992LE88200003
-
THE THEORY OF TIMED AUTOMATA
REX WORKSHOP ON REAL-TIME : THEORY IN PRACTICE
SPRINGER VERLAG. 1992: 45–73
View details for Web of Science ID A1992LE88200004
-
MINIMIZATION OF TIMED TRANSITION-SYSTEMS
LECTURE NOTES IN COMPUTER SCIENCE
1992; 630: 340-354
View details for Web of Science ID A1992LF69300025
-
CHECKING FOR LANGUAGE INCLUSION USING SIMULATION PREORDERS
LECTURE NOTES IN COMPUTER SCIENCE
1992; 575: 255-265
View details for Web of Science ID A1992KQ18500026
-
SELF-TIMED LOGIC USING CURRENT-SENSING COMPLETION DETECTION (CSCD)
INTERNATIONAL CONF ON COMPUTER DESIGN : VLSI IN COMPUTERS AND PROCESSORS
I E E E, COMPUTER SOC PRESS. 1991: 187–191
View details for Web of Science ID A1991BU43M00037
-
MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
18TH INTERNATIONAL COLLOQUIUM ON AUTOMATA, LANGUAGES AND PROGRAMMING ( ICALP 91 )
SPRINGER-VERLAG BERLIN. 1991: 115–126
View details for Web of Science ID A1991BT82D00008
-
SYNTHESIS OF ASYNCHRONOUS STATE MACHINES USING A LOCAL CLOCK
INTERNATIONAL CONF ON COMPUTER DESIGN : VLSI IN COMPUTERS AND PROCESSORS
I E E E, COMPUTER SOC PRESS. 1991: 192–197
View details for Web of Science ID A1991BU43M00038
- Synthesis of asynchronous state machines using a local clock. 1991
- Efficient self-timing with level-encoded two-phase dual rail (LEDR). 1991
- Automatic synthesis of locally-clocked asynchronous state machines. 1991
-
SYNTHESIZING PROCESSES AND SCHEDULERS FROM TEMPORAL SPECIFICATIONS
2ND INTERNATIONAL CONF ON COMPUTER-AIDED VERIFICATION ( CAV 90 )
SPRINGER. 1991: 272–281
View details for Web of Science ID A1991LE71400029
-
MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
LECTURE NOTES IN COMPUTER SCIENCE
1991; 510: 115-126
View details for Web of Science ID A1991GA06500008
-
COMPLETE TRACE STRUCTURES
WORKSHOP ON HARDWARE SPECIFICATION, VERIFICATION AND SYNTHESIS : MATHEMATICAL ASPECTS
SPRINGER-VERLAG BERLIN. 1990: 224–243
View details for Web of Science ID A1990BQ26K00012
-
COMPLETE TRACE STRUCTURES
LECTURE NOTES IN COMPUTER SCIENCE
1990; 408: 224-243
View details for Web of Science ID A1990CU37400012
-
AUTOMATA FOR MODELING REAL-TIME SYSTEMS
17TH INTERNATIONAL COLLOQUIUM ON AUTOMATA, LANGUAGES AND PROGRAMMING ( ICALP 90 )
SPRINGER-VERLAG. 1990: 322–335
View details for Web of Science ID A1990BR56W00026
-
TIMING ASSUMPTIONS AND VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS
LECTURE NOTES IN COMPUTER SCIENCE
1990; 407: 197-212
View details for Web of Science ID A1990CU37800017
- Symbolic model checking: 10 states and beyond. 1990
- Sequential circuit verification using symbolic model-checking. 1990
- Specification and automatic verification of self-timed queues Formal Veri cation of Hardware Design edited by Yoeli, M. IEEE Computer Society Press. 1990: 225–248
- Model-checking for real-time systems. 1990
- Automatic verification of sequential circuits using temporal logic Formal Verification of Hardware Design. edited by Yoeli, M. IEEE Computer Society Press. 1990: 166–175
- Automatic verification Synchronization Design for Digital Systems edited by Meng, T. H. Kluwer Academic Publishers. 1990: 147–172
- Automatic verification of asynchronous circuits using temporal logic. Formal Verification of Hardware Design, Reprint of a paper in IEE proceedings, Pt. E. edited by Yoeli, M. IEEE Computer Society Press. 1990: 176–183
-
TIMING ASSUMPTIONS AND VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS
INTERNATIONAL WORKSHOP ON AUTOMATIC VERIFICATION METHODS FOR FINITE STATE SYSTEMS
SPRINGER-VERLAG BERLIN. 1990: 197–212
View details for Web of Science ID A1990BQ26L00017
-
AUTOMATA FOR MODELING REAL-TIME SYSTEMS
LECTURE NOTES IN COMPUTER SCIENCE
1990; 443: 322-335
View details for Web of Science ID A1990DX76000026
- Trace Theory for Automatic Hierarchical Veri cation of Speed-independent Circuits edited by Dill, D. L. MIT Press. 1989
-
AUTOMATIC VERIFICATION OF SPEED-INDEPENDENT CIRCUITS WITH PETRI NET SPECIFICATIONS
1989 IEEE INTERNATIONAL CONF ON COMPUTER DESIGN : VLSI IN COMPUTERS AND PROCESSORS
I E E E. 1989: 212–216
View details for Web of Science ID A1989BP71U00041
-
PRACTICALITY OF STATE-MACHINE VERIFICATION OF SPEED-INDEPENDENT CIRCUITS
1989 IEEE INTERNATIONAL CONF ON COMPUTER-AIDED DESIGN : A CONF FOR THE EE CAD PROFESSIONAL ( ICCAD-89 )
I E E E, COMPUTER SOC PRESS. 1989: 266–269
View details for Web of Science ID A1989BP87R00059
- Practicality of state-machine verification of speed-independent circuits. 1989
- Automatic verification of speed-independent circuits with Petri net specifications. 1989
- Specification and automatic verification of self-timed queues. Technical Report CSL-TR-89-387, Computer Systems Laboratory, Stanford University, This was reprinted in the IEEE tutorial: Formal Verification of Hardware Design, by Michael Yoeli 1989
- Complete trace structures In Hardware Speci cation, Veri cation and Synthesis: Mathematical Aspects, volume 408 of Lecture Notes in Computer Science 1989: 224–243
- Trace theory for automatic hierarchical verification of speed-independent circuits. 1988
-
AUTOMATIC VERIFICATION OF SEQUENTIAL-CIRCUITS USING TEMPORAL LOGIC
IEEE TRANSACTIONS ON COMPUTERS
1986; 35 (12): 1035-1044
View details for Web of Science ID A1986E848200003
-
AUTOMATIC VERIFICATION OF ASYNCHRONOUS CIRCUITS USING TEMPORAL LOGIC
IEE PROCEEDINGS-E COMPUTERS AND DIGITAL TECHNIQUES
1986; 133 (5): 276-282
View details for Web of Science ID A1986E282200005
- Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, This was reprinted in the IEEE tutorial: Formal Veri cation of Hardware Design, by Michael Yoeli 1986; 12 (C-35): 1035–1044
- Automatic circuit verification using temporal logic: Two new examples. 1986
- Automatic verification of asynchronous circuits using temporal logic 1986
- Automatic verification of asynchronous circuits using temporal logic. Technical Report CMU-CS-85-125, Department of Computer Science, Carnegie-Mellon University 1985
- Automatic verification of sequential circuits using temporal logic. 1985
- Checking the correctness of sequential circuits. 1985
- Automatic verification of asynchronous circuits using temporal logic. 1985
- Automatic verification of sequential circuits using temporal logic. Technical Report CMU-CS-85-100, Department of Computer Science, Carnegie-Mellon University 1984