-
Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
Authors:
Paschal C. Amusuo,
Owen Cochell,
Taylor Le Lievre,
Parth V. Patil,
Aravind Machiry,
James C. Davis
Abstract:
Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded Model Checking (BMC), using unit proofs to formally verify memory safety. However, methods for creating unit proofs vary across organizations and are inconsistent within the same project, leading to errors and missed defe…
▽ More
Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded Model Checking (BMC), using unit proofs to formally verify memory safety. However, methods for creating unit proofs vary across organizations and are inconsistent within the same project, leading to errors and missed defects. In addition, unit proofing remains understudied, with no systematic development methods or empirical evaluations.
This work presents the first empirical study on unit proofing for memory safety verification. We introduce a systematic method for creating unit proofs that leverages verification feedback and objective criteria. Using this approach, we develop 73 unit proofs for four embedded operating systems and evaluate their effectiveness, characteristics, cost, and generalizability. Our results show unit proofs are cost-effective, detecting 74\% of recreated defects, with an additional 9\% found with increased BMC bounds, and 19 new defects exposed. We also found that embedded software requires small unit proofs, which can be developed in 87 minutes and executed in 61 minutes on average. These findings provide practical guidance for engineers and empirical data to inform tooling design.
△ Less
Submitted 17 March, 2025;
originally announced March 2025.
-
Recommending Pre-Trained Models for IoT Devices
Authors:
Parth V. Patil,
Wenxin Jiang,
Huiyun Peng,
Daniel Lugo,
Kelechi G. Kalu,
Josh LeBlanc,
Lawrence Smith,
Hyeonwoo Heo,
Nathanael Aou,
James C. Davis
Abstract:
The availability of pre-trained models (PTMs) has enabled faster deployment of machine learning across applications by reducing the need for extensive training. Techniques like quantization and distillation have further expanded PTM applicability to resource-constrained IoT hardware. Given the many PTM options for any given task, engineers often find it too costly to evaluate each model's suitabil…
▽ More
The availability of pre-trained models (PTMs) has enabled faster deployment of machine learning across applications by reducing the need for extensive training. Techniques like quantization and distillation have further expanded PTM applicability to resource-constrained IoT hardware. Given the many PTM options for any given task, engineers often find it too costly to evaluate each model's suitability. Approaches such as LogME, LEEP, and ModelSpider help streamline model selection by estimating task relevance without exhaustive tuning. However, these methods largely leave hardware constraints as future work-a significant limitation in IoT settings. In this paper, we identify the limitations of current model recommendation approaches regarding hardware constraints and introduce a novel, hardware-aware method for PTM selection. We also propose a research agenda to guide the development of effective, hardware-conscious model recommendation systems for IoT applications.
△ Less
Submitted 25 December, 2024;
originally announced December 2024.
-
A Unit Proofing Framework for Code-level Verification: A Research Agenda
Authors:
Paschal C. Amusuo,
Parth V. Patil,
Owen Cochell,
Taylor Le Lievre,
James C. Davis
Abstract:
Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and…
▽ More
Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and verifying each unit independently. We examined AWS's use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early.
△ Less
Submitted 30 April, 2025; v1 submitted 18 October, 2024;
originally announced October 2024.
-
Network Clustering Via Kernel-ARMA Modeling and the Grassmannian The Brain-Network Case
Authors:
Cong Ye,
Konstantinos Slavakis,
Pratik V. Patil,
Johan Nakuci,
Sarah F. Muldoon,
John Medaglia
Abstract:
This paper introduces a clustering framework for networks with nodes annotated with time-series data. The framework addresses all types of network-clustering problems: State clustering, node clustering within states (a.k.a. topology identification or community detection), and even subnetwork-state-sequence identification/tracking. Via a bottom-up approach, features are first extracted from the raw…
▽ More
This paper introduces a clustering framework for networks with nodes annotated with time-series data. The framework addresses all types of network-clustering problems: State clustering, node clustering within states (a.k.a. topology identification or community detection), and even subnetwork-state-sequence identification/tracking. Via a bottom-up approach, features are first extracted from the raw nodal time-series data by kernel autoregressive-moving-average modeling to reveal non-linear dependencies and low-rank representations, and then mapped onto the Grassmann manifold (Grassmannian). All clustering tasks are performed by leveraging the underlying Riemannian geometry of the Grassmannian in a novel way. To validate the proposed framework, brain-network clustering is considered, where extensive numerical tests on synthetic and real functional magnetic resonance imaging (fMRI) data demonstrate that the advocated learning framework compares favorably versus several state-of-the-art clustering schemes.
△ Less
Submitted 18 February, 2020;
originally announced February 2020.
-
Brain-Network Clustering via Kernel-ARMA Modeling and the Grassmannian
Authors:
Cong Ye,
Konstantinos Slavakis,
Pratik V. Patil,
Sarah F. Muldoon,
John Medaglia
Abstract:
Recent advances in neuroscience and in the technology of functional magnetic resonance imaging (fMRI) and electro-encephalography (EEG) have propelled a growing interest in brain-network clustering via time-series analysis. Notwithstanding, most of the brain-network clustering methods revolve around state clustering and/or node clustering (a.k.a. community detection or topology inference) within s…
▽ More
Recent advances in neuroscience and in the technology of functional magnetic resonance imaging (fMRI) and electro-encephalography (EEG) have propelled a growing interest in brain-network clustering via time-series analysis. Notwithstanding, most of the brain-network clustering methods revolve around state clustering and/or node clustering (a.k.a. community detection or topology inference) within states. This work answers first the need of capturing non-linear nodal dependencies by bringing forth a novel feature-extraction mechanism via kernel autoregressive-moving-average modeling. The extracted features are mapped to the Grassmann manifold (Grassmannian), which consists of all linear subspaces of a fixed rank. By virtue of the Riemannian geometry of the Grassmannian, a unifying clustering framework is offered to tackle all possible clustering problems in a network: Cluster multiple states, detect communities within states, and even identify/track subnetwork state sequences. The effectiveness of the proposed approach is underlined by extensive numerical tests on synthetic and real fMRI/EEG data which demonstrate that the advocated learning method compares favorably versus several state-of-the-art clustering schemes.
△ Less
Submitted 5 June, 2019;
originally announced June 2019.