Erik Miehling, Michael Desmond, Karthikeyan Natesan Ramamurthy, Elizabeth M. Daly, Kush R. Varshney, Eitan Farchi, Pierre Dognin, Jesus Rios, Djallel Bouneffouf, Miao Liu, Prasanna Sattigeri. Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers). 2025.

The softmax function is a ubiquitous component at the output of neural networks and increasingly in intermediate layers as well. This paper provides convex lower bounds and concave upper bounds on the softmax function, which are compatible with convex optimization formulations for characterizing neural networks and other ML models. We derive bounds using both a natural exponential-reciprocal decomposition of the softmax as well as an alternative decomposition in terms of the log-sum-exp function. The new bounds are provably and/or numerically tighter than linear bounds obtained in previous work on robustness verification of transformers. As illustrations of the utility of the bounds, we apply them to verification of transformers as well as of the robustness of predictive uncertainty estimates of deep ensembles.

We present a new model-based approach for testing systems that use sequences of actions and assertions as test vectors. Our solution includes a method for quantifying testing quality, a tool for generating high-quality test suites based on the coverage criteria we propose, and a framework for assessing risks. For testing quality, we propose a method that specifies generalized coverage criteria over sequences of actions, which extends previous approaches. Our publicly available tool demonstrates how to extract effective test suites from test plans based on these criteria. We also present a Bayesian approach for measuring the probabilities of bugs or risks, and show how this quantification can help achieve an informed balance between exploitation and exploration in testing. Finally, we provide an empirical evaluation demonstrating the effectiveness of our tool in finding bugs, assessing risks, and achieving coverage.

To make ML systems deployment ready, one of the prominent challenges is to debug the performance issues of the trained ML models. This can be done by associating the issues with a set of Data Slices - aggregates of validation data records - to help the developers investigate these technical issues at a deeper level of granularity. Since the possible number of data slices are exponential in number, there is a need to prioritize the order (i.e. ranking) of slices before presenting to the users. However, there does not exist any work that deals with ranking these automatically generated slices and we refer to this problem as the data slice ranking problem (DSRP). This problem is challenging to address as the top ranked slices should contain significant error concentration (i.e. number of mis-classified data points), be statistically significant (i.e. having large size), and be non-redundant (i.e. contain unique mis-classified data points). In this paper, we tackle this challenging problem by proposing a novel game theoretic framework building upon Shapley value concept to derive a rank order for a given collection of data slices. In particular, we formally present a scheme that explicitly accounts only for the error concentration and we refer to this as Shapley Slice Ranking with Error concentration (SSR-E). We then prove a few useful properties of this scheme. Using thorough experimentation on 7 open source data sets, we demonstrate the superior performance of SSR mechanism vis-à-vis two baseline methods.

Machine Learning (ML) based solutions are becoming increasingly popular and pervasive. When testing such solutions, there is a tendency to focus on improving the ML metrics such as the F1-score and accuracy at the expense of ensuring business value and correctness by covering business requirements. In this work, we adapt test planning methods of classical software to ML solutions. We use combinatorial modeling methodology to define the space of business requirements and map it to the ML solution data, and use the notion of data slices to identify the weaker areas of the ML solution and strengthen them. We apply our approach to three real-world case studies and demonstrate its value.

The ability to capture different levels of abstraction in a system model is especially important for remote integration, testing/verification, and manufacturing of cyber-physical systems (CPSs). However, the complexity of modelling and testing of CPSs makes these processes extremely prone to human error. In this paper we present our ongoing work on introducing human-centred considerations into modelling and testing of CPSs, which allow for agile iterative refinement processes of different levels of abstraction when errors are discovered or missing information is completed.

