-
HMTRace: Hardware-Assisted Memory-Tagging based Dynamic Data Race Detection
Authors:
Jaidev Shastri,
Xiaoguang Wang,
Basavesh Ammanaghatta Shivakumar,
Freek Verbeek,
Binoy Ravindran
Abstract:
Data race, a category of insidious software concurrency bugs, is often challenging and resource-intensive to detect and debug. Existing dynamic race detection tools incur significant execution time and memory overhead while exhibiting high false positives. This paper proposes HMTRace, a novel Armv8.5-A memory tag extension (MTE) based dynamic data race detection framework, emphasizing low compute…
▽ More
Data race, a category of insidious software concurrency bugs, is often challenging and resource-intensive to detect and debug. Existing dynamic race detection tools incur significant execution time and memory overhead while exhibiting high false positives. This paper proposes HMTRace, a novel Armv8.5-A memory tag extension (MTE) based dynamic data race detection framework, emphasizing low compute and memory requirements while maintaining high accuracy and precision. HMTRace supports race detection in userspace OpenMP- and Pthread-based multi-threaded C applications. HMTRace showcases a combined f1-score of 0.86 while incurring a mean execution time overhead of 4.01% and peak memory (RSS) overhead of 54.31%. HMTRace also does not report false positives, asserting all reported races.
△ Less
Submitted 29 April, 2024;
originally announced April 2024.
-
Advances in Kidney Biopsy Lesion Assessment through Dense Instance Segmentation
Authors:
Zhan Xiong,
Junling He,
Pieter Valkema,
Tri Q. Nguyen,
Maarten Naesens,
Jesper Kers,
Fons J. Verbeek
Abstract:
Renal biopsies are the gold standard for diagnosis of kidney diseases. Lesion scores made by renal pathologists are semi-quantitative and exhibit high inter-observer variability. Automating lesion classification within segmented anatomical structures can provide decision support in quantification analysis and reduce the inter-observer variability. Nevertheless, classifying lesions in regions-of-in…
▽ More
Renal biopsies are the gold standard for diagnosis of kidney diseases. Lesion scores made by renal pathologists are semi-quantitative and exhibit high inter-observer variability. Automating lesion classification within segmented anatomical structures can provide decision support in quantification analysis and reduce the inter-observer variability. Nevertheless, classifying lesions in regions-of-interest (ROIs) is clinically challenging due to (a) a large amount of densely packed anatomical objects (up to 1000), (b) class imbalance across different compartments (at least 3), (c) significant variation in object scales (i.e. sizes and shapes), and (d) the presence of multi-label lesions per anatomical structure. Existing models lack the capacity to address these complexities efficiently and generically. This paper presents \textbf{a generalized technical solution} for large-scale, multi-source datasets with diverse lesions. Our approach utilizes two sub-networks: dense instance segmentation and lesion classification. We introduce \textbf{DiffRegFormer}, an end-to-end dense instance segmentation model designed for multi-class, multi-scale objects within ROIs. Combining diffusion models, transformers, and RCNNs, DiffRegFormer efficiently recognizes over 500 objects across three anatomical classes (glomeruli, tubuli, arteries) within ROIs on a single NVIDIA GeForce RTX 3090 GPU. On a dataset of 303 ROIs (from 148 Jones' silver-stained renal WSIs), it outperforms state of art models, achieving AP of 52.1\% (detection) and 46.8\% (segmentation). Our lesion classification sub-network achieves 89.2\% precision and 64.6\% recall on 21889 object patches (from the 303 ROIs). Importantly, the model demonstrates direct domain transfer to PAS-stained WSIs without fine-tuning.
△ Less
Submitted 28 March, 2024; v1 submitted 29 September, 2023;
originally announced September 2023.
-
Anomalous NO2 emitting ship detection with TROPOMI satellite data and machine learning
Authors:
Solomiia Kurchaba,
Jasper van Vliet,
Fons J. Verbeek,
Cor J. Veenman
Abstract:
Starting from 2021, more demanding $\text{NO}_\text{x}$ emission restrictions were introduced for ships operating in the North and Baltic Sea waters. Since all methods currently used for ship compliance monitoring are financially and time demanding, it is important to prioritize the inspection of ships that have high chances of being non-compliant. The current state-of-the-art approach for a large…
▽ More
Starting from 2021, more demanding $\text{NO}_\text{x}$ emission restrictions were introduced for ships operating in the North and Baltic Sea waters. Since all methods currently used for ship compliance monitoring are financially and time demanding, it is important to prioritize the inspection of ships that have high chances of being non-compliant. The current state-of-the-art approach for a large-scale ship $\text{NO}_\text{2}$ estimation is a supervised machine learning-based segmentation of ship plumes on TROPOMI/S5P images. However, challenging data annotation and insufficiently complex ship emission proxy used for the validation limit the applicability of the model for ship compliance monitoring. In this study, we present a method for the automated selection of potentially non-compliant ships using a combination of machine learning models on TROPOMI satellite data. It is based on a proposed regression model predicting the amount of $\text{NO}_\text{2}$ that is expected to be produced by a ship with certain properties operating in the given atmospheric conditions. The model does not require manual labeling and is validated with TROPOMI data directly. The differences between the predicted and actual amount of produced $\text{NO}_\text{2}$ are integrated over observations of the ship in time and are used as a measure of the inspection worthiness of a ship. To assure the robustness of the results, we compare the obtained results with the results of the previously developed segmentation-based method. Ships that are also highly deviating in accordance with the segmentation method require further attention. If no other explanations can be found by checking the TROPOMI data, the respective ships are advised to be the candidates for inspection.
△ Less
Submitted 7 April, 2023; v1 submitted 24 February, 2023;
originally announced February 2023.
-
Reachability Logic for Low-Level Programs
Authors:
Nico Naus,
Freek Verbeek,
Marc Schoolderman,
Binoy Ravindran
Abstract:
Automatic exploit generation is a relatively new area of research. Work in this area aims to automate the manual and labor intensive task of finding exploits in software. In this paper we present a novel program logic to support automatic exploit generation. We develop a program logic called Reachability Logic, which formally defines the relation between reachability of an assertion and the precon…
▽ More
Automatic exploit generation is a relatively new area of research. Work in this area aims to automate the manual and labor intensive task of finding exploits in software. In this paper we present a novel program logic to support automatic exploit generation. We develop a program logic called Reachability Logic, which formally defines the relation between reachability of an assertion and the preconditions which allow them to occur. This relation is then used to calculate the search space of preconditions. We show that Reachability Logic is a powerful tool in automatically finding evidence that an assertion is reachable. We verify that the system works for small litmus tests, as well as real-world algorithms. An implementation has been developed, and the entire system is proven to be sound and complete in a theorem prover. This work represents an important step towards formally verified automatic exploit generation.
△ Less
Submitted 31 March, 2022;
originally announced April 2022.
-
Supervised segmentation of NO2 plumes from individual ships using TROPOMI satellite data
Authors:
Solomiia Kurchaba,
Jasper van Vliet,
Fons J. Verbeek,
Jacqueline J. Meulman,
Cor J. Veenman
Abstract:
The ship** industry is one of the strongest anthropogenic emitters of $\text{NO}_\text{x}$ -- substance harmful both to human health and the environment. The rapid growth of the industry causes societal pressure on controlling the emission levels produced by ships. All the methods currently used for ship emission monitoring are costly and require proximity to a ship, which makes global and conti…
▽ More
The ship** industry is one of the strongest anthropogenic emitters of $\text{NO}_\text{x}$ -- substance harmful both to human health and the environment. The rapid growth of the industry causes societal pressure on controlling the emission levels produced by ships. All the methods currently used for ship emission monitoring are costly and require proximity to a ship, which makes global and continuous emission monitoring impossible. A promising approach is the application of remote sensing. Studies showed that some of the $\text{NO}_\text{2}$ plumes from individual ships can visually be distinguished using the TROPOspheric Monitoring Instrument on board the Copernicus Sentinel 5 Precursor (TROPOMI/S5P). To deploy a remote sensing-based global emission monitoring system, an automated procedure for the estimation of $\text{NO}_\text{2}$ emissions from individual ships is needed. The extremely low signal-to-noise ratio of the available data as well as the absence of ground truth makes the task very challenging. Here, we present a methodology for the automated segmentation of $\text{NO}_\text{2}$ plumes produced by seagoing ships using supervised machine learning on TROPOMI/S5P data. We show that the proposed approach leads to a more than a 20\% increase in the average precision score in comparison to the methods used in previous studies and results in a high correlation of 0.834 with the theoretically derived ship emission proxy. This work is a crucial step toward the development of an automated procedure for global ship emission monitoring using remote sensing data.
△ Less
Submitted 7 April, 2023; v1 submitted 14 March, 2022;
originally announced March 2022.
-
Joint Registration and Segmentation via Multi-Task Learning for Adaptive Radiotherapy of Prostate Cancer
Authors:
Mohamed S. Elmahdy,
Laurens Beljaards,
Sahar Yousefi,
Hessam Sokooti,
Fons Verbeek,
U. A. van der Heide,
Marius Staring
Abstract:
Medical image registration and segmentation are two of the most frequent tasks in medical image analysis. As these tasks are complementary and correlated, it would be beneficial to apply them simultaneously in a joint manner. In this paper, we formulate registration and segmentation as a joint problem via a Multi-Task Learning (MTL) setting, allowing these tasks to leverage their strengths and mit…
▽ More
Medical image registration and segmentation are two of the most frequent tasks in medical image analysis. As these tasks are complementary and correlated, it would be beneficial to apply them simultaneously in a joint manner. In this paper, we formulate registration and segmentation as a joint problem via a Multi-Task Learning (MTL) setting, allowing these tasks to leverage their strengths and mitigate their weaknesses through the sharing of beneficial information. We propose to merge these tasks not only on the loss level, but on the architectural level as well. We studied this approach in the context of adaptive image-guided radiotherapy for prostate cancer, where planning and follow-up CT images as well as their corresponding contours are available for training. The study involves two datasets from different manufacturers and institutes. The first dataset was divided into training (12 patients) and validation (6 patients), and was used to optimize and validate the methodology, while the second dataset (14 patients) was used as an independent test set. We carried out an extensive quantitative comparison between the quality of the automatically generated contours from different network architectures as well as loss weighting methods. Moreover, we evaluated the quality of the generated deformation vector field (DVF). We show that MTL algorithms outperform their Single-Task Learning (STL) counterparts and achieve better generalization on the independent test set. The best algorithm achieved a mean surface distance of $1.06 \pm 0.3$ mm, $1.27 \pm 0.4$ mm, $0.91 \pm 0.4$ mm, and $1.76 \pm 0.8$ mm on the validation set for the prostate, seminal vesicles, bladder, and rectum, respectively. The high accuracy of the proposed method combined with the fast inference speed, makes it a promising method for automatic re-contouring of follow-up scans for adaptive radiotherapy.
△ Less
Submitted 4 May, 2021;
originally announced May 2021.
-
A Cross-Stitch Architecture for Joint Registration and Segmentation in Adaptive Radiotherapy
Authors:
Laurens Beljaards,
Mohamed S. Elmahdy,
Fons Verbeek,
Marius Staring
Abstract:
Recently, joint registration and segmentation has been formulated in a deep learning setting, by the definition of joint loss functions. In this work, we investigate joining these tasks at the architectural level. We propose a registration network that integrates segmentation propagation between images, and a segmentation network to predict the segmentation directly. These networks are connected i…
▽ More
Recently, joint registration and segmentation has been formulated in a deep learning setting, by the definition of joint loss functions. In this work, we investigate joining these tasks at the architectural level. We propose a registration network that integrates segmentation propagation between images, and a segmentation network to predict the segmentation directly. These networks are connected into a single joint architecture via so-called cross-stitch units, allowing information to be exchanged between the tasks in a learnable manner. The proposed method is evaluated in the context of adaptive image-guided radiotherapy, using daily prostate CT imaging. Two datasets from different institutes and manufacturers were involved in the study. The first dataset was used for training (12 patients) and validation (6 patients), while the second dataset was used as an independent test set (14 patients). In terms of mean surface distance, our approach achieved $1.06 \pm 0.3$ mm, $0.91 \pm 0.4$ mm, $1.27 \pm 0.4$ mm, and $1.76 \pm 0.8$ mm on the validation set and $1.82 \pm 2.4$ mm, $2.45 \pm 2.4$ mm, $2.45 \pm 5.0$ mm, and $2.57 \pm 2.3$ mm on the test set for the prostate, bladder, seminal vesicles, and rectum, respectively. The proposed multi-task network outperformed single-task networks, as well as a network only joined through the loss function, thus demonstrating the capability to leverage the individual strengths of the segmentation and registration tasks. The obtained performance as well as the inference speed make this a promising candidate for daily re-contouring in adaptive radiotherapy, potentially reducing treatment-related side effects and improving quality-of-life after treatment.
△ Less
Submitted 17 April, 2020;
originally announced April 2020.
-
Probabilistic Inference for Camera Calibration in Light Microscopy under Circular Motion
Authors:
Yuanhao Guo,
Fons J. Verbeek,
Ge Yang
Abstract:
Robust and accurate camera calibration is essential for 3D reconstruction in light microscopy under circular motion. Conventional methods require either accurate key point matching or precise segmentation of the axial-view images. Both remain challenging because specimens often exhibit transparency/translucency in a light microscope. To address those issues, we propose a probabilistic inference ba…
▽ More
Robust and accurate camera calibration is essential for 3D reconstruction in light microscopy under circular motion. Conventional methods require either accurate key point matching or precise segmentation of the axial-view images. Both remain challenging because specimens often exhibit transparency/translucency in a light microscope. To address those issues, we propose a probabilistic inference based method for the camera calibration that does not require sophisticated image pre-processing. Based on 3D projective geometry, our method assigns a probability on each of a range of voxels that cover the whole object. The probability indicates the likelihood of a voxel belonging to the object to be reconstructed. Our method maximizes a joint probability that distinguishes the object from the background. Experimental results show that the proposed method can accurately recover camera configurations in both light microscopy and natural scene imaging. Furthermore, the method can be used to produce high-fidelity 3D reconstructions and accurate 3D measurements.
△ Less
Submitted 30 October, 2019;
originally announced October 2019.
-
A benchmark for C program verification
Authors:
Marko van Eekelen,
Daniil Frumin,
Herman Geuvers,
Léon Gondelman,
Robbert Krebbers,
Marc Schoolderman,
Sjaak Smetsers,
Freek Verbeek,
Benoît Viguier,
Freek Wiedijk
Abstract:
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last purpose, we give a scoring formula that allows a verification system to score up to a hundred points.
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last purpose, we give a scoring formula that allows a verification system to score up to a hundred points.
△ Less
Submitted 1 April, 2019;
originally announced April 2019.
-
Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications
Authors:
Freek Verbeek,
Julien Schmaltz
Abstract:
This volume contains the proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2'14, a two-day workshop held in Vienna, Austria, on July 12-13, 2014. ACL2 workshops occur at approximately 18-month intervals and provide a major technical forum for researchers to present and discuss improvements and extensions to the theorem prover, comparisons of ACL2…
▽ More
This volume contains the proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2'14, a two-day workshop held in Vienna, Austria, on July 12-13, 2014. ACL2 workshops occur at approximately 18-month intervals and provide a major technical forum for researchers to present and discuss improvements and extensions to the theorem prover, comparisons of ACL2 with other systems, and applications of ACL2 in formal verification. These proceedings include 13 peer reviewed technical papers.
ACL2 is a state-of-the-art automated reasoning system that has been successfully applied in academia, government, and industry for specification and verification of computing systems and in teaching computer science courses. In 2005, Boyer, Kaufmann, and Moore were awarded the 2005 ACM Software System Award for their work in ACL2 and the other theorem provers in the Boyer-Moore family.
△ Less
Submitted 4 June, 2014;
originally announced June 2014.
-
Verification of Building Blocks for Asynchronous Circuits
Authors:
Freek Verbeek,
Julien Schmaltz
Abstract:
Scalable formal verification constitutes an important challenge for the design of asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We present our approach to using ACL2 to verify necessary and sufficient conditions over asynchronous delay-insensitive primitives. These conditions are used to…
▽ More
Scalable formal verification constitutes an important challenge for the design of asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We present our approach to using ACL2 to verify necessary and sufficient conditions over asynchronous delay-insensitive primitives. These conditions are used to derive SAT/SMT instances from circuits built out of these primitives. These SAT/SMT instances help in establishing absence of deadlocks. Our verification effort consists of building an executable checker in the ACL2 logic tailored for our purpose. We prove that this checker is correct. This approach enables us to prove ACL2 theorems involving defun-sk constructs and free variables fully automatically.
△ Less
Submitted 30 April, 2013;
originally announced April 2013.
-
Formal verification of a deadlock detection algorithm
Authors:
Freek Verbeek,
Julien Schmaltz
Abstract:
Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with wormhole switching. The algorithm has been specified and proven correct in ACL2. To enable a top-down proof methodology, some parts of the algorithm have been left unimplemented. For these parts, the ACL2 specification co…
▽ More
Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with wormhole switching. The algorithm has been specified and proven correct in ACL2. To enable a top-down proof methodology, some parts of the algorithm have been left unimplemented. For these parts, the ACL2 specification contains constrained functions introduced with defun-sk. We used single-threaded objects to represent the data structures used by the algorithm. In this paper, we present details on the proof of correctness of the algorithm. The process of formal verification was crucial to get the algorithm flawless. Our ultimate objective is to have an efficient executable, and formally proven correct implementation of the algorithm running in ACL2.
△ Less
Submitted 20 October, 2011;
originally announced October 2011.
-
Creating a new Ontology: a Modular Approach
Authors:
Julia Dmitrieva,
Fons J. Verbeek
Abstract:
Creating a new Ontology: a Modular Approach
Creating a new Ontology: a Modular Approach
△ Less
Submitted 7 December, 2010;
originally announced December 2010.
