Showing 1–17 of 17 results for author: Matos, J

EHRmonize: A Framework for Medical Concept Abstraction from Electronic Health Records using Large Language Models

Authors: João Matos, Jack Gallifant, Jian Pei, A. Ian Wong

Abstract: Electronic health records (EHRs) contain vast amounts of complex data, but harmonizing and processing this information remains a challenging and costly task requiring significant clinical expertise. While large language models (LLMs) have shown promise in various healthcare applications, their potential for abstracting medical concepts from EHRs remains largely unexplored. We introduce EHRmonize,… ▽ More Electronic health records (EHRs) contain vast amounts of complex data, but harmonizing and processing this information remains a challenging and costly task requiring significant clinical expertise. While large language models (LLMs) have shown promise in various healthcare applications, their potential for abstracting medical concepts from EHRs remains largely unexplored. We introduce EHRmonize, a framework leveraging LLMs to abstract medical concepts from EHR data. Our study uses medication data from two real-world EHR databases to evaluate five LLMs on two free-text extraction and six binary classification tasks across various prompting strategies. GPT-4o's with 10-shot prompting achieved the highest performance in all tasks, accompanied by Claude-3.5-Sonnet in a subset of tasks. GPT-4o achieved an accuracy of 97% in identifying generic route names, 82% for generic drug names, and 100% in performing binary classification of antibiotics. While EHRmonize significantly enhances efficiency, reducing annotation time by an estimated 60%, we emphasize that clinician oversight remains essential. Our framework, available as a Python package, offers a promising tool to assist clinicians in EHR data abstraction, potentially accelerating healthcare research and improving data harmonization processes. △ Less

Submitted 28 June, 2024; originally announced July 2024.

Comments: submitted for review, total of 10 pages

Analyzing Diversity in Healthcare LLM Research: A Scientometric Perspective

Authors: David Restrepo, Chenwei Wu, Constanza Vásquez-Venegas, João Matos, Jack Gallifant, Luis Filipe

Abstract: The deployment of large language models (LLMs) in healthcare has demonstrated substantial potential for enhancing clinical decision-making, administrative efficiency, and patient outcomes. However, the underrepresentation of diverse groups in the development and application of these models can perpetuate biases, leading to inequitable healthcare delivery. This paper presents a comprehensive scient… ▽ More The deployment of large language models (LLMs) in healthcare has demonstrated substantial potential for enhancing clinical decision-making, administrative efficiency, and patient outcomes. However, the underrepresentation of diverse groups in the development and application of these models can perpetuate biases, leading to inequitable healthcare delivery. This paper presents a comprehensive scientometric analysis of LLM research for healthcare, including data from January 1, 2021, to June 16, 2024. By analyzing metadata from PubMed and Dimensions, including author affiliations, countries, and funding sources, we assess the diversity of contributors to LLM research. Our findings highlight significant gender and geographic disparities, with a predominance of male authors and contributions primarily from high-income countries (HICs). We introduce a novel journal diversity index based on Gini impurity to measure the inclusiveness of scientific publications. Our results underscore the necessity for greater representation in order to ensure the equitable application of LLMs in healthcare. We propose actionable strategies to enhance diversity and inclusivity in artificial intelligence research, with the ultimate goal of fostering a more inclusive and equitable future in healthcare innovation. △ Less

Submitted 18 June, 2024; originally announced June 2024.

Unmasking Biases and Navigating Pitfalls in the Ophthalmic Artificial Intelligence Lifecycle: A Review

Authors: Luis Filipe Nakayama, João Matos, Justin Quion, Frederico Novaes, William Greig Mitchell, Rogers Mwavu, Ju-Yi Ji Hung, Alvina Pauline dy Santiago, Warachaya Phanphruk, Jaime S. Cardoso, Leo Anthony Celi

Abstract: Over the past two decades, exponential growth in data availability, computational power, and newly available modeling techniques has led to an expansion in interest, investment, and research in Artificial Intelligence (AI) applications. Ophthalmology is one of many fields that seek to benefit from AI given the advent of telemedicine screening programs and the use of ancillary imaging. However, bef… ▽ More Over the past two decades, exponential growth in data availability, computational power, and newly available modeling techniques has led to an expansion in interest, investment, and research in Artificial Intelligence (AI) applications. Ophthalmology is one of many fields that seek to benefit from AI given the advent of telemedicine screening programs and the use of ancillary imaging. However, before AI can be widely deployed, further work must be done to avoid the pitfalls within the AI lifecycle. This review article breaks down the AI lifecycle into seven steps: data collection; defining the model task; data pre-processing and labeling; model development; model evaluation and validation; deployment; and finally, post-deployment evaluation, monitoring, and system recalibration and delves into the risks for harm at each step and strategies for mitigating them. △ Less

