Showing 1–27 of 27 results for author: Greve, D

A Contrast-Agnostic Method for Ultra-High Resolution Claustrum Segmentation

Authors: Chiara Mauri, Ryan Fritz, Jocelyn Mora, Benjamin Billot, Juan Eugenio Iglesias, Koen Van Leemput, Jean Augustinack, Douglas N Greve

Abstract: The claustrum is a band-like gray matter structure located between putamen and insula whose exact functions are still actively researched. Its sheet-like structure makes it barely visible in in vivo Magnetic Resonance Imaging (MRI) scans at typical resolutions and neuroimaging tools for its study, including methods for automatic segmentation, are currently very limited. In this paper, we propose a… ▽ More The claustrum is a band-like gray matter structure located between putamen and insula whose exact functions are still actively researched. Its sheet-like structure makes it barely visible in in vivo Magnetic Resonance Imaging (MRI) scans at typical resolutions and neuroimaging tools for its study, including methods for automatic segmentation, are currently very limited. In this paper, we propose a contrast- and resolution-agnostic method for claustrum segmentation at ultra-high resolution (0.35 mm isotropic); the method is based on the SynthSeg segmentation framework (Billot et al., 2023), which leverages the use of synthetic training intensity images to achieve excellent generalization. In particular, SynthSeg requires only label maps to be trained, since corresponding intensity images are synthesized on the fly with random contrast and resolution. We trained a deep learning network for automatic claustrum segmentation, using claustrum manual labels obtained from 18 ultra-high resolution MRI scans (mostly ex vivo). We demonstrated the method to work on these 18 high resolution cases (Dice score = 0.632, mean surface distance = 0.458 mm, and volumetric similarity = 0.867 using 6-fold Cross Validation (CV)), and also on in vivo T1-weighted MRI scans at typical resolutions (~1 mm isotropic). We also demonstrated that the method is robust in a test-retest setting and when applied to multimodal imaging (T2-weighted, Proton Density and quantitative T1 scans). To the best of our knowledge this is the first accurate method for automatic ultra-high resolution claustrum segmentation, which is robust against changes in contrast and resolution. The method is released at https://github.com/chiara-mauri/claustrum_segmentation and as part of the neuroimaging package Freesurfer (Fischl, 2012). △ Less

Submitted 29 April, 2025; v1 submitted 22 November, 2024; originally announced November 2024.

Comments: 20 pages, 15 figures, 3 tables

Recon-all-clinical: Cortical surface reconstruction and analysis of heterogeneous clinical brain MRI

Authors: Karthik Gopinath, Douglas N. Greve, Colin Magdamo, Steve Arnold, Sudeshna Das, Oula Puonti, Juan Eugenio Iglesias

Abstract: Surface-based analysis of the cerebral cortex is ubiquitous in human neuroimaging with MRI. It is crucial for cortical registration, parcellation, and thickness estimation. Traditionally, these analyses require high-resolution, isotropic scans with good gray-white matter contrast, typically a 1mm T1-weighted scan. This excludes most clinical MRI scans, which are often anisotropic and lack the nece… ▽ More Surface-based analysis of the cerebral cortex is ubiquitous in human neuroimaging with MRI. It is crucial for cortical registration, parcellation, and thickness estimation. Traditionally, these analyses require high-resolution, isotropic scans with good gray-white matter contrast, typically a 1mm T1-weighted scan. This excludes most clinical MRI scans, which are often anisotropic and lack the necessary T1 contrast. To enable large-scale neuroimaging studies using vast clinical data, we introduce recon-all-clinical, a novel method for cortical reconstruction, registration, parcellation, and thickness estimation in brain MRI scans of any resolution and contrast. Our approach employs a hybrid analysis method that combines a convolutional neural network (CNN) trained with domain randomization to predict signed distance functions (SDFs) and classical geometry processing for accurate surface placement while maintaining topological and geometric constraints. The method does not require retraining for different acquisitions, thus simplifying the analysis of heterogeneous clinical datasets. We tested recon-all-clinical on multiple datasets, including over 19,000 clinical scans. The method consistently produced precise cortical reconstructions and high parcellation accuracy across varied MRI contrasts and resolutions. Cortical thickness estimates are precise enough to capture aging effects independently of MRI contrast, although accuracy varies with slice thickness. Our method is publicly available at https://surfer.nmr.mgh.harvard.edu/fswiki/recon-all-clinical, enabling researchers to perform detailed cortical analysis on the huge amounts of already existing clinical MRI scans. This advancement may be particularly valuable for studying rare diseases and underrepresented populations where research-grade MRI data is scarce. △ Less

Submitted 5 September, 2024; originally announced September 2024.

Comments: 16 pages in the manuscript with 11 page supplementary material

An amplitude equation for the conserved-Hopf bifurcation -- derivation, analysis and assessment

Authors: Daniel Greve, Uwe Thiele

Abstract: We employ weakly nonlinear theory to derive an amplitude equation for the conserved-Hopf instability, i.e., a generic large-scale oscillatory instability for systems with two conservation laws. The resulting equation represents in the conserved case the equivalent of the complex Ginzburg-Landau equation obtained in the nonconserved case as amplitude equation for the standard Hopf bifurcation.Consi… ▽ More We employ weakly nonlinear theory to derive an amplitude equation for the conserved-Hopf instability, i.e., a generic large-scale oscillatory instability for systems with two conservation laws. The resulting equation represents in the conserved case the equivalent of the complex Ginzburg-Landau equation obtained in the nonconserved case as amplitude equation for the standard Hopf bifurcation.Considering first the case of a relatively simple symmetric Cahn-Hilliard model with purely nonreciprocal coupling, we derive the nonlinear nonlocal amplitude equation with real coefficients and show that its bifurcation diagram and time evolution well agree with results for the full model. The solutions of the amplitude equation and their stability are analytically obtained thereby showing that in oscillatory phase separation the suppression of coarsening is universal. Second, we lift the two restrictions and obtain the amplitude equation in the generic case that has complex coefficients, that also shows very good agreement with the full model as exemplified for some transient dynamics that converges to traveling wave states. △ Less

