More Like this

1. Counterexample Classification

   https://doi.org/10.1007/978-3-030-92124-8_18  

   Vick, Cole; Kang, Eunsuk; Tripakis, Stavros (December 2021, International Conference on Software Engineering and Formal Methods)

   Calinescu, R.; Păsăreanu, C.S. (Ed.)

   In model checking, when a given model fails to satisfy the desired specification, a typical model checker provides a counterexample that illustrates how the violation occurs. In general, there exist many diverse counterexamples that exhibit distinct violating behaviors, which the user may wish to examine before deciding how to repair the model. Unfortunately, obtaining this information is challenging in existing model checkers since (1) the number of counterexamples may be too large to enumerate one by one, and (2) many of these counterexamples are redundant, in that they describe the same type of violating behavior. In this paper, we propose a technique called counterexample classification. The goal of classification is to partition the space of all counterexamples into a finite set of counterexample classes, each of which describes a distinct type of violating behavior for the given specification. These classes are then presented as a summary of possible violating behaviors in the system, freeing the user from manually having to inspect or analyze numerous counterexamples to extract the same information. We have implemented a prototype of our technique on top of an existing formal modeling and verification tool, the Alloy Analyzer, and evaluated the effectiveness of the technique on case studies involving the well-known Needham-Schroeder protocol with promising results. 

   more » « less
2. A counterexample to the HK-conjecture that is principal

   https://doi.org/10.1017/etds.2022.25  

   DEELEY, ROBIN J. (June 2023, Ergodic Theory and Dynamical Systems)

   Abstract Scarparo has constructed counterexamples to Matui’s HK-conjecture. These counterexamples and other known counterexamples are essentially principal but not principal. In the present paper, a counterexample to the HK-conjecture that is principal is given. Like Scarparo’s original counterexample, our counterexample is the transformation groupoid associated to a particular odometer. However, the relevant group is the fundamental group of a flat manifold (and hence is torsion-free) and the associated odometer action is free. The examples discussed here do satisfy the rational version of the HK-conjecture. 

   more » « less
3. Counterexample-guided data augmentation

   Dreossi, Tommaso; Ghosh, Shromona; Yue, Xiangyu; Keutzer, Kurt; Sangiovanni-Vincentelli, Alberto L; Seshia, Sanjit A. (July 2018, Proceedings of the ... International Conference on Artificial Intelligence)

   We present a novel framework for augmenting data sets for machine learning based on counterexamples. Counterexamples are misclassified examples that have important properties for retraining and improving the model. Key components of our framework include a counterexample generator, which produces data items that are misclassified by the model and error tables, a novel data structure that stores information pertaining to misclassifications. Error tables can be used to explain the model's vulnerabilities and are used to efficiently generate counterexamples for augmentation. We show the efficacy of the proposed framework by comparing it to classical augmentation techniques on a case study of object detection in autonomous driving based on deep neural networks. 

   more » « less
4. Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification

   https://doi.org/10.1007/978-3-031-30820-8_19  

   Jaber, Nouraldin; Wagner, Christopher; Jacobs, Swen; Kulkarni, Milind; Samanta, Roopsha (April 2023, Tools and Algorithms for the Construction and Analysis of Systems)

   Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class. In this paper, we present a synthesis-driven tool, CINNABAR, to help system designers building DAB systems ensure that their intended designs belong to an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, CINNABAR generates sketch completions using a counterexample-guided procedure. The core technique relies on compactly encoding root-causes of counterexamples to varied properties such as efficient-decidability and safety. We demonstrate CINNABAR ’s effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems including a distributed key-value store and a distributed consortium system. 

   more » « less
5. Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems

   Haojun Ma; Hammad Ahmad; Aman Goel; Eli Goldweber; Jean-Baptiste Jeannin; Manos Kapritsos; Baris Kasikci (July 2022, 2022 USENIX Annual Technical Conference)

   Distributed systems are hard to design and implement correctly. Recent work has tried to use formal verification techniques to provide rigorous correctness guarantees. These works present a hard choice, though. One must either opt for the power of refinement-based approaches like IronFleet and Verdi, at the cost of large amounts of manual effort; or choose the more automated approach of I4, IC3PO, SWISS and DistAI which give up the ability to prove refinement and the power and scalability that come with it. We propose an alternative approach, Sift, that combines the power of refinement with the ability to automate proofs. Sift is a two-tier methodology that uses a new technique, refinement-guided automation, to leverage automation in a refinement proof and a divide-and-conquer technique to split a system into more refinement layers when necessary. This combination advances the frontier of what systems can be proven correct using a high degree of automation. Contrary to what was possible before, our evaluation shows that our novel approach allows us to prove the correctness of a number of systems with little manual effort, and to extend our proofs to include not just the protocols, but also an executable distributed implementation of these systems. 

   more » « less