This special issue concerns a range of issues related to the development of concurrent programs. This is an important topic, because many systems are now either multi-threaded or distributed, and it is well known that concurrency makes testing, analysis and debugging significantly more complicated. Essentially, the alternative interleavings of events can lead to different behaviours, and so any analysis, debugging or testing technique must consider these interleavings. The interest in this topic is reflected in the larger than normal issue, which contains five papers. The papers fall into three groups: we start with a paper on debugging, then have two on static analysis techniques and finally have two on testing. All papers were reviewed in the normal way.

Combinatorial test design (CTD) is an effective test planning technique that reveals faulty feature interaction in a given system. The test space is modeled by a set of parameters, their respective values, and restrictions on the value combinations. A subset of the test space is then automatically constructed so that it covers all valid value combinations of every t parameters, where t is a user input. Various combinatorial testing tools exist, implementing different approaches to finding a set of tests that satisfies t-wise coverage. However, little consideration has been given to the process of defining the test space for CTD, which is usually a manual, labor-intensive, and error-prone effort. Potential errors include missing parameters and their values, wrong identification of parameters and of valid value combinations, and errors in the definition of restrictions that cause them not to capture the intended combinations. From our experience, lack of support for the test space definition process is one of the main obstacles in applying CTD to a wide range of testing domains.

Code coverage is a common aid in the testing process. It is generally used for marking the source code segments that were executed and, more importantly, those that were not executed.

We describe a version of review/inspection called selective homeworkless review. In these reviews, moderators are taught how to select artifacts for review and review methodologies with little or no preparation. Many review and inspection methodologies are known in the literature and used in industry with very good results. The main issue we faced was not how to tune an existing inspection methodology, but rather how to get people to seriously and continuously inspect their artifacts. With the shrinking of the release cycle, people try to avoid front-loaded methodologies such as reviews, which seem to waste time early on. This is true both at the organizational level, where the overall cost is considered and at the day-to-day level, where time for preparation needs to be found. Because the reasons for rejecting existing inspection techniques were more organizational than technical, the way our methodology overcomes these objections is as central to the paper as the selective homeworkless review methodology itself. We introduced selective homeworkless reviews three years ago. We now have convincing evidence that this methodology can be introduced even in organizations that are resistant to formal inspections, leading to significant improvements in quality.

PADTAD brings together researchers from academia and researchers and practitioners from industry to promote the development of techniques and tools that aid in testing, analysis, and debugging of multi-threaded/parallel/distributed software.

In simulation-based verification, we check the correctness of a given program by executing it on some input vectors. Even for medium-size programs, exhaustive testing is impossible. Thus, many errors are left undetected. The problem of increasing the exhaustiveness of testing and decreasing the number of undetected errors is the main problem of software testing. In this paper, we present a novel approach to software testing, which allows us to dramatically raise the probability of catching rare errors in large programs. Our approach is based on the cross-entropy method. We define a performance function, which is higher in the neighborhood of an error or a pattern we are looking for. Then, the program is executed many times, choosing input vectors from some random distribution. The starting distribution is usually uniform, and it is changed at each iteration based on the vectors with highest value of the performance function in the previous iteration. The crossentropy method was shown to be very efficient in estimating the probabilities of rare events and in searching for solutions for hard optimization problems. Our experiments show that the cross-entropy method is also very efficient in locating rare bugs and patterns in large programs.We show the experimental results of our cross-entropy based testing tool and compare them to the performance of ConTest and of Java scheduler.

Abstract The primary difficulty with testing concurrent programs is their non‐determinism, where two executions with the same input can yield different results due to a changed thread schedule (also known as interleaving). This problem is aggravated by the fact that most thread schedulers are almost deterministic, and generate the same interleavings over and over for a given testing environment. The traditional approach to testing concurrent programs is to identify and examine the race conditions. A different solution involves noise‐making, which generates different interleavings at runtime, for example, using embedded sleep statements. This paper proposes a totally different technique for generating a rich set of interleavings. In this approach, operations on shared variables are tracked. Every time a shared variable is read, the value to be read is selected from the set of values that were held by this variable during the program execution. The algorithm identifies those values that the variable could hold in some interleaving consistent with the past observed events. Within this subset, the value choice can be random, biased‐random, based on coverage, etc. The problem of identifying read values that are consistent with the past observations is far from simple, since past decisions on value selection affect future ones. Our solution is computationally intensive and, therefore, impractical as is. However, insights gained from this solution lead to new heuristics for noise‐making. Copyright © 2006 John Wiley & Sons, Ltd.

