skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Prototyping Formal Methods Tools: A Protocol Analysis Case Study
Modern-day formal methods tools are more than just a core solver: they also need convenient languages, useful editors, usable visualizations, and often also scriptability. These are required to attract a community of users, to put ideas to work in practice, and to conduct evaluations of the formalisms and core technical ideas. Off-the-shelf solvers address one of these issues but not the others. How can full prototype environments be obtained quickly? We have built Forge, a system for prototyping such environments. In this paper, we present a case-study to assess the utility of Forge. Concretely, we use Forge to build a basic protocol analyzer, inspired by the Cryptographic Protocol Shape Analyzer (CPSA). We show that we can obtain editing, basic visualization, and scriptability at no extra cost beyond embedding in Forge, and a modern, domain-specific visualization for relatively little extra effort.  more » « less
Award ID(s):
1714431
PAR ID:
10337612
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
Lecture notes in computer science
Volume:
13066
ISSN:
0302-9743
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ; ; ; ; ; ; ; et al (, Proceedings of the ACM on Programming Languages)
    This paper presents the design ofForge, a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry. Forge offers aprogression of languagesthat improve the learning experience by only gradually increasing in expressive power. Forge supportscustom visualizationof its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety oftesting featuresto ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use. 
    more » « less
  2. ; ; ; ; ; (, Current Protocols)
    Abstract Identifying impacted pathways is important because it provides insights into the biology underlying conditions beyond the detection of differentially expressed genes. Because of the importance of such analysis, more than 100 pathway analysis methods have been developed thus far. Despite the availability of many methods, it is challenging for biomedical researchers to learn and properly perform pathway analysis. First, the sheer number of methods makes it challenging to learn and choose the correct method for a given experiment. Second, computational methods require users to be savvy with coding syntax, and comfortable with command‐line environments, areas that are unfamiliar to most life scientists. Third, as learning tools and computational methods are typically implemented only for a few species (i.e., human and some model organisms), it is difficult to perform pathway analysis on other species that are not included in many of the current pathway analysis tools. Finally, existing pathway tools do not allow researchers to combine, compare, and contrast the results of different methods and experiments for both hypothesis testing and analysis purposes. To address these challenges, we developed an open‐source R package for Consensus Pathway Analysis (RCPA) that allows researchers to conveniently: (1) download and process data from NCBI GEO; (2) perform differential analysis using established techniques developed for both microarray and sequencing data; (3) perform both gene set enrichment, as well as topology‐based pathway analysis using different methods that seek to answer different research hypotheses; (4) combine methods and datasets to find consensus results; and (5) visualize analysis results and explore significantly impacted pathways across multiple analyses. This protocol provides many example code snippets with detailed explanations and supports the analysis of more than 1000 species, two pathway databases, three differential analysis techniques, eight pathway analysis tools, six meta‐analysis methods, and two consensus analysis techniques. The package is freely available on the CRAN repository. © 2024 The Authors. Current Protocols published by Wiley Periodicals LLC. Basic Protocol 1: Processing Affymetrix microarrays Basic Protocol 2: Processing Agilent microarrays Support Protocol: Processing RNA sequencing (RNA‐Seq) data Basic Protocol 3: Differential analysis of microarray data (Affymetrix and Agilent) Basic Protocol 4: Differential analysis of RNA‐Seq data Basic Protocol 5: Gene set enrichment analysis Basic Protocol 6: Topology‐based (TB) pathway analysis Basic Protocol 7: Data integration and visualization 
    more » « less
  3. ; ; ; ; (, Proceedings of the ACM on Management of Data)
    Supporting the interactive exploration of large datasets is a popular and challenging use case for data management systems. Traditionally, the interface and the back-end system are built and optimized separately, and interface design and system optimization require different skill sets that are difficult for one person to master. To enable analysts to focus on visualization design, we contribute VegaPlus, a system that automatically optimizes interactive dashboards to support large datasets. To achieve this, VegaPlus leverages two core ideas. First, we introduce an optimizer that can reason about execution plans in Vega, a back-end DBMS, or a mix of both environments. The optimizer also considers how user interactions may alter execution plan performance, and can partially or fully rewrite the plans when needed. Through a series of benchmark experiments on seven different dashboard designs, our results show that VegaPlus provides superior performance and versatility compared to standard dashboard optimization techniques. 
    more » « less
  4. ; ; (, Current Protocols)
    Abstract Histone acetyltransferases (HATs, also known as lysine acetyltransferases, KATs) catalyze acetylation of their cognate protein substrates using acetyl‐CoA (Ac‐CoA) as a cofactor and are involved in various physiological and pathological processes. Advances in mass spectrometry‐based proteomics have allowed the discovery of thousands of acetylated proteins and the specific acetylated lysine sites. However, due to the rapid dynamics and functional redundancy of HAT activities, and the limitation of using antibodies to capture acetylated lysines, it is challenging to systematically and precisely define both the substrates and sites directly acetylated by a given HAT. Here, we describe a chemoproteomic approach to identify and profile protein substrates of individual HAT enzymes on the proteomic scale. The approach involves protein engineering to enlarge the Ac‐CoA binding pocket of the HAT of interest, such that a mutant form is generated that can use functionalized acyl‐CoAs as a cofactor surrogate to bioorthogonally label its protein substrates. The acylated protein substrates can then be chemoselectively conjugated either with a fluorescent probe (for imaging detection) or with a biotin handle (for streptavidin pulldown and chemoproteomic identification). This modular chemical biology approach has been successfully implemented to identify protein substrates of p300, GCN5, and HAT1, and it is expected that this method can be applied to profile and identify the sub‐acetylomes of many other HAT enzymes. © 2022 Wiley Periodicals LLC. Basic Protocol 1: Labeling HAT protein substrates with azide/alkyne‐biotin Alternate Protocol: Labeling protein substrates of HATs with azide/alkyne‐TAMRA for in‐gel visualization Support Protocol 1: Expression and purification of HAT mutants Support Protocol 2: Synthesis of Ac‐CoA surrogates Basic Protocol 2: Streptavidin enrichment of biotinylated HAT substrates Basic Protocol 3: Chemoproteomic identification of HAT substrates Basic Protocol 4: Validation of specific HAT substrates with western blotting 
    more » « less
  5. ; ; ; ; ; ; ; ; ; ; et al (, Current Protocols)
    Abstract PhyloFisher is a software package written primarily in Python3 that can be used for the creation, analysis, and visualization of phylogenomic datasets that consist of protein sequences from eukaryotic organisms. Unlike many existing phylogenomic pipelines, PhyloFisher comes with a manually curated database of 240 protein‐coding genes, a subset of a previous phylogenetic dataset sampled from 304 eukaryotic taxa. The software package can also utilize a user‐created database of eukaryotic proteins, which may be more appropriate for shallow evolutionary questions. PhyloFisher is also equipped with a set of utilities to aid in running routine analyses, such as the prediction of alternative genetic codes, removal of genes and/or taxa based on occupancy/completeness of the dataset, testing for amino acid compositional heterogeneity among sequences, removal of heterotachious and/or fast‐evolving sites, removal of fast‐evolving taxa, supermatrix creation from randomly resampled genes, and supermatrix creation from nucleotide sequences. © 2024 Wiley Periodicals LLC. Basic Protocol 1: Constructing a phylogenomic dataset Basic Protocol 2: Performing phylogenomic analyses Support Protocol 1: Installing PhyloFisher Support Protocol 2: Creating a custom phylogenomic database 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email