Bio

Bio


Dill has interests in computational systems biology as well as the theory and application of formal verification techniques to system designs, which encompass hardware, protocols, and software. He has also done research in asynchronous circuit verification and synthesis, and in verification methods for hard real-time systems.

Academic Appointments


Honors & Awards


  • Fellow, American Academy of Arts and Sciences (2013)
  • Member, National Academy of Engineering (2013)
  • Fellow, ACM
  • Fellow, IEEE
  • Pioneer Award, Electronic Frontier Foundation

Professional Education


  • PhD, Carnegie Mellon (1987)

Research & Scholarship

Current Research and Scholarly Interests


Computational methods for understanding regulatory circuits in cell biology

Teaching

2014-15 Courses


Graduate and Fellowship Programs


  • Biomedical Informatics (Phd Program)

Publications

Journal Articles


  • The role of abcb5 alleles in susceptibility to haloperidol-induced toxicity in mice and humans. PLoS medicine Zheng, M., Zhang, H., Dill, D. L., Clark, J. D., Tu, S., Yablonovitch, A. L., Tan, M. H., Zhang, R., Rujescu, D., Wu, M., Tessarollo, L., Vieira, W., Gottesman, M. M., Deng, S., Eberlin, L. S., Zare, R. N., Billard, J., Gillet, J., Li, J. B., Peltz, G. 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

  • Mutant WT1 is associated with DNA hypermethylation of PRC2 targets in AML and responds to EZH2 inhibition. Blood Sinha, S., Thomas, D., Yu, L., Gentles, A. J., Jung, N., Corces-Zimmerman, M. R., Chan, S. M., Reinisch, A., Feinberg, A. P., Dill, D. L., Majeti, R. 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 Zhou, B., Schrader, J. M., Kalogeraki, V. S., Abeliuk, E., Dinh, C. B., Pham, J. Q., Cui, Z. Z., Dill, D. L., McAdams, H. H., Shapiro, L. 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

  • MYC through miR-17-92 Suppresses Specific Target Genes to Maintain Survival, Autonomous Proliferation, and a Neoplastic State. Cancer cell Li, Y., Choi, P. S., Casey, S. C., Dill, D. L., Felsher, D. W. 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 Bruggner, R. V., Bodenmiller, B., Dill, D. L., Tibshirani, R. J., Nolan, G. P. 2014; 111 (26): E2770-E2777
  • Mining TCGA Data Using Boolean Implications. PloS one Sinha, S., Tsang, E. K., Zeng, H., Meister, M., Dill, D. L. 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

  • Liquid chromatography/mass spectrometry methods for measuring dipeptide abundance in non-small-cell lung cancer RAPID COMMUNICATIONS IN MASS SPECTROMETRY Wu, M., Xu, Y., Fitch, W. L., Zheng, M., Merritt, R. E., Shrager, J. B., Zhang, W., Dill, D. L., Peltz, G., Hoang, C. D. 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 Web of Science ID 000323048600006

  • Identification of drug targets by chemogenomic and metabolomic profiling in yeast PHARMACOGENETICS AND GENOMICS Wu, M., Zheng, M., Zhang, W., Suresh, S., Schlecht, U., Fitch, W. L., Aronova, S., Baumann, S., Davis, R., St Onge, R., Dill, D. L., Peltz, G. 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 Zheng, M., Dill, D., Clark, J. D., Peltz, G. 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 Web of Science ID 000306273900005

    View details for PubMedID 22647490

  • Gene Expression Commons: An Open Platform for Absolute Gene Expression Profiling PLOS ONE Seita, J., Sahoo, D., Rossi, D. J., Bhattacharya, D., Serwold, T., Inlay, M. A., Ehrlich, L. I., Fathman, J. W., Dill, D. L., Weissman, I. L. 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

  • Cd14 SNPs regulate the innate immune response MOLECULAR IMMUNOLOGY Liu, H., Hu, Y., Zheng, M., Suhoski, M. M., Engleman, E. G., Dill, D. L., Hudnall, M., Wang, J., Spolski, R., Leonard, W. J., Peltz, G. 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

  • A better prognosis for genetic association studies in mice TRENDS IN GENETICS Zheng, M., Dill, D., Peltz, G. 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

  • Cd14 SNPs regulate the innate immune response Molecular Immunology Lu, H., Hu, Y., Zheng, M., Engleman, E., Dill, D., Hudnall, M. 2012; 2 (51): 112–127
  • Computational genetic discoveries that could improve perioperative medicine Current Opinion in Anesthesiology Zheng, M., Dill, D., Clark, J., Peltz, G. 2012
  • Gene Expression Commons: an open platform for absolute gene expression profiliing PLoS One Seita, J., Sahoo, D., Rossi, D., Bhattacharya, D., Serwold, T., Inlay, M., Dill, D. 2012; 7
  • A better prognosis for genetic association studies in mice Trends in Genetics Zheng, M., Dill, D., Peltz, G. 2012; 2 (28): 62–69
  • Identification of drug targets by chemogenomic and metabolomic profiling in yeast. Pharmacogenetic Genomics Wu, M., Zheng, M., Zhang, W., Suresh, S., Schlecht, U., Fitch, W. L., Dill, D. 2012
  • Next-Generation Computational Genetic Analysis: Multiple Complement Alleles Control Survival after Candida albicans Infection INFECTION AND IMMUNITY Peltz, G., Zaas, A. K., Zheng, M., Solis, N. V., Zhang, M. X., Liu, H., Hu, Y., Boxx, G. M., Phan, Q. T., Dill, D., Filler, S. G. 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

  • Are Cells Asynchronous Circuits? (Invited Talk) VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION Dill, D. L. 2011; 6538: 1-1
  • Next-generation computational genetic analysis: Multiple complement alleles control survival after candida albicans infection Infection and Immunity Peltz, G., Zaas, A., K., Zheng, M., Solis, N., V., Zhang, M., X., Liu, H., H., Dill, D. 2011; 11 (79): 4472–4479
  • The Role of Interleukin-1 in Wound Biology. Part II: In Vivo and Human Translational Studies ANESTHESIA AND ANALGESIA Hu, Y., Liang, D., Li, X., Liu, H., Zhang, X., Zheng, M., Dill, D., Shi, X., Qiao, Y., Yeomans, D., Carvalho, B., Angst, M. S., Clark, J. D., Peltz, G. 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 Web of Science ID 000284973300033

    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 Hu, Y., Liang, D., Li, X., Liu, H., Zhang, X., Zheng, M., Dill, D., Shi, X., Qiao, Y., Yeomans, D., Carvalho, B., Angst, M. S., Clark, J. D., Peltz, G. 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 Web of Science ID 000284973300032

    View details for PubMedID 20889942

  • MiDReG: A method of mining developmentally regulated genes using Boolean implications PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA Sahoo, D., Seita, J., Bhattacharya, D., Inlay, M. A., Weissman, I. L., Plevritis, S. K., Dill, D. L. 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 Web of Science ID 000276159500010

    View details for PubMedID 20231483

  • Timing Robustness in the Budding and Fission Yeast Cell Cycles PLOS ONE Mangla, K., Dill, D. L., Horowitz, M. A. 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

  • The role of interleukin-1 in wound biology. part i: murine in silico and in vitro experimental analysis Anesthesia & Analgesia Hu, Y., Liang, D., Li, X., Liu, H., Zhang, X., Zheng, M., Dill, D. 2010; 6 (111): 1525–1533
  • Timing robustness in the budding and fission yeast cell cycles PLoS ONE Mangla, K., Dill, D. L., Horowitz, M. A. 2010; 2 (5): e8906
  • The role of interleukin-1 in wound biology. part ii: in vivo and human translational studies Anesthesia & nalgesia Hu, Y., Liang, D., Li, X., Liu, H., Zhang, X., Zheng, M., Dill, D. 2010; 6 (111): 1534–1542
  • Gene expression changes induced by genistein in the prostate cancer cell line lncap Open Prostate Cancer J Bhamre, S., Sahoo, D., Tibshirani, R., Dill, D., L., Brooks, J., D 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 Inlay, M. A., Bhattacharya, D., Sahoo, D., Serwold, T., Seita, J., Karsunky, H., Plevritis, S. K., Dill, D. L., Weissman, I. L. 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 Web of Science ID 000270849700004

    View details for PubMedID 19833765

  • Temporal Changes in Gene Expression Induced by Sulforaphane in Human Prostate Cancer Cells PROSTATE Bhamre, S., Sahoo, D., Tibshirani, R., Dill, D. L., Brooks, J. D. 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

  • Temporal changes in gene expression induced by sulforaphane in human prostate cancer cells The Prostate Bhamre, S., Sahoo, D., Tibshirani, R., Dill, D., Brooks, J. 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 Inlay, Matthew, A., Bhattacharya, D., Sahoo, D., Serwold, T., Seita, J., Karsunky, H., Dill, D. 2009; 20 (23): 2376–2381
  • Point/Counterpoint The U. S. Should Ban Paperless Electronic Voting Machines COMMUNICATIONS OF THE ACM Dill, D. L. 2008; 51 (10): 29-30
  • Architecture and inherent robustness of a bacterial cell-cycle control system PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA Shen, X., Collier, J., Dill, D., Shapiro, L., Horowitz, M., McAdams, H. H. 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

  • Genomic and proteomic analysis reveals a threshold level of MYC required for tumor maintenance CANCER RESEARCH Shachaf, C. M., Gentles, A. J., Elchuri, S., Sahoo, D., Soen, Y., Sharpe, O., Perez, O. D., Chang, M., Mitchel, D., Robinson, W. H., Dill, D., Nolan, G. P., Plevritis, S. K., Felsher, D. W. 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 Web of Science ID 000257415300024

    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 Wu, C., Sahoo, D., Arvanitis, C., Bradon, N., Dill, D. L., Felsher, D. W. 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

  • Boolean implication networks derived from large scale, whole genome microarray datasets GENOME BIOLOGY Sahoo, D., Dill, D. L., Gentles, A. J., Tibshirani, R., Plevritis, S. K. 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 Web of Science ID 000260587300020

    View details for PubMedID 18973690

  • Boolean implication networks derived from large scale, whole genome microarray datasets Genome Biology Sahoo, D., Dill, D., L., Gentles, A., J., Tibshirani, R., Plevritis, S., K. 2008; 10 (9): R157
  • Architecture and inherent robustness of a bacterial cell-cycle control system Proceedings of the National Academy of Sciences Shen, X., Collier, J., Dill, D., L., Shapiro, L., Horowitz, M., McAdams, H., H. 2008; 32 (105): 11340–11345
  • EXE: automatically generating inputs of death. ACM Transactions on Information and System Security Cadar, C., Ganesh, V., Pawlowski, Peter, M., Dill, David, L., Engler, Dawson, R. 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 Wu, C., H., Sahoo, D., Arvanitis, C., Bradon, N., Dill, D., L., Felsher, D., W. 2008; 6 (4)
  • Genomic and proteomic analysis reveals a threshold level of myc required for tumor maintenance Cancer Research Shachaf, C., M., Gentles, A., J., Elchuri, S., Sahoo, D., Soen, Y., Sharpe, O., Dill, D. 2008; 13 (68): 5132
  • Automatic Formal Verification of Block Cipher Implementations 2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN Smith, E. W., Dill, D. L. 2008: 45-51
  • A retrospective on Mur phi 25 YEARS OF MODEL CHECKING: HISTORY, ACHIEVEMENTS, PERSPECTIVES Dill, D. L. 2008; 5000: 77-88
  • Extracting binary signals from microarray time-course data NUCLEIC ACIDS RESEARCH Sahoo, D., Dill, D. L., Tibshirani, R., Plevritis, S. K. 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 Web of Science ID 000247817500018

    View details for PubMedID 17517782

  • A decision procedure for bit-vectors and arrays COMPUTER AIDED VERIFICATION, PROCEEDINGS Ganesh, V., Dill, D. L. 2007; 4590: 519-531
  • Extracting boolean signals from microarray time course data. Nucleic Acids Research Sahoo, D., Dill, David, L., Tibshirani, R., Plevritis, Sylvia, K. 2007; 11 (35): 3705–3712
  • The Pathalyzer: A tool for analysis of signal transduction pathways SYSTEMS BIOLOGY AND REGULATORY GENOMICS Dill, D. L., Knapp, M. A., Gage, P., Talcott, C., Laderoute, K., Lincoln, P. 2007; 4023: 11-22
  • A refinement method for validity checking of quantified first-order formulas in hardware verification PROCEEDINGS OF FORMAL METHODS IN COMPUTER AIDED DESIGN Abu-Haimed, H., Dill, D. L., Berezin, S. 2006: 145-152
  • Multiple representations of biological processes. Transactions on Computational Systems Biology Talcott, C., Dill, David, L. 2006: 221–245
  • Multiple representations of biological processes TRANSACTIONS ON COMPUTATIONAL SYSTEMS BIOLOGY VI Talcott, C., Dill, D. L. 2006; 4220: 221-245
  • Evaluation of voting systems. Commun. ACM Vora, P., L., Adida, B., Bucholz, R., Chaum, D., Dill, D., L., Jefferson, D. 2004; 11 (47): 144
  • Guest editors' introduction: E-voting security. IEEE Security and Privacy Dill, David, L., Rubin, Aviel, D. 2004; 1 (2)
  • Using formal specifications for functional validation of hardware designs IEEE DESIGN & TEST OF COMPUTERS Shimizu, K., Dill, D. L. 2002; 19 (4): 96-106
  • Efficient algorithms for approximate time separation of events SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES Chakraborty, S., Dill, D. L., Yun, K. Y. 2002; 27: 129-162
  • Formal verification of out-of-order execution with incremental flushing FORMAL METHODS IN SYSTEM DESIGN Jones, R. B., Skakkebaek, J. U., Dill, D. L. 2002; 20 (2): 139-158
  • Deciding Presburger arithmetic by model checking and comparisons with other methods FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS Ganesh, V., Berezin, S., Dill, D. L. 2002; 2517: 171-186
  • Using formal specifications for functional validation of hardware designs IEEE Design & Test of Computers Shimizu, K., Dill, David, L. 2002; 4 (19): 96–106
  • Counter-example based predicate discovery in predicate abstraction FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS Das, S., Dill, D. L. 2002; 2517: 19-32
  • Deriving a simulation input generator and a coverage metric from a formal specification 39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002 Shimizu, K., Dill, D. L. 2002: 801-806
  • Successive approximation of abstract transition relations 16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS Das, S., Dill, D. L. 2001: 51-58
  • A decision procedure for an extensional theory of arrays 16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS Stump, A., Barrett, C. W., Dill, D. L., LEVITT, J. 2001: 29-37
  • A simple method for extracting models from protocol code 28TH ANNUAL INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE, PROCEEDINGS Lie, D., Chou, A., Engler, D., Dill, D. L. 2001: 192-203
  • Automatic checking of aggregation abstractions through state enumeration IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS Park, S., Das, S., Dill, D. L. 2000; 19 (10): 1202-1210
  • Monitor-based formal specification of PCI FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS Shimizu, K., Dill, D. L., Hu, A. J. 2000; 1954: 335-353
  • Reliable verification using symbolic simulation with scalar values 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000 Wilson, C., Dill, D. L. 2000: 124-129
  • Counterexample-guided choice of projections in approximate symbolic model checking ICCAD - 2000 : IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN Govindaraju, S. G., Dill, D. L. 2000: 115-119
  • Java model checking FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS Park, D. Y., Stern, U., Skakkebaek, J. U., Dill, D. L. 2000: 253-256
  • Symbolic simulation with approximate values FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS Wilson, C., Dill, D. L., Bryant, R. E. 2000; 1954: 470-485
  • A framework for cooperating decision procedures AUTOMATED DEDUCTION - CADE-17 Barrett, C. W., Dill, D. L., Stump, A. 2000; 1831: 79-98
  • Timing analysis of asynchronous systems using time separation of events IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS Chakraborty, S. A., Yun, K. Y., Dill, D. L. 1999; 18 (8): 1061-1076
  • Verifying systems with replicated components in Mur phi FORMAL METHODS IN SYSTEM DESIGN Ip, C. N., Dill, D. L. 1999; 14 (3): 273-310
  • 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 Yun, K. Y., Dill, D. L. 1999; 18 (2): 101-117
  • Min-max timing analysis and an application to asynchronous circuits PROCEEDINGS OF THE IEEE Chakraborty, S., Dill, D. L., Yun, K. Y. 1999; 87 (2): 332-346
  • An executable specification and verifier for relaxed memory order IEEE TRANSACTIONS ON COMPUTERS Park, S. J., Dill, D. L. 1999; 48 (2): 227-235
  • Automatic synthesis of extended burst-mode circuits: Part II (automatic synthesis) IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS Yun, K. Y., Dill, D. L. 1999; 18 (2): 118-132
  • Timing analysis of asynchronous systems using time separation of events. IEEE Transactions on Computer-Aided Design Chakraborty, S., Yun, Kenneth, Y., Dill, David, L. 1999; 8 (18): 1061–1076
  • 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 Yun, Kenneth, Y., Dill, David, L. 1999; 2 (18): 118–132
  • An executable specification, analyzer and verifier for RMO (relaxed memory order). IEEE Transactions on Computers Park, S., Dill, David, L. 1999; 2 (48): 227–335
  • 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 Yun, Kenneth, Y., Dill, David, L. 1999; 2 (18): 101–117
  • Verifying systems with replicated components in Murφ. Formal Methods in System Design Ip, C., Norris., Dill, David, L. 1999; 3 (14): 41–75
  • BDD-based synthesis of extended burst-mode controllers IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS Yun, K. Y., Lin, B., Dill, D. L., Devadas, S. 1998; 17 (9): 782-792
  • Using magnetic disk instead of main memory in the Mur phi verifier COMPUTER AIDED VERIFICATION Stern, U., Dill, D. L. 1998; 1427: 172-183
  • Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems Park, S., Dill, David, L. 1998; 4 (31): 355–376
  • Bdd-based synthesis of extended burst-mode controllers. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems Yun, Kenneth, Y., Lin, B., Dill, David, L., Devadas, S. 1998; 9 (17): 782–792
  • A decision procedure for bit-vector arithmetic 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS Barrett, C. W., Dill, D. L., LEVITT, J. R. 1998: 522-527
  • Verification by approximate forward and backward reachability 1998 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN Govindaraju, S. G., Dill, D. L. 1998: 366-370
  • Static analysis to identify invariants in RSML specifications FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS Park, D. Y., Skakkebaek, J. U., Dill, D. L. 1998; 1486: 133-142
  • Format verification of out-of-order execution using incremental flushing COMPUTER AIDED VERIFICATION Skakkebaek, J. U., Jones, R. B., Dill, D. L. 1998; 1427: 98-109
  • Practical timing analysis of asynchronous circuits using time separation of events IEEE 1998 CUSTOM INTEGRATED CIRCUITS CONFERENCE - PROCEEDINGS Chakraborty, S., Yun, K. Y., Dill, D. L. 1998: 455-458
  • Approximate reachability with BDDs using overlapping projections 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS Govindaraju, S. G., Dill, D. L., Hu, A. J., Horowitz, M. A. 1998: 451-456
  • What's between simulation and formal verification? (Extended abstract) 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS Dill, D. L. 1998: 328-329
  • Validation with guided search of the state space 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS Yang, C. H., Dill, D. L. 1998: 599-604
  • Parallelizing the Mur phi verifier COMPUTER AIDED VERIFICATION Stern, U., Dill, D. L. 1997; 1254: 256-267
  • Better verification through symmetry FORMAL METHODS IN SYSTEM DESIGN Ip, C. N., Dill, D. L. 1996; 9 (1-2): 41-75
  • State reduction using reversible rules 33RD DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 1996 Ip, C. N., Dill, D. L. 1996: 564-567
  • Formal methods: state of the art and future directions. ACM Computing Surveys Clarke, E., M., Wing, J., M., Alur, R., Cleaveland, R., Dill, D., Emerson, A. 1996; 4 (28): 626–43
  • Combining state space caching and hash compaction. In Methoden des Entwurfs und der Verifikation digitaler Systeme, 4. GI/ITG/GME Workshop Stern, U., Dill, D., L. 1996
  • Better verification through symmetry. Formal Methods in System Design Ip, C., Norris., Dill, David, L. 1996; 1–2 (9): 41–75
  • Validity checking for combinations of theories with equality FORMAL METHODS IN COMPUTER-AIDED DESIGN Barrett, C., Dill, D., LEVITT, J. 1996; 1166: 187-201
  • Self-consistency checking FORMAL METHODS IN COMPUTER-AIDED DESIGN Jones, R. B., Seger, C. J., Dill, D. L. 1996; 1166: 159-171
  • Automatic generation of invariants in processor verification FORMAL METHODS IN COMPUTER-AIDED DESIGN Su, J. X., Dill, D. L., Barrett, C. W. 1996; 1166: 377-388
  • EXACT 2-LEVEL MINIMIZATION OF HAZARD-FREE LOGIC WITH MULTIPLE-INPUT CHANGES IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS Nowick, S. M., Dill, D. L. 1995; 14 (8): 986-997
  • A high-performance asynchronous SCSI controller INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS & PROCESSORS, PROCEEDINGS Yun, K. Y., Dill, D. L. 1995: 44-49
  • Exact two-level minimization of hazard-free logic with multiple-input changes. IEEE Transactions on Computer-Aided Design of Integrated Circuits Nowick, S., M., Dill, D., L. 1995; 8 (14): 986–997
  • A theory of timed automata. Theoretical Computer Science Alur, R., Dill, D., L. 1995; 126: 183–235
  • Efficient validity checking for processor verification 1995 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN Jones, R. B., Dill, D. L., Burch, J. R. 1995: 2-6
  • Verification of real-time systems by successive over and under approximation COMPUTER AIDED VERIFICATION Dill, D. L., WONGTOI, H. 1995; 939: 409-422
  • Improved probabilistic verification by hash compaction CORRECT HARDWARE DESIGN AND VERIFICATION METHODS Stern, U., Dill, D. L. 1995; 987: 206-224
  • Automatic verification of the SCI cache coherence protocol CORRECT HARDWARE DESIGN AND VERIFICATION METHODS Stern, U., Dill, D. L. 1995; 987: 21-34
  • A THEORY OF TIMED AUTOMATA THEORETICAL COMPUTER SCIENCE Alur, R., Dill, D. L. 1994; 126 (2): 183-235
  • SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS Burch, J. R., Clarke, E. M., Long, D. E., McMillan, K. L., Dill, D. L. 1994; 13 (4): 401-424
  • SELF-TIMED LOGIC USING CURRENT-SENSING COMPLETION DETECTION (CSCD) JOURNAL OF VLSI SIGNAL PROCESSING Dean, M. E., Dill, D. L., Horowitz, M. 1994; 7 (1-2): 7-16
  • NEW TECHNIQUES FOR EFFICIENT VERIFICATION WITH IMPLICITLY CONJOINED BDDS 31ST DESIGN AUTOMATION CONFERENCE - PROCEEDINGS 1994 Hu, A. J., York, G., Dill, D. L. 1994: 276-282
  • PERFORMANCE-DRIVEN SYNTHESIS OF ASYNCHRONOUS CONTROLLERS 1994 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN - DIGEST OF TECHNICAL PAPERS Yun, K. Y., Lin, B., Dill, D. L., Devadas, S. 1994: 550-557
  • Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits Burch, Jerry, R., Clarke, Edmund, M., Long, David, E., McMillan, Kenneth, L., Dill, David, L. 1994; 4 (13): 401–424
  • Self-timed logic using current sensing completion detection (CSCD). Journal of VLSI Signal Processing Dean, M., Dill, David, L., Horowitz, M. 1994; 1–2 (7): 7–16
  • THE DESIGN OF A HIGH-PERFORMANCE CACHE CONTROLLER - A CASE-STUDY IN ASYNCHRONOUS SYNTHESIS INTEGRATION-THE VLSI JOURNAL Nowick, S. M., Dean, M. E., Dill, D. L., Horowitz, M. 1993; 15 (3): 241-262
  • MODEL-CHECKING IN DENSE REAL-TIME INFORMATION AND COMPUTATION Alur, R., Courcoubetis, C., Dill, D. 1993; 104 (1): 2-34
  • UNIFYING SYNCHRONOUS ASYNCHRONOUS STATE MACHINE SYNTHESIS 1993 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN - DIGEST OF TECHNICAL PAPERS Yun, K. Y., Dill, D. L. 1993: 255-260
  • Automatic technology mapping for generalized fundamental-mode asynchronous designs. Technical Report CSL-TR-93-580, Stanford University Computer Systems Laboratory Siegel, P., Micheli, G. D., Dill, D. 1993
  • Model-Checking for Real-Time Systems. Information and Computation Alur, R., Courcoubetis, C., Dill, D. 1993; 1 (104): 2–34
  • The design of a high-performance cache controller: a case study in asynchronous synthesis. Integration: the VLSI Journal Nowick, S., M., Dean, M., E., Dill, D., L., Horowitz, M. 1993; 3 (15): 241–262
  • EFFICIENT VERIFICATION OF SYMMETRICAL CONCURRENT SYSTEMS 1993 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS - PROCEEDINGS Ip, C. N., Dill, D. L. 1993: 230-234
  • AUTOMATIC TECHNOLOGY MAPPING FOR GENERALIZED FUNDAMENTAL-MODE ASYNCHRONOUS DESIGNS 30TH DESIGN AUTOMATION CONFERENCE : PROCEEDINGS 1993 Siegel, P., Demicheli, G., Dill, D. 1993: 61-67
  • BETTER VERIFICATION THROUGH SYMMETRY COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS Ip, C. N., Dill, D. L. 1993; 32: 97-111
  • MODELING HIERARCHICAL COMBINATIONAL-CIRCUITS 1993 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN - DIGEST OF TECHNICAL PAPERS Burch, J. R., Dill, D., Wolf, E., Demicheli, G. 1993: 612-617
  • CHECKING FOR LANGUAGE INCLUSION USING SIMULATION PREORDERS COMPUTER AIDED VERIFICATION Dill, D. L., Hu, A. J., WONGTOI, H. 1992; 575: 255-265
  • Specification and automatic verification of self-timed queues Formal Methods in Systems Design Dill, David, L., Nowick, Steven, M., Sproull, Robert, F. 1992; 1 (1): 29–62
  • PRACTICAL ASYNCHRONOUS CONTROLLER-DESIGN 1992 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS Nowick, S. M., Yun, K. Y., Dill, D. L. 1992: 341-345
  • SYNTHESIS OF 3D ASYNCHRONOUS STATE MACHINES 1992 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS Yun, K. Y., Dill, D. L., Nowick, S. M. 1992: 346-350
  • AN IMPLEMENTATION OF 3 ALGORITHMS FOR TIMING VERIFICATION BASED ON AUTOMATA EMPTINESS REAL-TIME SYSTEMS SYMPOSIUM : PROCEEDINGS Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., WONGTOI, H. 1992: 157-166
  • Practical generalizations of asynchronous state machines. Technical Report CSL-TR-92-544, Computer Systems Laboratory, Stanford University Yun, Kenneth, Y., Dill, David, L., Nowick, Steven, M. 1992
  • Formal Verification of Cache Systems using Refinement Relations. Formal Methods in Systems Design Loewenstein, P., Dill, D. 1992; 4 (1): 355–383
  • Symbolic model checking: 1020 states and beyond. Information and Computation Burch, J., R., Clarke, E., M., McMillan, K., L., Dill, D., L., Hwang, L., J. 1992; 2 (98): 142–170
  • MINIMIZATION OF TIMED TRANSITION-SYSTEMS LECTURE NOTES IN COMPUTER SCIENCE Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D., WONGTOI, H. 1992; 630: 340-354
  • SYNTHESIS OF ASYNCHRONOUS STATE MACHINES USING A LOCAL CLOCK IEEE INTERNATIONAL CONFERENCE ON COMPUTER-DESIGN : VLSI IN COMPUTERS AND PROCESSORS Nowick, S. M., Dill, D. L. 1991: 192-197
  • MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS LECTURE NOTES IN COMPUTER SCIENCE Alur, R., Courcoubetis, C., Dill, D. 1991; 510: 115-126
  • COMPLETE TRACE STRUCTURES LECTURE NOTES IN COMPUTER SCIENCE Dill, D. L. 1990; 408: 224-243
  • TIMING ASSUMPTIONS AND VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS LECTURE NOTES IN COMPUTER SCIENCE Dill, D. L. 1990; 407: 197-212
  • AUTOMATA FOR MODELING REAL-TIME SYSTEMS AUTOMATA, LANGUAGES AND PROGRAMMING / Alur, R., Dill, D. 1990; 443: 322-335
  • PRACTICALITY OF STATE-MACHINE VERIFICATION OF SPEED-INDEPENDENT CIRCUITS 1989 IEEE INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN Nowick, S. M., Dill, D. L. 1989: 266-269
  • AUTOMATIC VERIFICATION OF SPEED-INDEPENDENT CIRCUITS WITH PETRI NET SPECIFICATIONS PROCEEDINGS - IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN : VLSI IN COMPUTERS & PROCESSORS Dill, D. L., Nowick, S. M., SPROULL, R. F. 1989: 212-216
  • 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 Dill, David, L., Nowick, Steven, M., Sproull, Robert, F. 1989
  • AUTOMATIC VERIFICATION OF SEQUENTIAL-CIRCUITS USING TEMPORAL LOGIC IEEE TRANSACTIONS ON COMPUTERS Browne, M. C., Clarke, E. M., Dill, D. L., Mishra, B. 1986; 35 (12): 1035-1044
  • AUTOMATIC VERIFICATION OF ASYNCHRONOUS CIRCUITS USING TEMPORAL LOGIC IEE PROCEEDINGS-E COMPUTERS AND DIGITAL TECHNIQUES Dill, D. L., Clarke, E. M. 1986; 133 (5): 276-282
  • 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 Browne, Michael, C., Clarke, Edmund, M., Dill, David, L., Mishra, B. 1986; 12 (C-35): 1035–1044
  • Automatic verification of asynchronous circuits using temporal logic. Technical Report CMU-CS-85-125, Department of Computer Science, Carnegie-Mellon University Dill, David, L., Clarke, Edmund, M. 1985
  • Automatic verification of sequential circuits using temporal logic. Technical Report CMU-CS-85-100, Department of Computer Science, Carnegie-Mellon University Browne, Michael, C., Clarke, Edmund, M., Dill, David, L., Mishra, B. 1984