Submitted 13 January, 2025; v1 submitted 4 July, 2024; originally announced July 2024.

High-resolution segmentations of the hypothalamus and its subregions for training of segmentation models

Authors: Livia Rodrigues, Martina Bocchetta, Oula Puonti, Douglas Greve, Ana Carolina Londe, Marcondes França, Simone Appenzeller, Leticia Rittner, Juan Eugenio Iglesias

Abstract: Segmentation of brain structures on magnetic resonance imaging (MRI) is a highly relevant neuroimaging topic, as it is a prerequisite for different analyses such as volumetry or shape analysis. Automated segmentation facilitates the study of brain structures in larger cohorts when compared with manual segmentation, which is time-consuming. However, the development of most automated methods relies… ▽ More Segmentation of brain structures on magnetic resonance imaging (MRI) is a highly relevant neuroimaging topic, as it is a prerequisite for different analyses such as volumetry or shape analysis. Automated segmentation facilitates the study of brain structures in larger cohorts when compared with manual segmentation, which is time-consuming. However, the development of most automated methods relies on large and manually annotated datasets, which limits the generalizability of these methods. Recently, new techniques using synthetic images have emerged, reducing the need for manual annotation. Here we provide HELM, Hypothalamic ex vivo Label Maps, a dataset composed of label maps built from publicly available ultra-high resolution ex vivo MRI from 10 whole hemispheres, which can be used to develop segmentation methods using synthetic data. The label maps are obtained with a combination of manual labels for the hypothalamic regions and automated segmentations for the rest of the brain, and mirrored to simulate entire brains. We also provide the pre-processed ex vivo scans, as this dataset can support future projects to include other structures after these are manually segmented. △ Less

Submitted 27 June, 2024; originally announced June 2024.

Coexistence of uniform and oscillatory states resulting from nonreciprocity and conservation laws

Authors: Daniel Greve, Giorgio Lovato, Tobias Frohoff-Hülsmann, Uwe Thiele

Abstract: Employing a two-species Cahn-Hilliard model with nonreciprocal interactions we show that the interplay of nonreciprocity and conservation laws results in the robust coexistence of uniform stationary and oscillatory phases as well as of uniform and crystalline phases. For nonequilibrium models with a spurious gradient dynamics structure such coexistencies between two or more nonequilibrium phases a… ▽ More Employing a two-species Cahn-Hilliard model with nonreciprocal interactions we show that the interplay of nonreciprocity and conservation laws results in the robust coexistence of uniform stationary and oscillatory phases as well as of uniform and crystalline phases. For nonequilibrium models with a spurious gradient dynamics structure such coexistencies between two or more nonequilibrium phases and resulting phase diagrams can nevertheless be predicted by a Maxwell double-tangent construction. This includes phases with sustained regular or irregular out-of-equilibrium dynamics as further corroborated by bifurcation studies and time simulations. △ Less

Submitted 13 January, 2025; v1 submitted 13 February, 2024; originally announced February 2024.

H-SynEx: Using synthetic images and ultra-high resolution ex vivo MRI for hypothalamus subregion segmentation

Authors: Livia Rodrigues, Martina Bocchetta, Oula Puonti, Douglas Greve, Ana Carolina Londe, Marcondes França, Simone Appenzeller, Juan Eugenio Iglesias, Leticia Rittner

Abstract: The hypothalamus is a small structure located in the center of the brain and is involved in significant functions such as sleeping, temperature, and appetite control. Various neurological disorders are also associated with hypothalamic abnormalities. Automated image analysis of this structure from brain MRI is thus highly desirable to study the hypothalamus in vivo. However, most automated segment… ▽ More The hypothalamus is a small structure located in the center of the brain and is involved in significant functions such as sleeping, temperature, and appetite control. Various neurological disorders are also associated with hypothalamic abnormalities. Automated image analysis of this structure from brain MRI is thus highly desirable to study the hypothalamus in vivo. However, most automated segmentation tools currently available focus exclusively on T1w images. In this study, we introduce H-SynEx, a machine learning method for automated segmentation of hypothalamic subregions that generalizes across different MRI sequences and resolutions without retraining. H-synEx was trained with synthetic images built from label maps derived from ultra-high resolution ex vivo MRI scans, which enables finer-grained manual segmentation when compared with 1mm isometric in vivo images. We validated our method using Dice Coefficient (DSC) and Average Hausdorff distance (AVD) across in vivo images from six different datasets with six different MRI sequences (T1, T2, proton density, quantitative T1, fractional anisotrophy, and FLAIR). Statistical analysis compared hypothalamic subregion volumes in controls, Alzheimer's disease (AD), and behavioral variant frontotemporal dementia (bvFTD) subjects using the Area Under the Receiving Operating Characteristic curve (AUROC) and Wilcoxon rank sum test. Our results show that H-SynEx successfully leverages information from ultra-high resolution scans to segment in vivo from different MRI sequences. Our automated segmentation was able to discriminate controls versus Alzheimer's Disease patients on FLAIR images with 5mm spacing. H-SynEx is openly available at https://github.com/liviamarodrigues/hsynex. △ Less

Submitted 1 July, 2024; v1 submitted 30 January, 2024; originally announced January 2024.

Drops on polymer brushes -- advances in thin-film modelling of adaptive substrates

Authors: Simon Hartmann, Jan Diekmann, Daniel Greve, Uwe Thiele

Abstract: We briefly review recent advances in the hydrodynamic modeling of the dynamics of droplets on adaptive substrates, in particular, solids that are covered by polymer brushes. Thereby, the focus are long-wave and full-curvature variants of mesoscopic hydrodynamic models in gradient dynamics form. After introducing the approach for films/drops of nonvolatile simple liquids on rigid smooth solid subst… ▽ More We briefly review recent advances in the hydrodynamic modeling of the dynamics of droplets on adaptive substrates, in particular, solids that are covered by polymer brushes. Thereby, the focus are long-wave and full-curvature variants of mesoscopic hydrodynamic models in gradient dynamics form. After introducing the approach for films/drops of nonvolatile simple liquids on rigid smooth solid substrate, it is first expanded to an arbitrary number of coupled degrees of freedom, before considering the specific case of drops of volatile liquids on brush-covered solids. After presenting the model its usage is illustrated by briefly considering the natural and forced spreading of drops of nonvolatile liquids on a horizontal brush-covered substrate as well as drops sliding down a brush-covered incline. Finally, also volatile liquids are considered. △ Less

