Author name cluster

Emily Yu

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

FM Conference 2026 Conference Paper

Certifying Constraints in Hardware Model Checking

Nils Froleyks
Emily Yu
Armin Biere
Keijo Heljanko

Abstract Model checking is a powerful automated reasoning technique for verifying hardware designs, ensuring that they function correctly before deployment. However, modern model checkers are complex software systems with hundreds of thousands of lines of code, making them prone to errors. To increase confidence in verification results, recent efforts in hardware verification focus on requiring model checkers to produce machine-checkable proofs according to a standardized format that can be independently validated. Yet, implementing proof generation across different verification algorithms presents a unique challenge. In hardware model checking, constraints play an essential role, as they encode assumptions about the environment and help simplify analysis. This paper addresses the challenge by developing a certification approach that ensures verification results remain trustworthy when constraints are present. We introduce certificate generation methods for three classes of constraints that can be extracted from the models. Furthermore, to support a broader range of constraints and more complex reset logic for industrial use, we also provide alternative Quantified Boolean Formula checks in the proof format with a single quantifier alternation. Lastly, we present a certificate generation method for k -induction with uniqueness constraints, an important model checking technique. We implement these in a certification toolkit, and provide empirical evaluation on competition benchmarks, demonstrating their effectiveness.

DOI

FM Conference 2026 Conference Paper

Quantitative Monitoring of Signal First-Order Logic

Marek Chalupa
Thomas A. Henzinger
N. Ege Saraç
Emily Yu

Abstract Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.

DOI

AAAI Conference 2026 Short Paper

Spatiotemporal Transformers with Multiple Instance Learning for Label-Efficient Behavioral Analysis in Autism (Student Abstract)

Emily Yu

The identification of unique traits and behavior is essential to providing personalized intervention in individuals with Autism Spectrum Disorder. However, the limited personalized quantitative data with experts' annotations in autism research pose a fundamental challenge to train AI models for unique behavioral patten discovery. Multiple Instance Learning (MIL) has demonstrated promising results in medical domains, where annotations are only needed at the group level (i.e., a whole sequence) instead of individual data instances. It provides a cost-effective way to train statistical models with limited labeled data. Additionally, the rise of pretrained models have shown great success in improving the performance in few-shot learning scenarios. In this proof-of-concept study, we propose a novel framework that integrates a transformer encoder pre-trained on large-scale spatiotemporal data with MIL, for unique behavioral pattern detection from autistic individuals. Our results demonstrated the discrimination of individual-level autistic behavioral differences and the accurate classification of behaviors across distinct groups: typically developing (TD) and autistic (ASD). Beyond aggregate performance metrics, we highlight visual insights from temporal instance scores, revealing interpretable differences between individuals in their respective groups. These results show promising progress towards tools that can be used for personalized intervention for autistic individuals, and more interpretable AI diagnostics.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Neural Control and Certificate Repair via Runtime Monitoring

Emily Yu
Đorđe Žikelić
Thomas A. Henzinger

Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.

PDF Details DOI

AAAI Conference 2025 Short Paper

Understanding Unique Behavioral Patterns through Multimodal Analysis of Eye-Hand Coordination in Autistic Children (Student Abstract)

Emily Yu

Data-driven analysis has shown promising results in identifying subtle patterns in the behavior of individuals with Autism Spectrum Disorder (ASD) for diagnosis and intervention. However, most existing methods primarily focus on a single behavioral modality (e.g., eye movements) instead of capturing the intricate multimodal behavior of humans. We propose a multimodal approach that investigates the underlying connections between eye movements and hand motions through eye-to-hand prediction. To tackle the highly noisy and irregular behavioral data, we propose a novel approach that defines the prediction as a machine translation problem and leverages a sequence-to-sequence machine learning model for the prediction. An experimental study on a dataset collected from a VR system has demonstrated high prediction accuracy. The significant difference in the prediction accuracy between the autistic group and their typically developing (TD) peers serves as quantitative evidence to objectively understand the restricted and repetitive behaviors (RRBs) in autistic children. The source code can be accessed here: https://github.com/mathjams/AAAI_2024.

PDF Details DOI

JAIR Journal 2022 Journal Article

Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications

Francesco Belardinelli
Alessio Lomuscio
Vadim Malvone
Emily Yu

The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic ATL, hence ATL∗, under perfect recall and imperfect information is known to be undecidable. To tackle this problem, in this paper we investigate a notion of bounded recall under incomplete information. We present a novel three-valued semantics for ATL∗ in this setting and analyse the corresponding model checking problem. We show that the three-valued semantics here introduced is an approximation of the classic two-valued semantics, then give a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall. Finally, we extend MCMAS, an open-source model checker for ATL and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.

PDF Details DOI

AAAI Conference 2020 Conference Paper

Model Checking Temporal Epistemic Logic under Bounded Recall

Francesco Belardinelli
Alessio Lomuscio
Emily Yu

We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporalepistemic logic CTLK. We deﬁne and study the model checking problem against CTLK speciﬁcations under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.

PDF Details