Machine learning for classification has seen numerous applications to complex, real-world tasks. Learned classifiers have become important artifacts of software systems that, like code, require careful analyses, maintenance, and evolution. Existing work on the formal verification of learned classifiers has mainly focused on the properties of individual classifiers, e.g., safety, fairness, or robustness, but not on analyzing the commonalities and differences of multiple classifiers. We present MLDiff, a novel approach to comparing learned classifiers based on querying agreements and disagreements between classifications, where one classifier is an alternative or variant of another. We present a prototypical implementation that leverages an encoding to SMT and can discover differences not (yet) seen in available datasets. Our prototype implements MLDiff for any combination of Decision Trees, Linear Support Vector Classification, Logistic Regression Classification, and Neural Networks. We evaluate it on classifiers trained on popular datasets in terms of performance and effectiveness of the analysis to discover disagreements between classifiers.
The design of complex cyber-physical systems increasingly relies on heterogeneous, multi-domain models, each capturing different system aspects. As these models evolve independently, inconsistencies may arise. Such inconsistencies remain difficult to detect due to gaps between the modelling domains. We propose to bridge this gap by introducing a formal notion of observables, inspired by physics, as measurable system properties, such that every model can constrain the possible values of an observable. We define a semantic framework where observables induce consistency relations and show that any such relation can be expressed using suitable observable semantics. To capture realistic engineering scenarios, we extend the framework with meta-model spanning and compound observable semantics, enabling the modular construction of complex constraints. We also provide encodings of these observable semantics back into the original framework, preserving the original results and showing that extensions remain expressively equivalent to initial ones. Finally, we discuss some practical implications of our framework, namely how observables can support cross-domain communication, separation of concerns, and extensibility, allowing consistency requirements to evolve as part of the modelling process.
Solidity, the most popular smart contract language, has two different kinds of data areas, called storage and memory. Storage is persistent across transactions and stored in the blockchain, while memory is volatile and does not survive a transaction. In storage, data structures are of value kind, with deep copy and no aliasing. In memory, data structures are of reference kind, with shallow copy and potential aliasing. We are concerned with deductive verification of smart contracts written in Solidity. Hence, we provide a logic formalisation of both data areas supporting efficient representation of the data areas, striking a balance between term size and on-demand case distinctions. We present a formalisation of the Solidity data types in both storage and memory, meeting the stated objectives. Specifically, we detail our representation of these data areas, discussing their differences and the challenges we encountered, such as value vs. reference semantics, object identity creation, and eager vs. lazy evaluation to delay proof effort until necessary.
Class invariants characterize valid object states throughout an object’s lifecycle and play an important role for software maintenance and evolution. Because invariants are rarely documented, software engineers resort to modern data-driven techniques for their inference. Recent automatic techniques require representative sets of invalid objects as negative training examples, which are hard to come by for programs with reference-based data structures such as search trees. For example, techniques adopting program mutation invalidate search tree objects well wrt. their payload, but they fail to introduce cycles, despite acyclicity being an important property of trees. In this paper, we analyze the limitations of program mutation for constructing invalid objects and propose state mutation as a complementary approach. Our approach first retrieves valid objects from program executions and then systematically mutates object references to obtain structurally invalid objects. An evaluation on a benchmark of diverse reference-based data structures shows that, unlike program mutation, state mutation effectively generates invalid objects with structural violations. Moreover, combining both approaches significantly outperforms either one and delivers diverse negative training examples that capture more facets of a given data structure, thereby permitting the inference of more precise class invariants.
Testing probabilistic programs is non-trivial due to their stochastic nature. Given an input, the program may produce different outcomes depending on the underlying stochastic choices in the program. This means testing the expected outcomes of probabilistic programs requires repeated test executions unlike deterministic programs where a single execution may suffice for each test input. This raises the following question: how many times should we run a probabilistic program to effectively test it? This work proposes a novel black-box unit testing method, ProbTest, for testing the outcomes of probabilistic programs. Our method is founded on the theory surrounding a well-known combinatorial problem, the coupon collector’s problem. Using this method, developers can write unit tests as usual without extra effort while the number of required test executions is determined automatically with statistical guarantees for the results. We implement ProbTest as a plug-in for PyTest, a well-known unit testing tool for python programs. Using this plug-in, developers can write unit tests similar to any other Python program and the necessary test executions are handled automatically. We evaluate the method on case studies from the Gymnasium reinforcement learning library and a randomized data structure.