Submitted 22 December, 2023; v1 submitted 13 November, 2023; originally announced November 2023.

Journal ref: Langmuir 40, 4001-4021 (2024)

Cortical analysis of heterogeneous clinical brain MRI scans for large-scale neuroimaging studies

Authors: Karthik Gopinath, Douglas N. Greve, Sudeshna Das, Steve Arnold, Colin Magdamo, Juan Eugenio Iglesias

Abstract: Surface analysis of the cortex is ubiquitous in human neuroimaging with MRI, e.g., for cortical registration, parcellation, or thickness estimation. The convoluted cortical geometry requires isotropic scans (e.g., 1mm MPRAGEs) and good gray-white matter contrast for 3D reconstruction. This precludes the analysis of most brain MRI scans acquired for clinical purposes. Analyzing such scans would ena… ▽ More Surface analysis of the cortex is ubiquitous in human neuroimaging with MRI, e.g., for cortical registration, parcellation, or thickness estimation. The convoluted cortical geometry requires isotropic scans (e.g., 1mm MPRAGEs) and good gray-white matter contrast for 3D reconstruction. This precludes the analysis of most brain MRI scans acquired for clinical purposes. Analyzing such scans would enable neuroimaging studies with sample sizes that cannot be achieved with current research datasets, particularly for underrepresented populations and rare diseases. Here we present the first method for cortical reconstruction, registration, parcellation, and thickness estimation for clinical brain MRI scans of any resolution and pulse sequence. The methods has a learning component and a classical optimization module. The former uses domain randomization to train a CNN that predicts an implicit representation of the white matter and pial surfaces (a signed distance function) at 1mm isotropic resolution, independently of the pulse sequence and resolution of the input. The latter uses geometry processing to place the surfaces while accurately satisfying topological and geometric constraints, thus enabling subsequent parcellation and thickness estimation with existing methods. We present results on 5mm axial FLAIR scans from ADNI and on a highly heterogeneous clinical dataset with 5,000 scans. Code and data are publicly available at https://surfer.nmr.mgh.harvard.edu/fswiki/recon-all-clinical △ Less

Submitted 2 May, 2023; originally announced May 2023.

Anatomy-aware and acquisition-agnostic joint registration with SynthMorph

Authors: Malte Hoffmann, Andrew Hoopes, Douglas N. Greve, Bruce Fischl, Adrian V. Dalca

Abstract: Affine image registration is a cornerstone of medical image analysis. While classical algorithms can achieve excellent accuracy, they solve a time-consuming optimization for every image pair. Deep-learning (DL) methods learn a function that maps an image pair to an output transform. Evaluating the function is fast, but capturing large transforms can be challenging, and networks tend to struggle if… ▽ More Affine image registration is a cornerstone of medical image analysis. While classical algorithms can achieve excellent accuracy, they solve a time-consuming optimization for every image pair. Deep-learning (DL) methods learn a function that maps an image pair to an output transform. Evaluating the function is fast, but capturing large transforms can be challenging, and networks tend to struggle if a test-image characteristic shifts from the training domain, such as resolution. Most affine methods are agnostic to the anatomy the user wishes to align, meaning the registration will be inaccurate if algorithms consider all structures in the image. We address these shortcomings with SynthMorph, a fast, symmetric, diffeomorphic, and easy-to-use DL tool for joint affine-deformable registration of any brain image without preprocessing. First, we leverage a strategy that trains networks with widely varying images synthesized from label maps, yielding robust performance for image types unseen at training. Second, we optimize the spatial overlap of select anatomical labels. This enables networks to distinguish anatomy of interest from irrelevant structures, removing the need for preprocessing that excludes content that may impinge on anatomy-specific registration. Third, we combine the affine model with a deformable hypernetwork that lets users choose the optimal deformation-field regularity for their specific data, at registration time, in a fraction of the time required by classical methods. We analyze how competing architectures learn affine transforms and compare state-of-the-art registration tools across an extremely diverse set of neuroimaging data, aiming to truly capture the behavior of methods in the real world. SynthMorph demonstrates high accuracy and is available at https://w3id.org/synthmorph, as a single complete end-to-end solution for registration of brain MRI. △ Less

Submitted 11 July, 2024; v1 submitted 26 January, 2023; originally announced January 2023.

Comments: 33 pages, 19 figures, 4 tables, affine registration, deformable registration, deep learning, hypernetwork, domain shift, neuroimaging, final published version

Journal ref: Imaging Neuroscience, 2, 2024, 1-33

Stick-slip Dynamics in the Forced Wetting of Polymer Brushes

Authors: Daniel Greve, Simon Hartmann, Uwe Thiele

Abstract: We study the static and dynamic wetting of adaptive substrates using a mesoscopic hydrodynamic model for a liquid droplet on a solid substrate covered by a polymer brush. First, we show that on the macroscale Young's law still holds for the equilibrium contact angle and that on the mesoscale a Neumann-type law governs the shape of the wetting ridge. Following an analytic and numeric assessment of… ▽ More We study the static and dynamic wetting of adaptive substrates using a mesoscopic hydrodynamic model for a liquid droplet on a solid substrate covered by a polymer brush. First, we show that on the macroscale Young's law still holds for the equilibrium contact angle and that on the mesoscale a Neumann-type law governs the shape of the wetting ridge. Following an analytic and numeric assessment of the static profiles of droplet and wetting ridge, we examine the dynamics of the wetting ridge for a liquid meniscus that is advanced at constant speed. In other words, we consider an inverse Landau-Levich case where a brush-covered plate is introduced into (and not drawn from) a liquid bath. We find a characteristic stick-slip motion that emerges when the dynamic contact angle of the stationary moving meniscus decreases with increasing velocity, and relate the onset of slip to Gibbs' inequality and to a cross-over in relevant time scales. △ Less

Submitted 4 May, 2023; v1 submitted 25 January, 2023; originally announced January 2023.

Journal ref: Soft Matter 19, 4041-4061 (2023)

An Open-Source Tool for Longitudinal Whole-Brain and White Matter Lesion Segmentation

Authors: Stefano Cerri, Douglas N. Greve, Andrew Hoopes, Henrik Lundell, Hartwig R. Siebner, Mark Mühlau, Koen Van Leemput

Abstract: In this paper we describe and validate a longitudinal method for whole-brain segmentation of longitudinal MRI scans. It builds upon an existing whole-brain segmentation method that can handle multi-contrast data and robustly analyze images with white matter lesions. This method is here extended with subject-specific latent variables that encourage temporal consistency between its segmentation resu… ▽ More In this paper we describe and validate a longitudinal method for whole-brain segmentation of longitudinal MRI scans. It builds upon an existing whole-brain segmentation method that can handle multi-contrast data and robustly analyze images with white matter lesions. This method is here extended with subject-specific latent variables that encourage temporal consistency between its segmentation results, enabling it to better track subtle morphological changes in dozens of neuroanatomical structures and white matter lesions. We validate the proposed method on multiple datasets of control subjects and patients suffering from Alzheimer's disease and multiple sclerosis, and compare its results against those obtained with its original cross-sectional formulation and two benchmark longitudinal methods. The results indicate that the method attains a higher test-retest reliability, while being more sensitive to longitudinal disease effect differences between patient groups. An implementation is publicly available as part of the open-source neuroimaging package FreeSurfer. △ Less

Submitted 10 February, 2023; v1 submitted 10 July, 2022; originally announced July 2022.

A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A

Authors: David Greve, Jennifer Davis, Laura Humphrey

Abstract: The decentralized perimeter surveillance system (DPSS) seeks to provide a decentralized protocol for evenly distributing surveillance of a perimeter over time across an ensemble of unmanned aerial vehicles (UAVs) whose members may communicate only when in close proximity to each other. The protocol must also converge to an even distribution of the perimeter in bounded time. Two versions of the D… ▽ More The decentralized perimeter surveillance system (DPSS) seeks to provide a decentralized protocol for evenly distributing surveillance of a perimeter over time across an ensemble of unmanned aerial vehicles (UAVs) whose members may communicate only when in close proximity to each other. The protocol must also converge to an even distribution of the perimeter in bounded time. Two versions of the DPSS protocol presented in the original paper seem to converge in bounded time but only informal proofs and arguments are given. A later application of model checking to these protocols found an error in one of the key lemmas, invalidating the informal proof for one and casting doubt on the other. Therefore, a new hand proof of the convergence time for the simpler version of the DPSS protocol or algorithm, Algorithm A or DPSS-A, was developed by Jeremy Avigad and Floris van Doorn. This paper describes a mechanization of that hand proof in the logic of ACL2 and discusses three specific ACL2 utilities that proved useful for expressing and reasoning about the DPSS model. △ Less

Submitted 23 May, 2022; originally announced May 2022.

Comments: In Proceedings ACL2 2022, arXiv:2205.11103

Journal ref: EPTCS 359, 2022, pp. 33-47

Learning the Effect of Registration Hyperparameters with HyperMorph

Authors: Andrew Hoopes, Malte Hoffmann, Douglas N. Greve, Bruce Fischl, John Guttag, Adrian V. Dalca

Abstract: We introduce HyperMorph, a framework that facilitates efficient hyperparameter tuning in learning-based deformable image registration. Classical registration algorithms perform an iterative pair-wise optimization to compute a deformation field that aligns two images. Recent learning-based approaches leverage large image datasets to learn a function that rapidly estimates a deformation for a given… ▽ More We introduce HyperMorph, a framework that facilitates efficient hyperparameter tuning in learning-based deformable image registration. Classical registration algorithms perform an iterative pair-wise optimization to compute a deformation field that aligns two images. Recent learning-based approaches leverage large image datasets to learn a function that rapidly estimates a deformation for a given image pair. In both strategies, the accuracy of the resulting spatial correspondences is strongly influenced by the choice of certain hyperparameter values. However, an effective hyperparameter search consumes substantial time and human effort as it often involves training multiple models for different fixed hyperparameter values and may lead to suboptimal registration. We propose an amortized hyperparameter learning strategy to alleviate this burden by learning the impact of hyperparameters on deformation fields. We design a meta network, or hypernetwork, that predicts the parameters of a registration network for input hyperparameters, thereby comprising a single model that generates the optimal deformation field corresponding to given hyperparameter values. This strategy enables fast, high-resolution hyperparameter search at test-time, reducing the inefficiency of traditional approaches while increasing flexibility. We also demonstrate additional benefits of HyperMorph, including enhanced robustness to model initialization and the ability to rapidly identify optimal hyperparameter values specific to a dataset, image contrast, task, or even anatomical region, all without the need to retrain models. We make our code publicly available at http://hypermorph.voxelmorph.net. △ Less

Submitted 30 March, 2022; originally announced March 2022.

Comments: Accepted for publication at the Journal of Machine Learning for Biomedical Imaging (MELBA) at https://www.melba-journal.org

Interdigitated Columnar Representation of Personal Space and Visual Space in Human Parietal Cortex

Authors: Roger B. H. Tootell, Zahra Nasiriavanaki, Baktash Babadi, Douglas N. Greve, Shahin Nasr, Daphne J. Holt