Books and Book Chapters


  • A retrospective on murφ In 25 years of Model Checking, volume 4925 of Lecture Notes in Computer Science Dill, David, L. 2007: 1
  • Automata-theoretic verification of real-time systems. Formal Methods for Real-time Computing, number 5 in Trends in Software Alur, R., Dill, David, L. edited by Heitmeyer, C., Mandrioli, D. 1996: 55–81
  • Conference on Computer-Aided Veri cation, of Lecture Notes in Computer Science edited by Dill, D. L. 1994
  • The theory of timed automata. In Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science Alur, R., Dill, David, L. REX Workshop, Mook, The Netherlands. 1992: 45–73
  • Verifying automata specifications of probabilistic real-time systems. In Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science Alur, R., Courcoubetis, C., Dill, David, L. REX Workshop, Mook, The Netherlands. 1992: 28–44
  • Automatic verification of sequential circuits using temporal logic Formal Verification of Hardware Design. Browne, M. C., Clarke, E. M., Dill, D. L., Mishra, B. edited by Yoeli, M. IEEE Computer Society Press. 1990: 166–175
  • Specification and automatic verification of self-timed queues Formal Veri cation of Hardware Design Dill, D. L., Nowick, S. M., Sproull, R. F. edited by Yoeli, M. IEEE Computer Society Press. 1990: 225–248
  • Automatic verification Synchronization Design for Digital Systems Nowick, S. M., Dill, D. L. 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. Dill, David, L., Clarke, Edmund, M. edited by Yoeli, M. IEEE Computer Society Press. 1990: 176–183
  • Complete trace structures In Hardware Speci cation, Veri cation and Synthesis: Mathematical Aspects, volume 408 of Lecture Notes in Computer Science Dill, D. L. 1989: 224–243
  • Trace Theory for Automatic Hierarchical Veri cation of Speed-independent Circuits edited by Dill, D. L. MIT Press. 1989

