FormaliSE 2026
Sun 12 - Mon 13 April 2026 Rio de Janeiro, Brazil
co-located with ICSE 2026

Statement coverage is a perfect measure of test suite effectiveness, but only if the purpose of a test suite is to cover statements. Likewise, branch coverage, condition coverage, line coverage, mutation coverage, etc. are all excellent measures of test suite effectiveness, if the purpose of a test suite is, respectively, to cover branches, cover conditions, cover lines, or kill mutants. But if we posit, as we do in this paper, that the purpose of a test suite is to expose the failures of an incorrect program (or, equivalently, to give us confidence in the correctness of a correct program), then we ought to equate the effectiveness of a test suite with its ability to expose failures. In this paper we consider a failure based definition of test suite effectiveness, which we call failure coverage, and we analyze its relationship to traditional criteria for test suite adequacy; unlike all existing measures of test suite effectiveness, failure coverage is not a number but an element of a partially ordered set, which is fitting, given that the relation of being a more effective test suite is itself a partial ordering. Not surprisingly, we find that traditional coverage metrics bear little statistical correlation to failure coverage; but we also find that it is possible to combine them to gain a better, albeit still insufficient, approximation of failure coverage. We sketch a research agenda that aims to estimate failure coverage. To the extent that it is adopted and gains acceptance, the measure of failure coverage can be used to generate novel/ original test adequacy criteria.

Mon 13 Apr

Displayed time zone: Brasilia, Distrito Federal, Brazil change

11:00 - 12:30
Session 4: Automated Reasoning, and Program AnalysisResearch Track / FormaliSE Program at Oceania VIII
11:00
30m
Talk
Simple Lambda Lifting: Formalisation in Lean and a new efficient algorithm
Research Track
Tom Levy University of Waikato, Steve Reeves University of Waikato
11:30
30m
Talk
Domain-Guided Quantifier Instantiation with Yardbird
Research Track
Cole Vick University of Texas at Austin, Samuel Thomas The University of Texas at Austin, Texas, USA
12:00
15m
Talk
From Cognition to Coordination: Modeling Agentic Autonomy in Large-Scale Multi-Agent SystemsVirtual Attendance
Research Track
Minu Tiwari Siemens AG, Himanshu Kumar Singh Siemens AG
12:15
15m
Talk
Test Data Selection by Failure Coverage
Research Track
Amani Ayad Mount Saint Vincent University, Ali Mili NJIT