Submitted 7 October, 2023; originally announced October 2023.

Sound Atomicity Inference for Data-Centric Synchronization

Authors: Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, António Ravara

Abstract: Data-Centric Concurrency Control (DCCC) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCCC is hindered by the fact that it may require many annotations and/or multiple implementations of… ▽ More Data-Centric Concurrency Control (DCCC) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCCC is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters. Moreover, the existing DCCC solutions do not address the use of interfaces, precluding their use in most object-oriented programs. To overcome these limitations, in this paper we present AtomiS, a new DCCC model based on a rigorously defined type-sound programming language. Programming with AtomiS requires only (atomic)-qualifying types of parameters and return values in interface definitions, and of fields in class definitions. From this atomicity specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives, by means of the desired automatic technique and associated atomicity and deadlock-freedom guarantees, which can be plugged-into the model's pipeline. We present the foundations for the AtomiS analysis and synthesis, with formal guarantees that the generated program is well-typed and that it corresponds behaviourally to the original one. The proofs are mechanised in Coq. We also provide a Java implementation that showcases the applicability of AtomiS in real-life programs. △ Less

Submitted 11 September, 2023; originally announced September 2023.

Evaluating AI systems under uncertain ground truth: a case study in dermatology

Authors: David Stutz, Ali Taylan Cemgil, Abhijit Guha Roy, Tatiana Matejovicova, Melih Barsbey, Patricia Strachan, Mike Schaekermann, Jan Freyberg, Rajeev Rikhye, Beverly Freeman, Javier Perez Matos, Umesh Telang, Dale R. Webster, Yuan Liu, Greg S. Corrado, Yossi Matias, Pushmeet Kohli, Yun Liu, Arnaud Doucet, Alan Karthikesalingam

Abstract: For safety, AI systems in health undergo thorough evaluations before deployment, validating their predictions against a ground truth that is assumed certain. However, this is actually not the case and the ground truth may be uncertain. Unfortunately, this is largely ignored in standard evaluation of AI models but can have severe consequences such as overestimating the future performance. To avoid… ▽ More For safety, AI systems in health undergo thorough evaluations before deployment, validating their predictions against a ground truth that is assumed certain. However, this is actually not the case and the ground truth may be uncertain. Unfortunately, this is largely ignored in standard evaluation of AI models but can have severe consequences such as overestimating the future performance. To avoid this, we measure the effects of ground truth uncertainty, which we assume decomposes into two main components: annotation uncertainty which stems from the lack of reliable annotations, and inherent uncertainty due to limited observational information. This ground truth uncertainty is ignored when estimating the ground truth by deterministically aggregating annotations, e.g., by majority voting or averaging. In contrast, we propose a framework where aggregation is done using a statistical model. Specifically, we frame aggregation of annotations as posterior inference of so-called plausibilities, representing distributions over classes in a classification setting, subject to a hyper-parameter encoding annotator reliability. Based on this model, we propose a metric for measuring annotation uncertainty and provide uncertainty-adjusted metrics for performance evaluation. We present a case study applying our framework to skin condition classification from images where annotations are provided in the form of differential diagnoses. The deterministic adjudication process called inverse rank normalization (IRN) from previous work ignores ground truth uncertainty in evaluation. Instead, we present two alternative statistical models: a probabilistic version of IRN and a Plackett-Luce-based model. We find that a large portion of the dataset exhibits significant ground truth uncertainty and standard IRN-based evaluation severely over-estimates performance without providing uncertainty estimates. △ Less

Submitted 5 July, 2023; originally announced July 2023.

Bio-inspired Algorithms in the Optimisation of Wireless Sensor Networks

Authors: Joana Matos, Carine M. Rebello, Erbet A. Costa, Luana P. Queiroz, Maria Joao B. Regufe, Idelfonso B. R. Nogueira