Conference Proceedings


  • EXE: Automatically Generating Inputs of Death Cadar, C., Ganesh, V., Pawlowski, P. M., Dill, D. L., Engler, D. R. ASSOC COMPUTING MACHINERY. 2008
  • The pathway logic assistant Talcott, C., Dill, David, L. 2005
  • A practical approach to partial functions in CVC Lite. Barrett, C., Berezin, S., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, David, L. 2004
  • A partitioning methodology for bdd-based verification Sahoo, D., Iyer, Subramanian, K., Jain, J., Stangier, C., Narayan, A., Dill, David, L. 2004
  • A proof-producing boolean search engine. Barrett, C., Berezin, S., Dill, David, L. 2003
  • CVC: a Cooperating Validity Checker. Stump, A., Barrett, C., Dill, D. 2002
  • Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. Barrett, Clark, W., Dill, David, L., Stump, A. edited by Brinksma, E., Larsen, K. G. 2002
  • Parallelizing the Mur phi verifier Stern, U., Dill, D. L. SPRINGER. 2001: 117-129
  • Improved approximate reachability using auxiliary state variables. Govindaraju, Shankar, G., Dill, David, L., Bergmann, Jules, P. 1999
  • Experience with predicate abstraction. Das, S., Dill, David, L., Park, S. 1999
  • Verification of cache coherence protocols by aggregation of distributed transactions Park, S., Dill, D. L. SPRINGER. 1998: 355-376
  • Formally verifying data and control with weak reachability invariants. Su, Jeffrey, X., Dill, David, L., Skakkebæk, Jens, U. edited by Gopalakrishnan, G., Windley, P. 1998
  • Checking properties of safety critical specifications using efficient decision procedures. Park, David, Y.W., Skakkebæk, Jens, U., Heimdahl, Mats, P.E., Czerny, Barbara, J., Dill, David, L. 1998
  • Reducing manual abstraction in formal verification of out-of-order execution. Jones, Robert, B., Skakkebæk, Jens, U., Dill, David, L. edited by Gopalakrishnan, G., Windley, P. 1998
  • Timing analysis for extended burst-mode circuits Chakraborty, S., Dill, D. L., Yun, K. Y., Chang, K. Y. I E E E, COMPUTER SOC PRESS. 1997: 101-111
  • Approximate algorithms for time separation of events Chakraborty, S., Dill, D. L. I E E E, COMPUTER SOC PRESS. 1997: 190-194
  • More accurate polynomial-time min-max timing simulation Chakraborty, S., Dill, D. L. I E E E, COMPUTER SOC PRESS. 1997: 112-123
  • Protocol verification by aggregation of distributed actions. Park, S., Dill, David, L. 1996
  • Combining state space caching and hash compaction. Stern, U., Dill, David, L. 1996
  • Verification of flash cache coherence protocol by aggregation of distributed actions. Park, S., Dill, David, L. 1996
  • The murφ verification system. Dill, David, L. 1996
  • Protocol verification by aggregation of distributed transactions. Park, S., Dill, David, L. 1996
  • A new scheme for memory-efficient probabilistic verification. Stern, U., Dill, David, L. 1996
  • Architecture validation for processors Ho, R. C., Yang, C. H., Horowitz, M. A., Dill, D. L. ASSOC COMPUTING MACHINERY. 1995: 404-413
  • A high-performance asynchronous SCSI controller. Yun, Kenneth, Y., Dill, David, L. 1995
  • Automatic verification of pipelined microprocessor control. Burch, Jerry, R., Dill, David, L. edited by Dill, D. L. 1994
  • Performance-driven synthesis of asynchronous controllers. Yun, K., Y., Lin, B., Dill, D, L., Devadas, S. 1994
  • Automatic technology mapping for generalized fundamental-mode asynchronous designs Siegel, P., Micheli, G. D., Dill, D. 1993
  • Practical generalizations of asynchronous state machines. Yun, Kenneth, Y., Dill, David, L., Nowick, Steven, M. 1993
  • Reducing BDD size by exploiting functional dependencies. Hu, Alan, J., Dill, David, L. 1993
  • Efficient verification of symmetric concurrent systems. Ip, C. N., Dill, David, L. 1993
  • Higher-level specification and verification with BDDs. Hu, Alan, J., Dill, David, L., Drexler, Andreas, J., Yang, C., Han 1993
  • Efficient verification of bdds using implicitly conjoined invariants. Hu, Alan, J., Dill, David, L. 1993
  • FORMAL SPECIFICATION OF ABSTRACT MEMORY MODELS Dill, D. L., Park, S., Nowatzyk, A. G. M I T PRESS. 1993: 38-52
  • SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., Hwang, L. J. ACADEMIC PRESS INC JNL-COMP SUBSCRIPTIONS. 1992: 142-170
  • Algorithms for interface timing verification. McMillan, K., Dill, David, L. 1992
  • Verification with real-time COSPAN. Courcoubetis, C., Dill, D., Chatzaki, M., Tzounakis, P. 1992
  • An Implementation of Three Algorithms for Timing Veri cation Based on Automata Emptiness. Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H. 1992
  • Synthesis of 3D asynchronous state machines. Yun, Kenneth, Y., Dill, David, L. 1992
  • Protocol verification as a hardware design aid. Dill, David, L., Drexler, Andreas, J., Hu, Alan, J., Yang, C., Han 1992
  • Practical asynchronous controller design. Nowick, Steven, M., Yun, K., Dill, David, L. 1992
  • Automatic synthesis of 3D asynchronous state machines. Yun, Kenneth, Y., Dill, David, L. 1992
  • VERIFYING AUTOMATA SPECIFICATIONS OF PROBABILISTIC REAL-TIME SYSTEMS Alur, R., Courcoubetis, C., Dill, D. SPRINGER VERLAG. 1992: 28-44
  • THE THEORY OF TIMED AUTOMATA Alur, R., Dill, D. SPRINGER VERLAG. 1992: 45-73
  • SYNTHESIZING PROCESSES AND SCHEDULERS FROM TEMPORAL SPECIFICATIONS WONGTOI, H., Dill, D. L. SPRINGER. 1991: 272-281
  • SELF-TIMED LOGIC USING CURRENT-SENSING COMPLETION DETECTION (CSCD) Dean, M. E., Dill, D. L., Horowitz, M. I E E E, COMPUTER SOC PRESS. 1991: 187-191
  • Synthesis of asynchronous state machines using a local clock. Nowick, Steven, M., Dill, David, L. 1991
  • Efficient self-timing with level-encoded two-phase dual rail (LEDR). Dean, Mark, E., Williams, Ted, E., Dill, David, L. 1991
  • Automatic synthesis of locally-clocked asynchronous state machines. Nowick, Steven, M., Dill, David, L. 1991
  • Symbolic model checking: 10 states and beyond. Burch, J., R., Clarke, E., M., McMillan, K., L., Dill, D., L., Hwang, J. 1990
  • Sequential circuit verification using symbolic model-checking. Burch, J., R., Clarke, E., M., Dill, D., L., McMillan, K., L. 1990
  • Model-checking for real-time systems. Alur, R., Courcoubetis, C., Dill, D. 1990
  • Practicality of state-machine verification of speed-independent circuits. Nowick, Steven, M., Dill, David, L. 1989
  • Automatic verification of speed-independent circuits with Petri net specifications. Dill, David, L., Nowick, Steven, M., Sproull, Robert, F. 1989
  • Trace theory for automatic hierarchical verification of speed-independent circuits. Dill, David, L. 1988
  • Automatic verification of asynchronous circuits using temporal logic Dill, David, L., Clark, Edmund, M. 1986
  • Automatic circuit verification using temporal logic: Two new examples. Browne, Michael, C., Clarke, Edmund, M., Dill, David, L. 1986
  • Automatic verification of asynchronous circuits using temporal logic. Dill, David, L., Clarke, Edmund, M. 1985
  • Checking the correctness of sequential circuits. Browne, Michael, C., Clarke, Edmund, M., Dill, David, L. 1985
  • Automatic verification of sequential circuits using temporal logic. Browne, Michael, C., Clarke, Edmund, M., Dill, David, L., Mishra, B. 1985

Stanford Medicine Resources: