activity
20242026
most citedAutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

1 citations · 1 across the 2 of their papers we have counts for

collaborators
Showing cs.SEShow all

5 papers · 1 filter

cs.SE2026

SPIDER4TianoCore: Enhancing Patch-Propagation for the TianoCore UEFI Firmware Development Ecosystem

Laura Baird, Devin Haggitt, Terrance E. Boult +2

We propose and demonstrate SPIDER4TianoCore, a packaged Python command-line tool that provides integration-stage patch-status evidence for the TianoCore/UEFI firmware supply chain.…

cs.SE2026

An Empirical Study of the TianoCore Community

Nazanin Siavash, Connor Glosner, Ayushi Sharma +4

We investigate the software security and maintenance practices adopted by stakeholders in the TianoCore community and identify opportunities to improve firmware development workflo…

cs.SE20261 cited

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

Paschal C. Amusuo, Ricardo Calvo, Dharun Anandayuvaraj +5

Memory-safety errors remain a persistent source of zero-day vulnerabilities in low-level software. The problem is especially acute in embedded systems, where hardware protections a…

cs.SE2025

Finding 709 Defects in 258 Projects: An Experience Report on Applying CodeQL to Open-Source Embedded Software (Experience Paper) -- Extended Report

Mingjie Shen, Akul Abhilash Pillai, Brian A. Yuan +2

In this experience paper, we report on a large-scale empirical study of Static Application Security Testing (SAST) in Open-Source Embedded Software (EMBOSS) repositories. We collec…

cs.SE2025

Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification

Paschal C. Amusuo, Owen Cochell, Taylor Le Lievre +3

Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded M…