Abstract Desk checking is known to be an effective reading technique for early detection of sequential program errors. This paper discusses how to extend desk checking for concurrent and distributed programs. In addition to exponential possible schedules, concurrent and distributed programs have execution states that include more than one process. The new distributed desk‐checking technique supports the selection of schedules and execution states to be reviewed. The cross‐product functional coverage technique assists in the selection process. Schedule selection guidelines that facilitate early detection and coverage are introduced. It is demonstrated that code inspection can be applied effectively to large industrial applications using the selection mechanism introduced by this technique. Industrial pilots show that distributed desk checking is an effective early error‐detection review technique. Copyright © 2006 John Wiley & Sons, Ltd.

A noise maker is a tool that seeds a concurrent program with conditional synchronization primitives, such as yield(), for the purpose of increasing the likelihood that a bug manifest itself. We introduce a novel fault model that classifies locations as "good", "neutral", or "bad," based on the effect of a thread switch at the location. Using the model, we explore the terms under which an efficient search for real-life concurrent bugs can be conducted. We accordingly justify the use of probabilistic algorithms for this search and gain a deeper insight of the work done so far on noise- making. We validate our approach by experimenting with a set of programs taken from publicly available multi-threaded benchmarks. Our empirical evidence demonstrates that real-life behavior is similar to one derived from the model.

View-oriented group communication is an important and widely used building block for constructing highly-available fault-tolerant systems. Unfortunately, group-communication based systems are extremely hard to test and debug due to a number of stateful complex algorithms deployed in parallel and the unique combination of distributed and concurrent programming paradigms that amplifies the non-determinism in the system behavior. In this work, we elaborate on the specific challenges we encountered during the process of testing DCS, a group communication component of the WebSphere (WAS) architecture, as well as on the methodology we have devised and employed in order to cope with these challenges. Our solution relies on a carefully compiled set of invariants that need to be preserved at every execution point and a log analyzer algorithm that performs cross-log verification for all the processes participating in the execution, as well as on of other techniques whose details are described in the paper.

Coverage analysis is a useful testing technology. However, some coverage models are more acceptable to the industry than others. In the field of testing multi-threaded applications, there is a need for a coverage model that can be used to evaluate tests for concurrent completeness and to find new testing requirements. We present a new coverage model: synchronization coverage. This model is simple to understand and the action items generated by each uncovered task are clear to testers and developers. We propose that synchronization coverage could, and should, become one of the more commonly used coverage models.

Summary form only given. In previous work, we introduced the alternative pasts algorithm that delays the assignment of values to variables until their usage. Whenever a variable is used, the algorithm chooses one of its past values that is consistent with some possible execution. The alternative pasts algorithm can be seen as belonging to a class of algorithms that shadow the execution and choose at any point to modify the values of some of the variables. We build on this work and extend it in two directions. First we show a more powerful shadowing algorithm that can delay not only writes but also reads and other kinds of instructions, at most until a relevant control decision is taken, which is the longest possible delay for algorithms of this class. We prove that this algorithm inherits the ability of the alternative pasts algorithm to generate significantly different interleavings, which are guaranteed to execute differently. In addition, we show a new use for the two algorithms, namely alternative replay. Unlike regular replay, where the execution of the program is reproduced, alternative replay is an execution that did not happen before but could have happened. For example, if a bug did not materialize, alternative replay can be used to show the user alternative execution in which the impact of the bug can be observed.