Abstract: Personal space (PS) is the distance that people prefer to maintain between themselves and unfamiliar others. Interpersonal intrusion into a given persons PS evokes discomfort, and an urge to move further apart. We hypothesized that in parietal cortex: 1. PS processing involves a previously-described threat-sensitive brain circuit, and 2. the spatial encoding of distance is transformed accordingly,… ▽ More Personal space (PS) is the distance that people prefer to maintain between themselves and unfamiliar others. Interpersonal intrusion into a given persons PS evokes discomfort, and an urge to move further apart. We hypothesized that in parietal cortex: 1. PS processing involves a previously-described threat-sensitive brain circuit, and 2. the spatial encoding of distance is transformed accordingly, from purely sensory to PS-related. These hypotheses were tested using 7T fMRI at high spatial resolution. In response to images of different visual stimuli across a range of virtual distances, we found two categories of distance encoding in functionally corresponding columns within parietal cortex. First, PD (personal distance) columns responded selectively to moving and stationary face images presented at virtual distances nearer (but not further) than each subjects behaviorally-defined PS boundary. In the majority of PD columns, BOLD response amplitudes increased monotonically and nonlinearly with increasing virtual face proximity. In the remaining PD columns, BOLD responses decreased with increasing proximity. These fMRI response functions appear related to previously-reported variations in subjective discomfort levels, and physiologic arousal, during intrusion into but not beyond personal space. Secondly, DD (disparity distance) columns in parietal cortex responded selectively to disparity-based near or far distances, in random dot stimuli, like disparity-selective columns described previously in occipital cortex. In parietal cortex, maps of DD columns were systematically non-overlapping (interdigitated) with the PD columns. These results suggest that the transformation of spatial information, from visual to higher-order, may be computed in multiple small sites, rather than across a larger cortical gradient, in parietal cortex. △ Less

Submitted 14 March, 2022; v1 submitted 8 November, 2021; originally announced November 2021.

Comments: 19 pages, 10 figures and 1 table. Tootell and Nasiriavanaki share joint first authorship

SynthSeg: Segmentation of brain MRI scans of any contrast and resolution without retraining

Authors: Benjamin Billot, Douglas N. Greve, Oula Puonti, Axel Thielscher, Koen Van Leemput, Bruce Fischl, Adrian V. Dalca, Juan Eugenio Iglesias

Abstract: Despite advances in data augmentation and transfer learning, convolutional neural networks (CNNs) difficultly generalise to unseen domains. When segmenting brain scans, CNNs are highly sensitive to changes in resolution and contrast: even within the same MRI modality, performance can decrease across datasets. Here we introduce SynthSeg, the first segmentation CNN robust against changes in contrast… ▽ More Despite advances in data augmentation and transfer learning, convolutional neural networks (CNNs) difficultly generalise to unseen domains. When segmenting brain scans, CNNs are highly sensitive to changes in resolution and contrast: even within the same MRI modality, performance can decrease across datasets. Here we introduce SynthSeg, the first segmentation CNN robust against changes in contrast and resolution. SynthSeg is trained with synthetic data sampled from a generative model conditioned on segmentations. Crucially, we adopt a domain randomisation strategy where we fully randomise the contrast and resolution of the synthetic training data. Consequently, SynthSeg can segment real scans from a wide range of target domains without retraining or fine-tuning, which enables straightforward analysis of huge amounts of heterogeneous clinical data. Because SynthSeg only requires segmentations to be trained (no images), it can learn from labels obtained by automated methods on diverse populations (e.g., ageing and diseased), thus achieving robustness to a wide range of morphological variability. We demonstrate SynthSeg on 5,000 scans of six modalities (including CT) and ten resolutions, where it exhibits unparalleled generalisation compared with supervised CNNs, state-of-the-art domain adaptation, and Bayesian segmentation. Finally, we demonstrate the generalisability of SynthSeg by applying it to cardiac MRI and CT scans. △ Less

Submitted 28 February, 2023; v1 submitted 20 July, 2021; originally announced July 2021.

Journal ref: Medical Image Analysis (83), May 2023, pp 102789

Synthesis of Infinite-State Systems with Random Behavior

Authors: Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David Greve, Sanjai Rayadurgam, Michael W. Whalen

Abstract: Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its appl… ▽ More Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification,while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed frame-work unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems. △ Less

Submitted 25 September, 2020; originally announced September 2020.

Comments: 12 pages, 7 figures, The 35th IEEE/ACM International Conference on Automated Software Engineering (ASE 2020)

A Longitudinal Method for Simultaneous Whole-Brain and Lesion Segmentation in Multiple Sclerosis

Authors: Stefano Cerri, Andrew Hoopes, Douglas N. Greve, Mark Mühlau, Koen Van Leemput

Abstract: In this paper we propose a novel method for the segmentation of longitudinal brain MRI scans of patients suffering from Multiple Sclerosis. The method builds upon an existing cross-sectional method for simultaneous whole-brain and lesion segmentation, introducing subject-specific latent variables to encourage temporal consistency between longitudinal scans. It is very generally applicable, as it d… ▽ More In this paper we propose a novel method for the segmentation of longitudinal brain MRI scans of patients suffering from Multiple Sclerosis. The method builds upon an existing cross-sectional method for simultaneous whole-brain and lesion segmentation, introducing subject-specific latent variables to encourage temporal consistency between longitudinal scans. It is very generally applicable, as it does not make any prior assumptions on the scanner, the MRI protocol, or the number and timing of longitudinal follow-up scans. Preliminary experiments on three longitudinal datasets indicate that the proposed method produces more reliable segmentations and detects disease effects better than the cross-sectional method it is based upon. △ Less

Submitted 15 September, 2020; v1 submitted 12 August, 2020; originally announced August 2020.

SynthMorph: learning contrast-invariant registration without acquired images

Authors: Malte Hoffmann, Benjamin Billot, Douglas N. Greve, Juan Eugenio Iglesias, Bruce Fischl, Adrian V. Dalca