Abstract: WSN are a growing technology in industrial and personal use fields. The Quality of Service (QoS) of WSN is associated to the architecture of WSN nodes and network design. In this work, the composition of the nodes and network is analysed. The success of WSN is related to the maximisation of the lifetime and coverage of the device, allied to the minimisation of energy consumption and number of node… ▽ More WSN are a growing technology in industrial and personal use fields. The Quality of Service (QoS) of WSN is associated to the architecture of WSN nodes and network design. In this work, the composition of the nodes and network is analysed. The success of WSN is related to the maximisation of the lifetime and coverage of the device, allied to the minimisation of energy consumption and number of nodes, guaranteeing a good network connectivity and high transmission. The most common WSN issues are presented and reviewed. The most suitable optimisation technique is Multi-objective (MOO) which is exemplified in this work from complex multi-objective functions which include several WSN problems. The second part of this review focus on bio-inspired algorithms in WSN optimisation: Genetic Algorithms (GA), Particles Swarm Optimisation (PSO) and Ant Colony Optimisation (ACO). Other less common methods are also present and related to WSN issues. △ Less

Submitted 23 April, 2023; v1 submitted 10 October, 2022; originally announced October 2022.

Comments: We will not continue this research

CEG4N: Counter-Example Guided Neural Network Quantization Refinement

Authors: João Batista P. Matos Jr., Iury Bessa, Edoardo Manino, Xidan Song, Lucas C. Cordeiro

Abstract: Neural networks are essential components of learning-based software systems. However, their high compute, memory, and power requirements make using them in low resources domains challenging. For this reason, neural networks are often quantized before deployment. Existing quantization techniques tend to degrade the network accuracy. We propose Counter-Example Guided Neural Network Quantization Refi… ▽ More Neural networks are essential components of learning-based software systems. However, their high compute, memory, and power requirements make using them in low resources domains challenging. For this reason, neural networks are often quantized before deployment. Existing quantization techniques tend to degrade the network accuracy. We propose Counter-Example Guided Neural Network Quantization Refinement (CEG4N). This technique combines search-based quantization and equivalence verification: the former minimizes the computational requirements, while the latter guarantees that the network's output does not change after quantization. We evaluate CEG4N~on a diverse set of benchmarks, including large and small networks. Our technique successfully quantizes the networks in our evaluation while producing models with up to 72% better accuracy than state-of-the-art techniques. △ Less

Submitted 9 July, 2022; originally announced July 2022.

Large-Margin Representation Learning for Texture Classification

Authors: Jonathan de Matos, Luiz Eduardo Soares de Oliveira, Alceu de Souza Britto Junior, Alessandro Lameiras Koerich

Abstract: This paper presents a novel approach combining convolutional layers (CLs) and large-margin metric learning for training supervised models on small datasets for texture classification. The core of such an approach is a loss function that computes the distances between instances of interest and support vectors. The objective is to update the weights of CLs iteratively to learn a representation with… ▽ More This paper presents a novel approach combining convolutional layers (CLs) and large-margin metric learning for training supervised models on small datasets for texture classification. The core of such an approach is a loss function that computes the distances between instances of interest and support vectors. The objective is to update the weights of CLs iteratively to learn a representation with a large margin between classes. Each iteration results in a large-margin discriminant model represented by support vectors based on such a representation. The advantage of the proposed approach w.r.t. convolutional neural networks (CNNs) is two-fold. First, it allows representation learning with a small amount of data due to the reduced number of parameters compared to an equivalent CNN. Second, it has a low training cost since the backpropagation considers only support vectors. The experimental results on texture and histopathologic image datasets have shown that the proposed approach achieves competitive accuracy with lower computational cost and faster convergence when compared to equivalent CNNs. △ Less

Submitted 17 June, 2022; originally announced June 2022.

Comments: 7 pages

Multiscale Analysis for Improving Texture Classification

Authors: Steve T. M. Ataky, Diego Saqui, Jonathan de Matos, Alceu S. Britto Jr., Alessandro L. Koerich