Summary form only given. The paper describes a tool for black-box testing of UDP-based distributed Java programs. UDP provides little guarantee for correct delivery of data, and therefore requires the application to verify the integrity of communication according to its needs. Debugging such application is hard, since it is hard to create at will bad network conditions. The tool describes here creates an intermediary layer above the Java API which simulates network noises. It therefore enables stress-testing the application even on a flawless network environment. We describe a field experience of testing an application, using the tool vs. using specially-written testing code. We show the two approaches to be complementary.

Summary form only given. This paper discusses how to extend desk checking for concurrent and distributed programs. In addition to unbounded possible schedules, concurrent and distributed programs have execution states that include more than one process. Schedule selection guidelines that facilitate early detection and coverage are introduced. The cross-product technique assists in the selection process. Industrial pilots show that concurrent desk checking is a promising review technique for early error detection.

Abstract Finding bugs due to race conditions in multi‐threaded programs is difficult, mainly because there are many possible interleavings, any of which may contain a fault. In this work we present a methodology for testing multi‐threaded programs which has minimal impact on the user and is likely to find interleaving bugs. Our method reruns existing tests in order to detect synchronization faults. We find that a single test executed a number of times in a controlled environment may be as effective in finding synchronization faults as many different tests. A great deal of resources are saved since tests are very expensive to write and maintain. We observe that simply rerunning tests, without ensuring in some way that the interleaving will change, yields almost no benefits. We implement the methodology in our test generation tool—ConTest. ConTest combines the replay algorithm, which is essential for debugging, with our interleaving test generation heuristics. ConTest also contains an instrumentation engine, a coverage analyzer, and a race detector (not finished yet) that enhance bug detection capabilities. The greatest advantage of ConTest, besides finding bugs of course, is its minimal effect on the user. When ConTest is combined into the test harness, the user may not even be aware that ConTest is being used. Copyright © 2003 John Wiley & Sons, Ltd.

This work describes an automatic query refinement technique, which focuses on improving precision of the top ranked documents. The terms used for refinement are lexical affinities (LAs), pairs of closely related words which contain exactly one of the original query terms. Adding these terms to the query is equivalent to re-ranking search results, thus, precision is improved while recall is preserved. We describe a novel method that selects the most informative LAs for refinement, namely, those LAs that best separate relevant documents from irrelevant documents in the set of results. The information gain of candidate LAs is determined using unsupervised estimation that is based on the scoring function of the search engine. This method is thus fully automatic and its quality depends on the quality of the scoring function. Experiments we conducted with TREC data clearly show a significant improvement in the precision of the top ranked documents.

We introduce static index pruning methods that significantly reduce the index size in information retrieval systems.We investigate uniform and term-based methods that each remove selected entries from the index and yet have only a minor effect on retrieval results. In uniform pruning, there is a fixed cutoff threshold, and all index entries whose contribution to relevance scores is bounded above by a given threshold are removed from the index. In term-based pruning, the cutoff threshold is determined for each term, and thus may vary from term to term. We give experimental evidence that for each level of compression, term-based pruning outperforms uniform pruning, under various measures of precision. We present theoretical and experimental evidence that under our term-based pruning scheme, it is possible to prune the index greatly and still get retrieval results that are almost as good as those based on the full index.

It is well known that the optimal solution for searching in a finite total order set is binary search. In binary search we divide the set into two "halves" by querying the middle element and continue the search on the suitable half. What is the equivalent of binary search when the set P is partially ordered? A query in this case is to a point $x\in P$, with two possible answers: "yes" indicates that the required element is "below" x or "no" if the element is not below x. We show that the problem of computing an optimal strategy for search in posets that are tree-like (or forests) is polynomial in the size of the tree and requires at most O(n 4 log 3 n ) steps. Optimal solutions of such search problems are often needed in program testing and debugging, where a given program is represented as a tree and a bug should be found using a minimal set of queries. This type of search is also applicable in searching classified large tree-like databases (e.g., the Internet).