A blockchain is a list of data blocks as a publicly distributed ledger, which are linked together using cryptography. By allowing Turing-complete programming languages to implement smart contracts, recent blockchains such as Ethereum can reduce needs in trusted intermediators, arbitrations and enforcement costs. However, subtle errors in smart contracts have induced an enormous financial loss—for examples, the DAO attack, Parity multisignature wallet attacks, and integer underflow/overflow attacks. To identify such errors in smart contracts, various researches are performed, which are based on static analysis and theorem proving. However, they only support inspection for pre-defined error patterns, or they cannot explore the whole searching space exhaustively or be fully automatic. Hence, in this paper, we propose a novel formal verification technique to analyze blockchain smart contracts by using ATL model checking. In our methodology, we represent the interaction between users and smart contracts into a two-player game and verify properties we want to check using MCMAS that is an efficient ATL model checker for multi-agent systems. Moreover, we present three case studies to show that our proposal can successfully identify subtle flaws in real world smart contracts.

Deep neural networks have achieved remarkable performance in various fields such as image recognition and natural language processing. However, recent research has revealed that even a small imperceptible perturbation can confound well-trained neural network models and yield incorrect answers. Such adversarial examples are regarded as a key hazard to the application of machine learning techniques to safety-critical systems, such as unmanned vehicle navigation and security systems. In this study, we propose an efficient technique for searching one-pixel attacks in deep neural networks, which are recently reported as an adversarial example. Using exhaustive search, our method can identify one-pixel attacks which existing methods cannot detect. Moreover, the method can adjust exhaustiveness to reduce the search space dramatically. However, it still identifies most attacks. We present our experiment using the MNIST data set to demonstrate that our adjustable search method efficiently identifies one-pixel attacks in well-trained deep neural networks, including convolutional layers.

Recent research has revealed that subtle imperceptible perturbations can deceive well-trained neural network models, leading to inaccurate outcomes. These instances, known as adversarial examples, pose significant threats to the secure application of machine learning techniques in safety-critical systems. In this paper, we delve into the study of one-pixel attacks in deep neural networks, recently reported as a kind of adversarial examples. To identify such one-pixel attacks, most existing methodologies rely on the differential evolution method, which utilizes random selection from the current population to escape local optima. However, the differential evolution technique might waste search time and overlook good solutions if the number of iterations is insufficient. Hence, in this paper, we propose a gradient ascent with momentum approach to efficiently discover good solutions for the one-pixel attack problem. As our method takes a more direct route to the goal compared to existing methods relying on blind random walks, it can effectively identify one-pixel attacks. Our experiments conducted on popular CNNs demonstrate that, in comparison with existing methodologies, our technique can detect one-pixel attacks significantly faster.

Alzheimer’s disease (AD) is a progressive neurodegenerative disorder that impairs cognitive function, making early detection crucial for timely intervention. This study proposes a novel AD detection framework integrating gaze and head movement analysis via a dual-pathway convolutional neural network (CNN). Unlike conventional methods relying on linguistic, speech, or neuroimaging data, our approach leverages non-invasive video-based tracking, offering a more accessible and cost-effective solution to early AD detection. To enhance feature representation, we introduce GazeMap, a novel transformation converting 1D gaze and head pose time-series data into 2D spatial representations, effectively capturing both short- and long-term temporal interactions while mitigating missing or noisy data. The dual-pathway CNN processes gaze and head movement features separately before fusing them to improve diagnostic accuracy. We validated our framework using a clinical dataset (112 participants) from Konkuk University Hospital and an out-of-distribution dataset from senior centers and nursing homes. Our method achieved 91.09% accuracy on in-distribution data collected under controlled clinical settings, and 83.33% on out-of-distribution data from real-world scenarios, outperforming several time-series baseline models. Model performance was validated through cross-validation on in-distribution data and tested on an independent out-of-distribution dataset. Additionally, our gaze-saliency maps provide interpretable visualizations, revealing distinct AD-related gaze patterns.

Aspect-based sentiment analysis (ABSA) aims at identifying the sentiment polarity for a particular aspect in a review. ABSA studies based on deep learning models have exploited the attention mechanism to detect aspect-related parts. Conventional softmax-based attention mechanisms generate dense distributions, which may limit performance in tasks that inherently require sparsity. Recent studies on sparse attention transformation functions have demonstrated their effectiveness over the conventional softmax function. However, these studies primarily focus on highly sparse tasks based on self-attention architectures, leaving their applicability to the ABSA domain unexplored. In addition, most ABSA research has focused on leveraging aspect terms despite the usefulness of aspect categories. To address these issues, we propose a sparse-attention-based residual joint network (SPA-RJ Net) for the aspect-category-based sentiment analysis (ACSA) task. SPA-RJ Net incorporates two aspect-guided sparse attentions—sparse aspect-category attention and sparse aspect-sentiment attention—that introduce sparsity in attention via a sparse distribution transformation function, enabling the model to selectively focus on aspect-related information. In addition, it employs a residual joint learning framework that connects the aspect category detection (ACD) task module and the ACSA task module via residual connections, enabling the ACSA module to receive explicit guidance on relevant aspect categories from the ACD module. Our experiment validates that SPA-RJ Net consistently outperforms existing models, demonstrating the effectiveness of sparse attention and residual joint learning for aspect category-based sentiment classification.

Recent studies have shown that deep neural networks can be misled by adversarial examples that involve only imperceptible perturbations. Among these, one-pixel attacks (OPA) represent an extreme yet powerful threat, as they alter only a single pixel of an input image while causing misclassification. While prior work has demonstrated the effectiveness of OPAs on low-resolution datasets, extending these attacks to high-resolution images poses a significant challenge due to the dramatic increase in the number of pixels and the resulting expansion of the search space. In this paper, we address this challenge by proposing a scalable one-pixel attack framework for deep neural networks on high-resolution images. The key difficulty in high-resolution OPAs lies in identifying a vulnerable pixel among tens of thousands of candidates under a black-box setting, where exhaustive pixel-wise probing is prohibitively expensive. To overcome this limitation, we decompose the attack into two phases. In the first phase, we efficiently identify a small set of promising pixel locations using a hierarchical patch-based search strategy, which iteratively prunes large image regions via coarse-grained patch perturbations, thereby substantially reducing the number of required model queries. In the second phase, for each selected pixel candidate, we search for adversarial RGB values using a black-box optimization method based on momentum-accelerated finite-difference gradient estimation. We evaluate our method on popular deep neural network architectures using high-resolution ImageNet images. The experimental results demonstrate that our approach achieves high attack success rates while significantly reducing query cost and improving the quality of the resulting adversarial perturbations compared to existing strategies.