Fizzer is a gray-box fuzzer introduced at Test-Comp 2024. This paper summarizes the lessons learned with the original version and describes the major changes including new analyses implemented in the current version of Fizzer. In particular, Fizzer now uses dynamic taint-flow analysis and local space fuzzing. We also provide experimental results showing the progress between the two versions.
Proving properties about robotic systems with humans-in-the-loop relies on assumptions about human behaviour. Existing technologies require expertise not reasonably expected from psychologists and human-factors engineers, for instance. A user-needs analysis of industrial design techniques for human-robot interaction has identified a lack of standardised approach. We present RoboScene, a notation based on UML sequence diagrams that can be used to capture assumptions derived from human-factors artefacts, through novel constructs enabling consideration of stakeholders with different traits. We describe a tock-CSP semantics for RoboScene, and show how we can connect (mathematically) RoboScene diagrams to platform-independent software models. This is applied in the context of a Human-Centered Engineering process, demonstrated via an industrial case study.
In a service system, operations engineers generally deploy numerous monitoring mechanisms in system components to detect anomalies caused by system faults and generate alerts, also known as alarms, that record the phenomenon of anomalies. Due to the topological relationships between system components, a system fault in a system component may affect other components and result in various local anomalies and generate multiple alerts across different components. Therefore, to facilitate troubleshooting, alerts of the same system fault are usually correlated into one group, called alert incident. However, although there are existing approaches that can automatically correlate alerts for operations engineers, analyzing alert incidents still rely on manual work. In this paper, we propose an approach, VOCE (Virtual On-Call Engineer). Using the emerging capabilities of a large language model, VOCE can automatically comprehend the anomaly information described by alerts and emulate the process of operations engineers analyzing an alert incident. Extensive experiments conducted on real alert incidents and two popular large language models demonstrate the effectiveness and efficiency of VOCE in automatically analyzing alert incidents.
The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results). To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.
It is often the case that a robot must adapt to unexpected changes in its environment. It is, however, important that these changes can be demonstrated to maintain the safe operation of the robot. The adaptive systems community has developed the MAPE-K pattern as a widely recognised conceptual architecture. We propose extending MAPE-K to incorporate runtime verification, resulting in an architecture we call MAPLE-K. In this paper, we capture and formalise both the MAPE-K and MAPLE-K architectures using a domain-specific language. Additionally, we provide support for translation from architectural models to software models and code to facilitate the deployment of verified applications. MAPE-K is rarely maintained at the implementation level, but our work ensures traceability between the code and its design, enabling the use of architectural information to verify the correctness of the software.
ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the Cover-Branches category of Test-Comp 2025.
Hypervisors allow sharing of computing resources between applications—possibly of various levels of criticality—that makes them increasingly relevant for modern embedded systems. In this context, memory isolation properties (including low-level cache isolation) are essential to guarantee. This paper presents a case study on formal verification of the cache coloring mechanism implemented in the Bao hypervisor. It proposes an original technique for coloring memory pages and assigning to each virtual machine only pages of certain colors, aimed to provide strong isolation guarantees. The implementation presents several challenges for formal verification, such as bit-level operations, complex arithmetic operations, multiple levels of nested loops, and linked lists. We identify two subtle bugs in the existing implementation breaking the expected guarantees, and propose bug fixes. We provide formal specification for the key functions of the mechanism and verify their (fixed) version in the Frama-C verification platform with a few lemmas proved in the Coq proof assistant. We present our specification choices, verification approach and obtained results. Finally, we outline possible optimizations of the current implementation.
Subtyping in object-oriented languages is widely based on Liskov’s substitution principle, which offers static correctness guarantees of type safety while abstracting implementation details. Unfortunately, the type systems of languages like Java cannot statically enforce full behavioral substitutability, and in fact there are numerous examples of libraries some of whose components are related by inheritance but not substitutable (for example, because they do not implement “optional” operations). In this paper, we present a novel approach to precisely specify and reason about substitutability in JVM languages. A distinctive feature of our approach is that it targets JVM bytecode, as opposed to a program’s source code, as it is based on the ByteBack deductive verifier. To support reasoning about substitutability, we extended ByteBack with ghost specifications, a (restricted) form of class invariants, and substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening). Equipped with these features, ByteBack can now reason precisely about behavioral substitutability violations in a way that is applicable to realistic examples (such as with optional operations of Java’s List interface). Our experiments also demonstrate that ByteBack can analyze substitutability in programs written in a combination of JVM languages, including multi-language code where Scala or Kotlin code interacts with Java libraries.
Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.
The 7th edition of the Competition on Software Testing (Test-Comp 2025) provides an overview and comparative evaluation of automatic test-suite generators for C programs. The experimental evaluation was performed on a benchmark set of 11 226 test-generation tasks for C programs. Each test-generation task consisted of a program and a test specification. The test specifications included error coverage (generate a test suite that exhibits a bug) and branch coverage (generate a test suite that executes as many program branches as possible). Test-Comp 2025 evaluated 20 software systems for test generation that are all freely available. This included 13 test-suite generators that participated with active support from teams led by 12 different representatives from 8 countries (actively maintained software systems, participation in competition jury). Test-Comp 2025 had 1 new participant ( ) and 2 re-entries ( , ). The evaluation included also 7 test-generation tools from previous years.
Automata learning is an approach for extracting a model in the shape of an automaton from a black-box system. This approach has recently gained much attention in both industry and academia. In this paper, we introduce a compositional automata learning algorithm for systems comprising synchronous parallel components. Our algorithm assumes no prior knowledge about the number of components, their individual alphabets, and the synchronizing alphabets. The learning process is automatic and figures out the alphabet symbols on-the-fly during learning the components. We prove that the proposed algorithm terminates and correctly learns the individual components. We use a number of case studies from the industrial automotive domain and synthetic benchmarks to evaluate the performance of the proposed algorithm. The experimental results show that the algorithm requires significantly fewer input symbols and resets to learn the system compositionally.
Efficiency is essential to support responsiveness w.r.t. ever-growing datasets, especially for Deep Learning (DL) systems. DL frameworks have traditionally embraced deferred execution-style DL code—supporting symbolic, graph-based Deep Neural Network (DNN) computation. While scalable, such development is error-prone, non-intuitive, and difficult to debug. Consequently, more natural, imperative DL frameworks encouraging eager execution have emerged but at the expense of run-time performance. Though hybrid approaches aim for the “best of both worlds,” using them effectively requires subtle considerations to make code amenable to safe, accurate, and efficient graph execution—avoiding performance bottlenecks and semantically inequivalent results. We discuss the engineering aspects of a refactoring tool that automatically determines when it is safe and potentially advantageous to migrate imperative DL code to graph execution and vice-versa.
Direct kernel fuzzing is a targeted approach that focuses on specific areas of the kernel, effectively addressing the challenges of frequent updates and the inherent complexity of operating systems, which are critical infrastructure. This paper introduces SyzAgent, a framework integrating LLMs with the state-of-the-art kernel fuzzer Syzkaller, where the LLMs are used to guide the mutation and generation of test cases in real-time. We present preliminary results demonstrating that this method is effective on around 67
Code review is a vital but demanding aspect of software development, generating significant interest in automating review comments. Traditional evaluation methods for these comments, primarily based on text similarity, face two major challenges: inconsistent reliability of human-authored comments in open-source projects and the weak correlation of text similarity with objectives like enhancing code quality and detecting defects. This study empirically analyzes benchmark comments using a novel set of criteria informed by prior research and developer interviews. We then similarly revisit the evaluation of existing methodologies. Our evaluation framework, DeepCRCEval, integrates human evaluators and Large Language Models (LLMs) for a comprehensive reassessment of current techniques based on the criteria set. Besides, we also introduce an innovative and efficient baseline, LLM-Reviewer, leveraging the few-shot learning capabilities of LLMs for a target-oriented comparison. Our research highlights the limitations of text similarity metrics, finding that less than 10% of benchmark comments are high quality for automation. In contrast, DeepCRCEval effectively distinguishes between high and low-quality comments, proving to be a more reliable evaluation mechanism. Incorporating LLM evaluators into DeepCRCEval significantly boosts efficiency, reducing time and cost by 88.78% and 90.32%, respectively. Furthermore, LLM-Reviewer demonstrates significant potential of focusing task real targets in comment generation.
Tabular reinforcement learning methods cannot operate directly on continuous state spaces. One solution to this problem is to partition the state space. A good partitioning enables generalization during learning and more efficient exploitation of prior experiences. Consequently, the learning process becomes faster and produces more reliable policies. However, partitioning introduces approximation, which is particularly harmful in the presence of nonlinear relations between state components. An ideal partition should be as coarse as possible, while capturing the key structure of the state space for the given problem. This work extracts partitions from the environment dynamics by symbolic execution. We show that symbolic partitioning improves state space coverage with respect to environmental behavior and allows reinforcement learning to perform better for sparse rewards. We evaluate symbolic state space partitioning with respect to precision, scalability, learning agent performance and state space coverage for the learned policies.
KLEEF is a complete overhaul of the KLEE symbolic execution engine for LLVM , fine-tuned for a robust analysis of industrial C/C++ code. KLEEF natively handles complex data structures, such as trees, linked lists, and dynamically allocated arrays, via lazy initialization and symcrete values. KLEEF has fine-tuned modes for both maximal test coverage generation and reproducing error traces, in particular reaching a specific point in the program. In the paper, we describe the above features and a competition configuration of KLEEF .
In recent years, more people have seen their work depend on data manipulation tasks. However, many of these users do not have the background in programming required to write complex programs, particularly SQL queries. One way of helping these users is automatically synthesizing the SQL query given a small set of examples. Several program synthesizers for SQL have been recently proposed, but they do not leverage multicore architectures. This paper proposes Cubes , a parallel program synthesizer for the domain of SQL queries using input-output examples. Since input-output examples are an under-specification of the desired SQL query, sometimes, the synthesized query does not match the user’s intent. Cubes incorporates a new disambiguation procedure based on fuzzing techniques that interacts with the user and increases the confidence that the returned query matches the user intent. We perform an extensive evaluation on around 4000 SQL queries from different domains. Experimental results show that our parallel approach can scale up to 16 processes with super-linear speedups for many hard instances, and that our disambiguation approach is critical to achieving an accuracy of around 60%, significantly larger than other SQL synthesizers.
Maintaining software is cumbersome when method argument constraints are undocumented. To reveal them, previous work learned preconditions from exemplary valid and invalid method arguments. In practice, it would be highly beneficial to know class invariants, too, because functionality added during software maintenance must not break them. Even more so than method preconditions, class invariants are rarely documented and often cannot completely be inferred automatically, especially for objects exhibiting complex state such as dynamic data structures. This paper presents a novel dynamic approach to learning class invariants, thereby complementing related work on learning method preconditions. We automatically synthesize assertions from an adjustable assertion grammar to distinguish valid and invalid objects. While random walks generate valid objects, a combination of bounded-exhaustive testing techniques and behavioral oracles yield invalid objects. The utility of our approach for code comprehension and software maintenance is demonstrated by comparing our learned invariants to documented invariant validation methods found in real-world Java classes and to the invariants detected by the Daikon tool.
Deductive verification tools can prove a large range of program properties, but often face issues on recursive data structures. Abstract interpretation tools based on separation logic and shape analysis can efficiently reason about such structures but cannot deal with so large classes of properties. This short paper presents an ongoing work on combining both techniques. We show how a deductive verifier for C programs, Frama-C / Wp , can benefit from a shape analysis tool, MemCAD , where structural and separation properties proved in the latter become assumptions for the former. A case study on selected functions of the tpm2-tss library using linked lists confirms the interest of the approach.
