Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Amusuo, Paschal C., Cochell, Owen, Lievre, Taylor Le, Patil, Parth V., Machiry, Aravind, Davis, James C.
Format:	Preprint
Published:	2025
Subjects:	Software Engineering D.2.4; F.3.1
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Unit Proofing Framework for Code-level Verification: A Research Agenda
by: Amusuo, Paschal C., et al.
Published: (2024)

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
by: Amusuo, Paschal C., et al.
Published: (2026)

FalseCrashReducer: Mitigating False Positive Crashes in OSS-Fuzz-Gen Using Agentic AI
by: Amusuo, Paschal C., et al.
Published: (2025)

LEMIX: Enabling Testing of Embedded Applications as Linux Applications (Extended Report)
by: Tanksalkar, Sai Ritvik, et al.
Published: (2025)

ZTD$_{JAVA}$: Mitigating Software Supply Chain Vulnerabilities via Zero-Trust Dependencies
by: Amusuo, Paschal C., et al.
Published: (2023)

Towards a Benchmark for Dependency Decision-Making
by: Singla, Tanmay, et al.
Published: (2026)

Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
by: Beyer, Dirk, et al.
Published: (2022)

A Guide to Stakeholder Analysis for Cybersecurity Researchers
by: Davis, James C, et al.
Published: (2025)

On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)
by: Abdulla, Parosh Aziz, et al.
Published: (2026)

Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
by: McCann, Alan L.
Published: (2026)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
by: Frenkel, Eden, et al.
Published: (2026)

QuickCheck for VDM
by: Battle, Nick, et al.
Published: (2024)

Bounded Model Checking for Unbounded Client Server Systems
by: Phawade, Ramchandra, et al.
Published: (2022)

Adaptive Proof Refinement with LLM-Guided Strategy Selection
by: Lu, Minghai, et al.
Published: (2025)

Reactive Bottom-Up Testing
by: Muralee, Siddharth, et al.
Published: (2025)

Precision Guided Approach to Mitigate Data Poisoning Attacks in Federated Learning
by: Kumar, K Naveen, et al.
Published: (2024)

ICAN-Deploy: Identity-Stable Canary Deployment for Safety-Critical Embodied Agents
by: Qin, Xue, et al.
Published: (2026)

Physical oceanography during Walther Herwig I cruise WH24
by: Anonymous
Published: (2011)

UR4NNV: Neural Network Verification, Under-approximation Reachability Works!
by: Liang, Zhen, et al.
Published: (2024)

ExVerus: Verus Proof Repair via Counterexample Reasoning
by: Yang, Jun, et al.
Published: (2026)

Marine optical absorption during Akademik Vernadsky cruise AV24
by: Piontkovski, Sergey, et al.
Published: (2011)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
by: Chiari, Michele, et al.
Published: (2024)

Memory Traces: Are Transformers Tulving Machines?
by: Chauvet, Jean-Marie
Published: (2024)

Physical oceanography, phytoplankton, and primary production in surface water during Professor Vodyanitskiy cruise PV24
by: Piontkovski, Sergey, et al.
Published: (2011)

Model Checking Probabilistic Operator Precedence Automata
by: Pontiggia, Francesco, et al.
Published: (2024)

Physical oceanography during Akademik Vernadsky cruise AV24
by: Piontkovski, Sergey, et al.
Published: (2011)

Channels with Markov Synchronization Errors: Information Stability and Capacity Bounds
by: Morozov, Ruslan, et al.
Published: (2024)

Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains
by: Untila, Octavian
Published: (2026)

Memory GAPS: Would LLMs pass the Tulving Test?
by: Chauvet, Jean-Marie
Published: (2024)

Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking
by: Marksteiner, Stefan, et al.
Published: (2025)

Verification of E-Voting Algorithms in Dafny
by: Büttner, Robert, et al.
Published: (2025)

QUT: A Unit Testing Framework for Quantum Subroutines
by: Klymenko, Mykhailo V., et al.
Published: (2025)

Reachability and Safety Games under TSO Semantics
by: Spengler, Stephan
Published: (2024)

Finding 709 Defects in 258 Projects: An Experience Report on Applying CodeQL to Open-Source Embedded Software (Experience Paper) -- Extended Report
by: Shen, Mingjie, et al.
Published: (2023)

Rethinking Software Empirical Studies with Structural Causal Models
by: Rodriguez-Cardenas, Daniel, et al.
Published: (2026)

Hydrochemistry measured on water bottle samples during Akademik Vernadsky cruise AV24
by: Piontkovski, Sergey, et al.
Published: (2011)

Inorganic nutrients measured on water bottle samples during POLARSTERN cruise ARK-IX/1b
by: Kattner, Gerhard
Published: (2011)

(Supplemental Materials, Table 3) Observations from images collected by the Submersible ALVIN on Dorado Outcrop, December 2014 (AT26-24)
by: Wheat, C Geoffrey, et al.
Published: (2019)

Verification Challenge: Fractional Cascading for Multi-Nuclide Grid Lookup
by: Siegel, Andrew R.
Published: (2025)

Tool-Assisted Conformance Checking to Reference Process Models
by: Rumpe, Bernhard, et al.
Published: (2025)