Abstract: We introduce a strategy for learning image registration without acquired imaging data, producing powerful networks agnostic to contrast introduced by magnetic resonance imaging (MRI). While classical registration methods accurately estimate the spatial correspondence between images, they solve an optimization problem for every new image pair. Learning-based techniques are fast at test time but lim… ▽ More We introduce a strategy for learning image registration without acquired imaging data, producing powerful networks agnostic to contrast introduced by magnetic resonance imaging (MRI). While classical registration methods accurately estimate the spatial correspondence between images, they solve an optimization problem for every new image pair. Learning-based techniques are fast at test time but limited to registering images with contrasts and geometric content similar to those seen during training. We propose to remove this dependency on training data by leveraging a generative strategy for diverse synthetic label maps and images that exposes networks to a wide range of variability, forcing them to learn more invariant features. This approach results in powerful networks that accurately generalize to a broad array of MRI contrasts. We present extensive experiments with a focus on 3D neuroimaging, showing that this strategy enables robust and accurate registration of arbitrary MRI contrasts even if the target contrast is not seen by the networks during training. We demonstrate registration accuracy surpassing the state of the art both within and across contrasts, using a single model. Critically, training on arbitrary shapes synthesized from noise distributions results in competitive performance, removing the dependency on acquired data of any kind. Additionally, since anatomical label maps are often available for the anatomy of interest, we show that synthesizing images from these dramatically boosts performance, while still avoiding the need for real intensity images. Our code is available at https://w3id.org/synthmorph. △ Less

Submitted 3 March, 2022; v1 submitted 21 April, 2020; originally announced April 2020.

Comments: 16 pages, 15 figures, 3 tables, deformable image registration, data independence, deep learning, MRI-contrast invariance, anatomy agnosticism, final published version

Journal ref: IEEE Trans Med Imaging, 41 (3), 2022, 543-558

A Learning Strategy for Contrast-agnostic MRI Segmentation

Authors: Benjamin Billot, Douglas Greve, Koen Van Leemput, Bruce Fischl, Juan Eugenio Iglesias, Adrian V. Dalca

Abstract: We present a deep learning strategy that enables, for the first time, contrast-agnostic semantic segmentation of completely unpreprocessed brain MRI scans, without requiring additional training or fine-tuning for new modalities. Classical Bayesian methods address this segmentation problem with unsupervised intensity models, but require significant computational resources. In contrast, learning-bas… ▽ More We present a deep learning strategy that enables, for the first time, contrast-agnostic semantic segmentation of completely unpreprocessed brain MRI scans, without requiring additional training or fine-tuning for new modalities. Classical Bayesian methods address this segmentation problem with unsupervised intensity models, but require significant computational resources. In contrast, learning-based methods can be fast at test time, but are sensitive to the data available at training. Our proposed learning method, SynthSeg, leverages a set of training segmentations (no intensity images required) to generate synthetic sample images of widely varying contrasts on the fly during training. These samples are produced using the generative model of the classical Bayesian segmentation framework, with randomly sampled parameters for appearance, deformation, noise, and bias field. Because each mini-batch has a different synthetic contrast, the final network is not biased towards any MRI contrast. We comprehensively evaluate our approach on four datasets comprising over 1,000 subjects and four types of MR contrast. The results show that our approach successfully segments every contrast in the data, performing slightly better than classical Bayesian segmentation, and three orders of magnitude faster. Moreover, even within the same type of MRI contrast, our strategy generalizes significantly better across datasets, compared to training using real images. Finally, we find that synthesizing a broad range of contrasts, even if unrealistic, increases the generalization of the neural network. Our code and model are open source at https://github.com/BBillot/SynthSeg. △ Less

Submitted 8 April, 2021; v1 submitted 4 March, 2020; originally announced March 2020.

Comments: 19 pages, 5 figures

Journal ref: Proceedings of the Third Conference on Medical Imaging with Deep Learning (2020), vol.121, pp. 75-93

An 860 MHz Wireless Surface Acoustic Wave Sensor with a Metal-Organic Framework Sensing Layer for CO2 and CH4

Authors: Jagannath Devkota, David W. Greve, Tao Hong, Ki-Joong Kim, Paul R. Ohodnicki

Abstract: Wireless and passive surface acoustic wave (SAW) devices with nanoporous metal-organic framework (MOF) sensing layers are attractive gas sensors for applications in many fields such as energy industries and air pollution control. Here, we report on enhancing the sensitivity and detection limit of zeolitic imidazolate framework-8 (ZIF-8) MOF-coated SAW reflective delay line mass sensors by increasi… ▽ More Wireless and passive surface acoustic wave (SAW) devices with nanoporous metal-organic framework (MOF) sensing layers are attractive gas sensors for applications in many fields such as energy industries and air pollution control. Here, we report on enhancing the sensitivity and detection limit of zeolitic imidazolate framework-8 (ZIF-8) MOF-coated SAW reflective delay line mass sensors by increasing the operating frequency for sensitive detection of carbon dioxide (CO2) and methane (CH4) at ambient conditions. In particular, we show at least four times higher sensitivity of an 860 MHz (4-μm periodicity) SAW reflective delay line coated with a 240 nm thick ZIF-8 compared to the sensitivity of a 430 MHz (8-μm periodicity) otherwise identical sensor device to the targeted gases. The detection limits of the higher frequency wireless devices for CO2 and CH4 were estimated to be 0.91 vol-% and 7.01 vol-%, respectively. The enhanced sensitivity for higher frequency devices is explained in terms of the frequency dependent acoustic wave energy confinement. △ Less

Submitted 1 May, 2020; v1 submitted 9 December, 2019; originally announced February 2020.

Comments: 8 pages, accepted to publish in IEEE Sensors Journal

MSC Class: General; Electromagnetic Theory; Acoustics

Journal ref: IEEE Sensors Journal, 2020

PSACNN: Pulse Sequence Adaptive Fast Whole Brain Segmentation

Authors: Amod Jog, Andrew Hoopes, Douglas N. Greve, Koen Van Leemput, Bruce Fischl