Abstract: Information from an image occurs over multiple and distinct spatial scales. Image pyramid multiresolution representations are a useful data structure for image analysis and manipulation over a spectrum of spatial scales. This paper employs the Gaussian-Laplacian pyramid to treat different spatial frequency bands of a texture separately. First, we generate three images corresponding to three levels… ▽ More Information from an image occurs over multiple and distinct spatial scales. Image pyramid multiresolution representations are a useful data structure for image analysis and manipulation over a spectrum of spatial scales. This paper employs the Gaussian-Laplacian pyramid to treat different spatial frequency bands of a texture separately. First, we generate three images corresponding to three levels of the Gaussian-Laplacian pyramid for an input image to capture intrinsic details. Then we aggregate features extracted from gray and color texture images using bio-inspired texture descriptors, information-theoretic measures, gray-level co-occurrence matrix features, and Haralick statistical features into a single feature vector. Such an aggregation aims at producing features that characterize textures to their maximum extent, unlike employing each descriptor separately, which may lose some relevant textural information and reduce the classification performance. The experimental results on texture and histopathologic image datasets have shown the advantages of the proposed method compared to state-of-the-art approaches. Such findings emphasize the importance of multiscale image analysis and corroborate that the descriptors mentioned above are complementary. △ Less

Submitted 20 April, 2022; originally announced April 2022.

Comments: 6 pages

Machine Learning Methods for Histopathological Image Analysis: A Review

Authors: Jonathan de Matos, Steve Tsham Mpinda Ataky, Alceu de Souza Britto Jr., Luiz Eduardo Soares de Oliveira, Alessandro Lameiras Koerich

Abstract: Histopathological images (HIs) are the gold standard for evaluating some types of tumors for cancer diagnosis. The analysis of such images is not only time and resource consuming, but also very challenging even for experienced pathologists, resulting in inter- and intra-observer disagreements. One of the ways of accelerating such an analysis is to use computer-aided diagnosis (CAD) systems. In thi… ▽ More Histopathological images (HIs) are the gold standard for evaluating some types of tumors for cancer diagnosis. The analysis of such images is not only time and resource consuming, but also very challenging even for experienced pathologists, resulting in inter- and intra-observer disagreements. One of the ways of accelerating such an analysis is to use computer-aided diagnosis (CAD) systems. In this paper, we present a review on machine learning methods for histopathological image analysis, including shallow and deep learning methods. We also cover the most common tasks in HI analysis, such as segmentation and feature extraction. In addition, we present a list of publicly available and private datasets that have been used in HI research. △ Less

Submitted 7 February, 2021; originally announced February 2021.

Comments: 45 pages. arXiv admin note: text overlap with arXiv:1904.07900

Quantum Accelerator Stack: A Research Roadmap

Authors: K. Bertels, A. Sarkar, A. Krol, R. Budhrani, J. Samadi, E. Geoffroy, J. Matos, R. Abreu, G. Gielen, I. Ashraf

Abstract: This paper presents the definition and implementation of a quantum computer architecture to enable creating a new computational device - a quantum computer as an accelerator In this paper, we present explicitly the idea of a quantum accelerator which contains the full stack of the layers of an accelerator. Such a stack starts at the highest level describing the target application of the accelerato… ▽ More This paper presents the definition and implementation of a quantum computer architecture to enable creating a new computational device - a quantum computer as an accelerator In this paper, we present explicitly the idea of a quantum accelerator which contains the full stack of the layers of an accelerator. Such a stack starts at the highest level describing the target application of the accelerator. Important to realise is that qubits are defined as perfect qubits, implying they do not decohere and perform good quantum gate operations. The next layer abstracts the quantum logic outlining the algorithm that is to be executed on the quantum accelerator. In our case, the logic is expressed in the universal quantum-classical hybrid computation language developed in the group, called OpenQL. We also have to start thinking about how to verify, validate and test the quantum software such that the compiler generates a correct version of the quantum circuit. The OpenQL compiler translates the program to a common assembly language, called cQASM. We need to develop a quantum operating system that manages all the hardware of the micro-architecture. The layer below the micro-architecture is responsible of the mapping and routing of the qubits on the topology such that the nearest-neighbour-constraint can be be respected. At any moment in the future when we are capable of generating multiple good qubits, the compiler can convert the cQASM to generate the eQASM, which is executable on a particular experimental device incorporating the platform-specific parameters. This way, we are able to distinguish clearly the experimental research towards better qubits, and the industrial and societal applications that need to be developed and executed on a quantum device. △ Less

Submitted 17 May, 2021; v1 submitted 3 February, 2021; originally announced February 2021.

Comments: 39 pages. arXiv admin note: text overlap with arXiv:1903.09575

Data Augmentation for Histopathological Images Based on Gaussian-Laplacian Pyramid Blending

Authors: Steve Tsham Mpinda Ataky, Jonathan de Matos, Alceu de S. Britto Jr., Luiz E. S. Oliveira, Alessandro L. Koerich

