Search

Datasets such as Defects4J and BugsInPy that contain bugs from real-world software projects are necessary for a realistic evaluation of automated debugging tools. However these datasets largely identify only a single bug in each entry, while real-world software projects (including those used in Defects4J and BugsInPy) typically contain multiple bugs at the same time. We lift this limitation and describe an extension to these datasets in which multiple bugs are identified in individual entries. We use test case transplantation and fault location translation, in order to expose and locate the bugs, respectively. We thus provide datasets of true multi-fault versions within real-world software projects, which maintain the properties and usability of the original datasets., Comment: 9 pages, LaTeX; references for dataset projects added

Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterative Test Suite Reduction), a novel SBFL extension that improves the localization of a given base metric specifically in the presence of multiple faults. FLITSR iteratively selects reduced versions of the test suite that better localize the individual faults in the system. This allows it to identify and re-rank faults ranked too low by the base metric because they were masked by other program elements. We evaluated FLITSR over method-level spectra from an existing large synthetic dataset comprising 75000 variants of 15 open-source projects with up to 32 injected faults, as well as method-level and statement-level spectra from a new dataset with 326 true multi-fault versions from the Defects4J benchmark set containing up to 14 real faults. For all three spectrum types we consistently see substantial reductions of the average wasted efforts at different fault levels, of 30%-90% over the best base metric, and generally similarly large increases in precision and recall, albeit with larger variance across the underlying projects. For the method-level real faults, FLITSR also substantially outperforms GRACE, a state-of-the-art learning-based fault localizer.

We are demonstrating the optical control of a specific state of the germanium telluride (GeTe) phase change material and its integration as control element for realizing extremely efficient optically reconfigurable THz devices. The excellent contrast of the material THz electrical properties in the two dissimilar states were used for optical-induced fast modulation of THz resonances of a hybrid metamaterial based of arrays of split ring resonator metallic structures integrating GeTe patterns. We experimentally confirm for the first time the feasibility to develop all dielectric (metal free) GeTe-based THz polarizers presenting a broadband response, a high extinction ratio when the GeTe is in the metal-like phase (up to 16.5 dB) and almost transparent when the material is in the amorphous phase. The presented highly functional approach based on non-volatile, optically controlled multi-operational THz devices integrating PCMs, is extremely stimulating for generating disruptive developments like field-programmable metasurfaces or all-dielectric coding metamaterials with multifunctional capabilities for THz waves manipulation.

We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we complement CSA's existing heuristics that remove spurious bug reports. We encode the path constraints produced by CSA as Satisfiability Modulo Theories (SMT) problems, use SMT solvers to precisely check them for satisfiability, and remove bug reports whose associated path constraints are unsatisfiable. Our refutation extension refutes spurious bug reports in 8 out of 12 widely used open-source applications; on average, it refutes ca. 7% of all bug reports, and never refutes any true bug report. It incurs only negligible performance overheads, and on average adds 1.2% to the runtime of the full Clang/LLVM toolchain. A demonstration is available at {\tt https://www.youtube.com/watch?v=ylW5iRYNsGA}., Comment: 4 pages

Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checker such as ESBMC. Thus, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood., Comment: 16 pages

The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three approaches to model check multi-threaded software and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the BMC procedure on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation-widening approach, we reduce the state space by abstracting the number of state variables and interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we use partial-order reduction (POR) techniques to reduce the number of interleavings explored. Experiments show that our approaches can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that combine classic POR methods with symbolic algorithms and others that implement the Counter-Example Guided Abstraction Refinement technique.

The complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. In this context, SAT-based bounded model checking has been successfully applied to discover subtle errors, but for larger applications, it often suffers from the state space explosion problem. This paper describes a new approach called continuous verification to detect design errors as quickly as possible by looking at the Software Configuration Management (SCM) system and by combining dynamic and static verification to reduce the state space to be explored. We also give a set of encodings that provide accurate support for program verification and use different background theories in order to improve scalability and precision in a completely automatic way. A case study from the telecommunications domain shows that the proposed approach improves the error-detection capability and reduces the overall verification time by up to 50%.