Abstract: With the advent of convolutional neural networks~(CNN), supervised learning methods are increasingly being used for whole brain segmentation. However, a large, manually annotated training dataset of labeled brain images required to train such supervised methods is frequently difficult to obtain or create. In addition, existing training datasets are generally acquired with a homogeneous magnetic re… ▽ More With the advent of convolutional neural networks~(CNN), supervised learning methods are increasingly being used for whole brain segmentation. However, a large, manually annotated training dataset of labeled brain images required to train such supervised methods is frequently difficult to obtain or create. In addition, existing training datasets are generally acquired with a homogeneous magnetic resonance imaging~(MRI) acquisition protocol. CNNs trained on such datasets are unable to generalize on test data with different acquisition protocols. Modern neuroimaging studies and clinical trials are necessarily multi-center initiatives with a wide variety of acquisition protocols. Despite stringent protocol harmonization practices, it is very difficult to standardize the gamut of MRI imaging parameters across scanners, field strengths, receive coils etc., that affect image contrast. In this paper we propose a CNN-based segmentation algorithm that, in addition to being highly accurate and fast, is also resilient to variation in the input acquisition. Our approach relies on building approximate forward models of pulse sequences that produce a typical test image. For a given pulse sequence, we use its forward model to generate plausible, synthetic training examples that appear as if they were acquired in a scanner with that pulse sequence. Sampling over a wide variety of pulse sequences results in a wide variety of augmented training examples that help build an image contrast invariant model. Our method trains a single CNN that can segment input MRI images with acquisition parameters as disparate as $T_1$-weighted and $T_2$-weighted contrasts with only $T_1$-weighted training data. The segmentations generated are highly accurate with state-of-the-art results~(overall Dice overlap$=0.94$), with a fast run time~($\approx$ 45 seconds), and consistent across a wide range of acquisition protocols. △ Less

Submitted 1 March, 2019; v1 submitted 17 January, 2019; originally announced January 2019.

Comments: Typo in author name corrected. Greves -> Greve

Trapezoidal Generalization over Linear Constraints

Authors: David Greve, Andrew Gacek

Abstract: We are developing a model-based fuzzing framework that employs mathematical models of system behavior to guide the fuzzing process. Whereas traditional fuzzing frameworks generate tests randomly, a model-based framework can deduce tests from a behavioral model using a constraint solver. Because the state space being explored by the fuzzer is often large, the rapid generation of test vectors is cr… ▽ More We are developing a model-based fuzzing framework that employs mathematical models of system behavior to guide the fuzzing process. Whereas traditional fuzzing frameworks generate tests randomly, a model-based framework can deduce tests from a behavioral model using a constraint solver. Because the state space being explored by the fuzzer is often large, the rapid generation of test vectors is crucial. The need to generate tests quickly, however, is antithetical to the use of a constraint solver. Our solution to this problem is to use the constraint solver to generate an initial solution, to generalize that solution relative to the system model, and then to perform rapid, repeated, randomized sampling of the generalized solution space to generate fuzzing tests. Crucial to the success of this endeavor is a generalization procedure with reasonable size and performance costs that produces generalized solution spaces that can be sampled efficiently. This paper describes a generalization technique for logical formulae expressed in terms of Boolean combinations of linear constraints that meets the unique performance requirements of model-based fuzzing. The technique represents generalizations using trapezoidal solution sets consisting of ordered, hierarchical conjunctions of linear constraints that are more expressive than simple intervals but are more efficient to manipulate and sample than generic polytopes. Supporting materials contain an ACL2 proof that verifies the correctness of a low-level implementation of the generalization algorithm against a specification of generalization correctness. Finally a post-processing procedure is described that results in a restricted trapezoidal solution that can be sampled (solved) rapidly and efficiently without backtracking, even for integer domains. While informal correctness arguments are provided, a formal proof of the correctness of the restriction algorithm remains as future work. △ Less

Submitted 9 October, 2018; originally announced October 2018.

Comments: In Proceedings ACL2 2018, arXiv:1810.03762

Journal ref: EPTCS 280, 2018, pp. 30-46

A probabilistic atlas of the human thalamic nuclei combining ex vivo MRI and histology

Authors: Juan Eugenio Iglesias, Ricardo Insausti, Garikoitz Lerma-Usabiaga, Martina Bocchetta, Koen Van Leemput, Douglas N Greve, Andre van der Kouwe, Bruce Fischl, Cesar Caballero-Gaudes, Pedro M Paz-Alonso

Abstract: The human thalamus is a brain structure that comprises numerous, highly specific nuclei. Since these nuclei are known to have different functions and to be connected to different areas of the cerebral cortex, it is of great interest for the neuroimaging community to study their volume, shape and connectivity in vivo with MRI. In this study, we present a probabilistic atlas of the thalamic nuclei b… ▽ More The human thalamus is a brain structure that comprises numerous, highly specific nuclei. Since these nuclei are known to have different functions and to be connected to different areas of the cerebral cortex, it is of great interest for the neuroimaging community to study their volume, shape and connectivity in vivo with MRI. In this study, we present a probabilistic atlas of the thalamic nuclei built using ex vivo brain MRI scans and histological data, as well as the application of the atlas to in vivo MRI segmentation. The atlas was built using manual delineation of 26 thalamic nuclei on the serial histology of 12 whole thalami from six autopsy samples, combined with manual segmentations of the whole thalamus and surrounding structures (caudate, putamen, hippocampus, etc.) made on in vivo brain MR data from 39 subjects. The 3D structure of the histological data and corresponding manual segmentations was recovered using the ex vivo MRI as reference frame, and stacks of blockface photographs acquired during the sectioning as intermediate target. The atlas, which was encoded as an adaptive tetrahedral mesh, shows a good agreement with with previous histological studies of the thalamus in terms of volumes of representative nuclei. When applied to segmentation of in vivo scans using Bayesian inference, the atlas shows excellent test-retest reliability, robustness to changes in input MRI contrast, and ability to detect differential thalamic effects in subjects with Alzheimer's disease. The probabilistic atlas and companion segmentation tool are publicly available as part of the neuroimaging package FreeSurfer. △ Less

Submitted 22 June, 2018; originally announced June 2018.

Kinetic Compressive Sensing

Authors: Michele Scipioni, Maria F. Santarelli, Luigi Landini, Ciprian Catana, Douglas N. Greve, Julie C. Price, Stefano Pedemonte