Abstract: Data imbalance is a major problem that affects several machine learning (ML) algorithms. Such a problem is troublesome because most of the ML algorithms attempt to optimize a loss function that does not take into account the data imbalance. Accordingly, the ML algorithm simply generates a trivial model that is biased toward predicting the most frequent class in the training data. In the case of hi… ▽ More Data imbalance is a major problem that affects several machine learning (ML) algorithms. Such a problem is troublesome because most of the ML algorithms attempt to optimize a loss function that does not take into account the data imbalance. Accordingly, the ML algorithm simply generates a trivial model that is biased toward predicting the most frequent class in the training data. In the case of histopathologic images (HIs), both low-level and high-level data augmentation (DA) techniques still present performance issues when applied in the presence of inter-patient variability; whence the model tends to learn color representations, which is related to the staining process. In this paper, we propose a novel approach capable of not only augmenting HI dataset but also distributing the inter-patient variability by means of image blending using the Gaussian-Laplacian pyramid. The proposed approach consists of finding the Gaussian pyramids of two images of different patients and finding the Laplacian pyramids thereof. Afterwards, the left-half side and the right-half side of different HIs are joined in each level of the Laplacian pyramid, and from the joint pyramids, the original image is reconstructed. This composition combines the stain variation of two patients, avoiding that color differences mislead the learning process. Experimental results on the BreakHis dataset have shown promising gains vis-a-vis the majority of DA techniques presented in the literature. △ Less

Submitted 16 May, 2020; v1 submitted 31 January, 2020; originally announced February 2020.

Comments: 8 pages

Journal ref: IEEE International Joint Conference on Neural Networks (IJCNN 2020), Glasgow, UK

Texture CNN for Histopathological Image Classification

Authors: Jonathan de Matos, Alceu de S. Britto Jr., Luiz E. S. de Oliveira, Alessandro L. Koerich

Abstract: Biopsies are the gold standard for breast cancer diagnosis. This task can be improved by the use of Computer Aided Diagnosis (CAD) systems, reducing the time of diagnosis and reducing the inter and intra-observer variability. The advances in computing have brought this type of system closer to reality. However, datasets of Histopathological Images (HI) from biopsies are quite small and unbalanced… ▽ More Biopsies are the gold standard for breast cancer diagnosis. This task can be improved by the use of Computer Aided Diagnosis (CAD) systems, reducing the time of diagnosis and reducing the inter and intra-observer variability. The advances in computing have brought this type of system closer to reality. However, datasets of Histopathological Images (HI) from biopsies are quite small and unbalanced what makes difficult to use modern machine learning techniques such as deep learning. In this paper we propose a compact architecture based on texture filters that has fewer parameters than traditional deep models but is able to capture the difference between malignant and benign tissues with relative accuracy. The experimental results on the BreakHis dataset have show that the proposed texture CNN achieves almost 90% of accuracy for classifying benign and malignant tissues. △ Less

Submitted 28 May, 2019; originally announced May 2019.

A Novel Orthogonal Direction Mesh Adaptive Direct Search Approach for SVM Hyperparameter Tuning

Authors: Alexandre Reeberg Mello, Jonathan de Matos, Marcelo R. Stemmer, Alceu de Souza Britto Jr., Alessandro Lameiras Koerich

Abstract: In this paper, we propose the use of a black-box optimization method called deterministic Mesh Adaptive Direct Search (MADS) algorithm with orthogonal directions (Ortho-MADS) for the selection of hyperparameters of Support Vector Machines with a Gaussian kernel. Different from most of the methods in the literature that exploit the properties of the data or attempt to minimize the accuracy of a val… ▽ More In this paper, we propose the use of a black-box optimization method called deterministic Mesh Adaptive Direct Search (MADS) algorithm with orthogonal directions (Ortho-MADS) for the selection of hyperparameters of Support Vector Machines with a Gaussian kernel. Different from most of the methods in the literature that exploit the properties of the data or attempt to minimize the accuracy of a validation dataset over the first quadrant of (C, gamma), the Ortho-MADS provides convergence proof. We present the MADS, followed by the Ortho-MADS, the dynamic stopping criterion defined by the MADS mesh size and two different search strategies (Nelder-Mead and Variable Neighborhood Search) that contribute to a competitive convergence rate as well as a mechanism to escape from undesired local minima. We have investigated the practical selection of hyperparameters for the Support Vector Machine with a Gaussian kernel, i.e., properly choose the hyperparameters gamma (bandwidth) and C (trade-off) on several benchmark datasets. The experimental results have shown that the proposed approach for hyperparameter tuning consistently finds comparable or better solutions, when using a common configuration, than other methods. We have also evaluated the accuracy and the number of function evaluations of the Ortho-MADS with the Nelder-Mead search strategy and the Variable Neighborhood Search strategy using the mesh size as a stopping criterion, and we have achieved accuracy that no other method for hyperparameters optimization could reach. △ Less

