Mutation testing is a popular way of assessing and improving test suites by creating defective variants of the code under test (CUT) using mutation operators. A test suite is run against all such defective CUT variants and its adequacy is measured in terms of the number of defective variants it is able to detect. Traditionally, mutation operators target individual statements of the CUT and presume the defect detection ability of mutant-revealing tests on the basis of the coupling effect hypothesis: Tests that reveal all simple faults are sensitive enough to also detect complex faults [7]. This hypothesis has been repeatedly investigated by comparing typical mutations against real defects or more complex (synthetic) mutations.

Abstract This tutorial provides an introduction toCPAcheckerfor users.CPAcheckeris a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking,Impact, interpolation-based model checking,k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases forCPAcheckerin formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases ofCPAcheckerfor test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge ofCPAcheckeris not required. This tutorial and user guide is based onCPAcheckerin version 3.0. This user guide’s latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php .

Identifying and fixing bugs in programs remains a challenge and is one of the most time-consuming tasks in software development. But even after a bug is identified, and a fix has been proposed by a developer or tool, it is not uncommon that the fix is incomplete and does not cover all possible inputs that trigger the bug. This can happen quite often and leads to re-opened issues and inefficiencies. In this paper, we introduce P3, a curated dataset composed of incomplete fixes. Each entry in the set contains a series of commits fixing the same underlying issue, where multiple of the intermediate commits are incomplete fixes. These are sourced from real-world open-source C projects. The selection process involves both automated and manual stages. Initially, we employ heuristics to identify potential partial fixes from repositories, subsequently we validate them through meticulous manual inspection. This process ensures the accuracy and reliability of our curated dataset. We envision that the dataset will support researchers while investigating partial fixes in more detail, allowing them to develop new techniques to detect and fix them. We make our dataset publicly available at https://gitlab.com/sosy-lab/research/data/partial-fix-dataset.

Abstract When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.

Abstract CPAcheckeris a versatile framework for software verification, rooted in the established concept ofconfigurable program analysis. Compared to the last published system description at SV-COMP 2015, theCPAcheckersubmission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses inCPAcheckerand cover the full spectrum of the diverse program characteristics and specifications in the competition, we usestrategy selectionto predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses usingk-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms inCPAcheckerenables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories.CPAcheckeralso generates verification witnesses in the new YAML format.

Abstract We present Infer-sv, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-sv, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.