Abstract: Parametric images provide insight into the spatial distribution of physiological parameters, but they are often extremely noisy, due to low SNR of tomographic data. Direct estimation from projections allows accurate noise modeling, improving the results of post-reconstruction fitting. We propose a method, which we name kinetic compressive sensing (KCS), based on a hierarchical Bayesian model and o… ▽ More Parametric images provide insight into the spatial distribution of physiological parameters, but they are often extremely noisy, due to low SNR of tomographic data. Direct estimation from projections allows accurate noise modeling, improving the results of post-reconstruction fitting. We propose a method, which we name kinetic compressive sensing (KCS), based on a hierarchical Bayesian model and on a novel reconstruction algorithm, that encodes sparsity of kinetic parameters. Parametric maps are reconstructed by maximizing the joint probability, with an Iterated Conditional Modes (ICM) approach, alternating the optimization of activity time series (OS-MAP-OSL), and kinetic parameters (MAP-LM). We evaluated the proposed algorithm on a simulated dynamic phantom: a bias/variance study confirmed how direct estimates can improve the quality of parametric maps over a post-reconstruction fitting, and showed how the novel sparsity prior can further reduce their variance, without affecting bias. Real FDG PET human brain data (Siemens mMR, 40min) images were also processed. Results enforced how the proposed KCS-regularized direct method can produce spatially coherent images and parametric maps, with lower spatial noise and better tissue contrast. A GPU-based open source implementation of the algorithm is provided. △ Less

Submitted 27 March, 2018; originally announced March 2018.

Comments: 5 pages, 6 figures, Submitted to the Conference Record of "IEEE Nuclear Science Symposium and Medical Imaging Conference (IEEE NSS-MIC) 2017"

Zeolitic imidazolate framework-coated acoustic sensors for room temperature detection of carbon dioxide and methane

Authors: Jagannath Devkota, Ki-Joong Kim, Paul R. Ohodnicki, Jeffrey T. Culp, David W. Greve, Jonathan W. Lekse

Abstract: Integration of nanoporous materials such as metal organic frameworks (MOFs) with sensitive transducers can result robust sensing platforms for monitoring gases and chemical vapors for a range of applications. Here, we report on an integration of the zeolitic imidazolate framework-8 (ZIF-8) MOF with surface acoustic wave (SAW) and thickness shear mode quartz crystal microbalance (QCM) devices to mo… ▽ More Integration of nanoporous materials such as metal organic frameworks (MOFs) with sensitive transducers can result robust sensing platforms for monitoring gases and chemical vapors for a range of applications. Here, we report on an integration of the zeolitic imidazolate framework-8 (ZIF-8) MOF with surface acoustic wave (SAW) and thickness shear mode quartz crystal microbalance (QCM) devices to monitor carbon dioxide(CO2)and methane (CH4) at ambient conditions. The MOF was directly coated on the custom fabricated Y-Z LiNbO3 SAW delay lines (operating frequency,f0 = 436 MHz)and AT-cut Quartz TSM resonators (resonant frequency, f0 = 9 MHz) and the devices were tested for various gases in N2 at ambient condition. The devices were able to detect the changes in CO2 or CH4 concentrations with relatively higher sensitivity to CO2, which was due to its higher adsorption potential and heavier molecular weight. The sensors showed full reversibility and repeatability which were attributed to the physisorption of the gases into the MOF and high stability of the devices. Both types of the sensors showed linear responses relative to changes in the binary gas compositions thereby allowing to construct calibration curves which correlated well with the expected mass changes in the sorbent layer based on mixed-gas gravimetric adsorption isotherms measured on bulk samples.For 200 nm thick films, the SAW sensitivity to CO2 and CH4 were 1.44x10^-6/vol-%, respectivel yagainst the QCM sensitivities 0.24x10^-6/vol-% and 1x10^-8/vol-%,respectively which were evaluated as the fractional change in the signal. The SAW sensors were also evaluated for 100 nm - 300 nm thick films, the sensitivities of which were found to increase with the thickness due to the increased number of pores for adsorption of larger amount of gases. Also, the SAW devices had a good wireless response for detecting gases remotely. △ Less

Submitted 18 April, 2018; v1 submitted 22 December, 2017; originally announced December 2017.

Comments: 32 pages (double spacing), 10 figures, 2 tables, regular paper accepted to publish in Nanoscale for publication

MSC Class: 78-05

Development of a Translator from LLVM to ACL2

Authors: David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg

Abstract: In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystems whose top-level assurance relies on the assurance of the individual components. We have thus undertaken a project to build a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem p… ▽ More In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystems whose top-level assurance relies on the assurance of the individual components. We have thus undertaken a project to build a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover. Our translator produces executable ACL2 formal models, allowing us to both prove theorems about the translated models as well as validate those models by testing. The resulting models can be translated and certified without user intervention, even for code with loops, thanks to the use of the def::ung macro which allows us to defer the question of termination. Initial measurements of concrete execution for translated LLVM functions indicate that performance is nearly 2.4 million LLVM instructions per second on a typical laptop computer. In this paper we overview the translation process and illustrate the translator's capabilities by way of a concrete example, including both a functional correctness theorem as well as a validation test for that example. △ Less

Submitted 5 June, 2014; originally announced June 2014.

Comments: In Proceedings ACL2 2014, arXiv:1406.1238

ACM Class: F.3.1; F.4.1

Journal ref: EPTCS 152, 2014, pp. 163-177

A Step-Indexing Approach to Partial Functions

Authors: David Greve, Konrad Slind

Abstract: We describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL2 and they provide little, if any, support for executing the resulting definitions. We use step-inde… ▽ More We describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL2 and they provide little, if any, support for executing the resulting definitions. We use step-indexing as the underlying implementation technology, enabling the definitions to be carried out in first order logic. We also show how recent enhancements to ACL2's guard feature can be used to enable the efficient execution of partial recursive functions. △ Less

Submitted 30 April, 2013; originally announced April 2013.

Comments: In Proceedings ACL2 2013, arXiv:1304.7123

Journal ref: EPTCS 114, 2013, pp. 42-53