Submitted 25 April, 2019; originally announced April 2019.

Histopathologic Image Processing: A Review

Authors: Jonathan de Matos, Alceu de Souza Britto Jr., Luiz E. S. Oliveira, Alessandro L. Koerich

Abstract: Histopathologic Images (HI) are the gold standard for evaluation of some tumors. However, the analysis of such images is challenging even for experienced pathologists, resulting in problems of inter and intra observer. Besides that, the analysis is time and resource consuming. One of the ways to accelerate such an analysis is by using Computer Aided Diagnosis systems. In this work we present a lit… ▽ More Histopathologic Images (HI) are the gold standard for evaluation of some tumors. However, the analysis of such images is challenging even for experienced pathologists, resulting in problems of inter and intra observer. Besides that, the analysis is time and resource consuming. One of the ways to accelerate such an analysis is by using Computer Aided Diagnosis systems. In this work we present a literature review about the computing techniques to process HI, including shallow and deep methods. We cover the most common tasks for processing HI such as segmentation, feature extraction, unsupervised learning and supervised learning. A dataset section show some datasets found during the literature review. We also bring a study case of breast cancer classification using a mix of deep and shallow machine learning methods. The proposed method obtained an accuracy of 91% in the best case, outperforming the compared baseline of the dataset. △ Less

Submitted 16 April, 2019; originally announced April 2019.

Double Transfer Learning for Breast Cancer Histopathologic Image Classification

Authors: Jonathan de Matos, Alceu de S. Britto Jr., Luiz E. S. Oliveira, Alessandro L. Koerich

Abstract: This work proposes a classification approach for breast cancer histopathologic images (HI) that uses transfer learning to extract features from HI using an Inception-v3 CNN pre-trained with ImageNet dataset. We also use transfer learning on training a support vector machine (SVM) classifier on a tissue labeled colorectal cancer dataset aiming to filter the patches from a breast cancer HI and remov… ▽ More This work proposes a classification approach for breast cancer histopathologic images (HI) that uses transfer learning to extract features from HI using an Inception-v3 CNN pre-trained with ImageNet dataset. We also use transfer learning on training a support vector machine (SVM) classifier on a tissue labeled colorectal cancer dataset aiming to filter the patches from a breast cancer HI and remove the irrelevant ones. We show that removing irrelevant patches before training a second SVM classifier, improves the accuracy for classifying malign and benign tumors on breast cancer images. We are able to improve the classification accuracy in 3.7% using the feature extraction transfer learning and an additional 0.7% using the irrelevant patch elimination. The proposed approach outperforms the state-of-the-art in three out of the four magnification factors of the breast cancer dataset. △ Less

Submitted 16 April, 2019; originally announced April 2019.

Model Checking Event-B by Encoding into Alloy

Authors: Paulo J. Matos, Joao Marques-Silva

Abstract: As systems become ever more complex, verification becomes more main stream. Event-B and Alloy are two formal specification languages based on fairly different methodologies. While Event-B uses theorem provers to prove that invariants hold for a given specification, Alloy uses a SAT-based model finder. In some settings, Event-B invariants may not be proved automatically, and so the often difficul… ▽ More As systems become ever more complex, verification becomes more main stream. Event-B and Alloy are two formal specification languages based on fairly different methodologies. While Event-B uses theorem provers to prove that invariants hold for a given specification, Alloy uses a SAT-based model finder. In some settings, Event-B invariants may not be proved automatically, and so the often difficult step of interactive proof is required. One solution for this problem is to validate invariants with model checking. This work studies the encoding of Event-B machines and contexts to Alloy in order to perform temporal model checking with Alloy's SAT-based engine. △ Less

Submitted 30 May, 2008; v1 submitted 21 May, 2008; originally announced May 2008.