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: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Abstract This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool’s architectural design and highlight the major features and components introduced since its initial release.  more » « less
Award ID(s):
2211505
PAR ID:
10584626
Author(s) / Creator(s):
; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;
Editor(s):
Gurfinkel, Arie; Ganesh, Vijay
Publisher / Repository:
Springer Nature Switzerland
Date Published:
Page Range / eLocation ID:
249 to 264
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ABSTRACT MotivationSNAPSHOT USA is an annual, multicontributor camera trap survey of mammals across the United States. The growing SNAPSHOT USA dataset is intended for tracking the spatial and temporal responses of mammal populations to changes in land use, land cover and climate. These data will be useful for exploring the drivers of spatial and temporal changes in relative abundance and distribution, as well as the impacts of species interactions on daily activity patterns. Main Types of Variables ContainedSNAPSHOT USA 2019–2023 contains 987,979 records of camera trap image sequence data and 9694 records of camera trap deployment metadata. Spatial Location and GrainData were collected across the United States of America in all 50 states, 12 ecoregions and many ecosystems. Time Period and GrainData were collected between 1st August and 29th December each year from 2019 to 2023. Major Taxa and Level of MeasurementThe dataset includes a wide range of taxa but is primarily focused on medium to large mammals. Software FormatSNAPSHOT USA 2019–2023 comprises two .csv files. The original data can be found within the SNAPSHOT USA Initiative in the Wildlife Insights platform. 
    more » « less
  2. BackgroundA lack of in utero imaging data hampers our understanding of the connections in the human fetal brain. Generalizing observations from postmortem subjects and premature newborns is inaccurate due to technical and biological differences. PurposeTo evaluate changes in fetal brain structural connectivity between 23 and 35 weeks postconceptional age using a spatiotemporal atlas of diffusion tensor imaging (DTI). Study TypeRetrospective. PopulationPublicly available diffusion atlases, based on 60 healthy women (age 18–45 years) with normal prenatal care, from 23 and 35 weeks of gestation. Field Strength/Sequence3.0 Tesla/DTI acquired with diffusion‐weighted echo planar imaging (EPI). AssessmentWe performed whole‐brain fiber tractography from DTI images. The cortical plate of each diffusion atlas was segmented and parcellated into 78 regions derived from the Edinburgh Neonatal Atlas (ENA33). Connectivity matrices were computed, representing normalized fiber connections between nodes. We examined the relationship between global efficiency (GE), local efficiency (LE), small‐worldness (SW), nodal efficiency (NE), and betweenness centrality (BC) with gestational age (GA) and with laterality. Statistical TestsLinear regression was used to analyze changes in GE, LE, NE, and BC throughout gestation, and to assess changes in laterality. Thet‐tests were used to assess SW.P‐values were corrected using Holm‐Bonferroni method. A correctedP‐value <0.05 was considered statistically significant. ResultsNetwork analysis revealed a significant weekly increase in GE (5.83%/week, 95% CI 4.32–7.37), LE (5.43%/week, 95% CI 3.63–7.25), and presence of SW across GA. No significant hemisphere differences were found in GE (P = 0.971) or LE (P = 0.458). Increasing GA was significantly associated with increasing NE in 41 nodes, increasing BC in 3 nodes, and decreasing BC in 2 nodes. Data ConclusionExtensive network development and refinement occur in the second and third trimesters, marked by a rapid increase in global integration and local segregation. Level of Evidence3 Technical EfficacyStage 2 
    more » « less
  3. Abstract AimsTo examine changes in drinking behavior among United States (US) adults between March 10 and July 21, 2020, a critical period during the COVID‐19 pandemic. DesignLongitudinal, internet‐based panel survey. SettingThe Understanding America Study (UAS), a nationally representative panel of US adults age 18 or older. ParticipantsA total of 4298 US adults who reported alcohol use. MeasurementsChanges in number of reported drinking days from March 11, 2020 through July 21, 2020 in the overall sample and stratified by sex, age, race/ethnicity, household structure, poverty status, and census region. FindingsCompared with March 11, the number of drinking days per week was significantly higher on April 1 by an average of 0.36 days (95% CI = 0.30, 0.43), on May 1 by an average of 0.55 days (95% CI = 0.47, 0.63), on June 1 by an average of 0.41 days (95% CI = 0.33, 0.49), and on July 1 by an average of 0.39 days (95% CI = 0.31, 0.48). Males, White participants, and older adults reported sustained increases in drinking days, whereas female participants and individuals living under the federal poverty line had attenuated drinking days in the latter part of the study period. ConclusionsBetween March and mid‐July 2020, adults in the United States reported increases in the number of drinking days, with sustained increases observed among males, White participants, and older adults. 
    more » « less
  4. Abstract MotivationMapping positional features from one-dimensional (1D) sequences onto three-dimensional (3D) structures of biological macromolecules is a powerful tool to show geometric patterns of biochemical annotations and provide a better understanding of the mechanisms underpinning protein and nucleic acid function at the atomic level. ResultsWe present a new library designed to display fully customizable interactive views between 1D positional features of protein and/or nucleic acid sequences and their 3D structures as isolated chains or components of macromolecular assemblies. Availability and implementationhttps://github.com/rcsb/rcsb-saguaro-3d. Supplementary informationSupplementary data are available at Bioinformatics online. 
    more » « less
  5. Abstract AimThis study investigates the biogeographic patterns of Pacific white‐sided dolphins (Lagenorhynchus obliquidens) in the Eastern North Pacific based on long‐term passive acoustic records. We aim to elucidate the ecological and behavioural significance of distinct echolocation click types and their implications for population delineation, geographic distribution, environmental adaptation and management. LocationEastern North Pacific Ocean. Time Period2005–2021. Major Taxa StudiedPacific white‐sided dolphin. MethodsOver 50 cumulative years of passive acoustic monitoring (PAM) data from 14 locations were analyzed using a deep neural network to classify two distinct Pacific white‐sided dolphin echolocation click types. The study assessed spatial, diel, seasonal and interannual patterns of the two click types, correlating them with major environmental drivers such as the El Niño Southern Oscillation and the North Pacific Gyre Oscillation, and modeling long‐term spatial‐seasonal patterns. ResultsDistinct spatial, diel and seasonal patterns were observed for each click type. Significant biogeographical shifts in presence were observed following the 2014–2016 marine heatwave event. Main ConclusionsDistinct spatial distributions of the two click types support the hypothesis that Pacific white‐sided dolphins produce population‐specific echolocation clicks. Seasonal and diel patterns suggest spatiotemporal niche partitioning between the populations in Southern California. Interannual changes, notably initiated during the 2014–2016 marine heatwave, indicate climate‐driven range expansions and contractions related to gradual tropicalization of the Southern California Bight. 
    more » « less