Scholarlink

In this short paper we introduce the notion of proof-based coverage. While traditional test coverage metrics measure which parts of the code are executed when a test passes, proof-based coverage aims to measure what parts of the code are required for a test to pass. Through formal verification, a proof of validity of an assertion is created. By mapping back the proof onto the source code, the essential parts can be marked, obtaining a novel coverage metric. We sketch a formalization of this notion, discuss the relationship to previous coverage metrics and show differences on small examples.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

From Execution to Necessity: Proof-Based Metrics for Code Coverage (Short Paper)

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年

查看全文
  • Karl Mattsson,
  • Peter Backeman

摘要

In this short paper we introduce the notion of proof-based coverage. While traditional test coverage metrics measure which parts of the code are executed when a test passes, proof-based coverage aims to measure what parts of the code are required for a test to pass. Through formal verification, a proof of validity of an assertion is created. By mapping back the proof onto the source code, the essential parts can be marked, obtaining a novel coverage metric. We sketch a formalization of this notion, discuss the relationship to previous coverage metrics and show differences on small examples.