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.


Title: Generating and Exploiting Automated Reasoning Proof Certificates
Moving toward a full suite of proof-producing automated reasoning tools with SMT solvers that can produce full, independently checkable proofs for real-world problems.  more » « less
Award ID(s):
2110397
PAR ID:
10475462
Author(s) / Creator(s):
; ; ; ; ; ; ; ; ; ; ; ;
Publisher / Repository:
ACM
Date Published:
Journal Name:
Communications of the ACM
Volume:
66
Issue:
10
ISSN:
0001-0782
Page Range / eLocation ID:
86 to 95
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Adeno-associated viral vectors (AAVs) are the predominant viral vectors used for gene therapy applications. A significant challenge in obtaining effective doses is removing non-therapeutic empty viral capsids lacking DNA cargo. Current methods for separating full (gene-containing) and empty capsids are challenging to scale, produce low product yields, are slow, and are difficult to operationalize for continuous biomanufacturing. This communication demonstrates the feasibility of separating full and empty capsids by ultrafiltration. Separation performance was quantified by measuring the sieving coefficients for full and empty capsids using ELISA, qPCR, and an infectivity assay based on the live cell imaging of green fluorescent protein expression. We demonstrated that polycarbonate track-etched membranes with a pore size of 30 nm selectively permeated empty capsids to full capsids, with a high recovery yield (89%) for full capsids. The average sieving coefficients of full and empty capsids obtained through ELISA/qPCR were calculated as 0.25 and 0.49, indicating that empty capsids were about twice as permeable as full capsids. Establishing ultrafiltration as a viable unit operation for separating full and empty AAV capsids has implications for developing the scale-free continuous purification of AAVs. 
    more » « less
  2. EDBT (Ed.)
    Data integration is an important step in any data science pipeline where the objective is to unify the information available in differ- ent datasets for comprehensive analysis. Full Disjunction, which is an associative extension of the outer join operator, has been shown to be an effective operator for integrating datasets. It fully preserves and combines the available information. Existing Full Disjunction algorithms only consider the equi-join scenario where only tuples having the same value on joining columns are integrated. This, however, does not realistically represent many realistic scenarios where datasets come from diverse sources with inconsistent values (e.g., synonyms, abbreviations, etc.) and with limited metadata. So, joining just on equal values severely limits the ability of Full Disjunction to fully combine datasets. Thus, in this work, we propose an extension of Full Disjunction to also account for “fuzzy” matches among tuples. We present a novel data-driven approach to enable the joining of approximate or fuzzy matches within Full Disjunction. Experimentally, we show that fuzzy Full Disjunction does not add significant time over- head over a state-of-the-art Full Disjunction implementation and also that it enhances the accuracy of a downstream data quality task. 
    more » « less
  3. The full data set for the seed germination survey conducted at Barro Colorado Island, Panama formatted as an easily readable and searchable PDF file. Table 1 describes the column headings for the full data set. Table 2 defines codes used frequently in the full data set . Table 3 defines codes used in "Duration Notes", the final column of the full data set. Table 4 defines miscellaneous symbols used in Supplement 2. Table 5 defines symbols used to represent probability levels. The next 195 pages present the full data set.The source reference follows: Garwood, N. C. 2024. Chapter 18 - An Expanded Survey of Seed Germination for Barro Colorado Island. In The First 100 Years of Research on Barro Colorado: Plant and Ecosystem Science, ed. H. C. Muller-Landau and S. J. Wright: Smithsonian Institution Scholarly Press, Washington, DC. 
    more » « less
  4. Full-body tracking in virtual reality improves presence, allows interaction via body postures, and facilitates better social expression among users. However, full-body tracking systems today require a complex setup fixed to the environment (e.g., multiple lighthouses/cameras) and a laborious calibration process, which goes against the desire to make VR systems more portable and integrated. We present HybridTrak, which provides accurate, real-time full-body tracking by augmenting inside-out1 upper-body VR tracking systems with a single external off-the-shelf RGB web camera. HybridTrak uses a full-neural solution to convert and transform users’ 2D full-body poses from the webcam to 3D poses leveraging the inside-out upper-body tracking data. We showed HybridTrak is more accurate than RGB or depth-based tracking methods on the MPI-INF-3DHP dataset. We also tested HybridTrak in the popular VRChat app and showed that body postures presented by HybridTrak are more distinguishable and more natural than a solution using an RGBD camera. 
    more » « less
  5. In medical vision, different imaging modalities provide complementary information. However, in practice, not all modalities may be available during inference or even training. Previous approaches, e.g., knowledge distillation or image synthesis, often assume the availability of full modalities for all patients during training; this is unrealistic and impractical due to the variability in data collection across sites. We propose a novel approach to learn enhanced modality-agnostic representations by employing a meta-learning strategy in training, even when only limited full modality samples are available. Meta-learning enhances partial modality representations to full modality representations by meta-training on partial modality data and meta-testing on limited full modality samples. Additionally, we co-supervise this feature enrichment by introducing an auxiliary adversarial learning branch. More specifically, a missing modality detector is used as a discriminator to mimic the full modality setting. Our segmentation framework significantly outperforms state-of-the-art brain tumor segmentation techniques in missing modality scenarios. 
    more » « less