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. Counterexamples to the tilting and (p,r)-filtration conjectures

   https://doi.org/10.1515/crelle-2019-0036  

   Bendel, Christopher P.; Nakano, Daniel K.; Pillen, Cornelius; Sobaje, Paul (November 2019, Journal für die reine und angewandte Mathematik (Crelles Journal))

   Abstract In this paper the authors produce a projective indecomposable module for the Frobenius kernel of a simple algebraic group in characteristic p that is not the restriction of an indecomposable tilting module. This yields a counterexample to Donkin’s longstanding Tilting Module Conjecture. The authors also produce a Weyl module that does not admit a p -Weyl filtration. This answers an old question of Jantzen, and also provides a counterexample to the {(p,r)} -Filtration Conjecture. 

   more » « less
3. Dynamic asymptotic dimension and Matui's HK conjecture

   https://doi.org/10.1112/plms.12510  

   Bönicke, Christian; Dell'Aiera, Clément; Gabe, James; Willett, Rufus (January 2023, Proceedings of the London Mathematical Society)

   Abstract We prove that the homology groups of a principal ample groupoid vanish in dimensions greater than the dynamic asymptotic dimension of the groupoid (as a side‐effect of our methods, we also give a new model of groupoid homology in terms of the Tor groups of homological algebra, which might be of independent interest). As a consequence, the K‐theory of the ‐algebras associated with groupoids of finite dynamic asymptotic dimension can be computed from the homology of the underlying groupoid. In particular, principal ample groupoids with dynamic asymptotic dimension at most two and finitely generated second homology satisfy Matui's HK‐conjecture. We also construct explicit maps from the groupoid homology groups to the K‐theory groups of their ‐algebras in degrees zero and one, and investigate their properties. 

   more » « less
4. On Bourgain’s Counterexample for the Schrödinger Maximal Function

   https://doi.org/10.1093/qmath/haaa032  

   Pierce, Lillian B (November 2020, The Quarterly Journal of Mathematics)

   null (Ed.)

   Abstract This paper provides a rigorous derivation of a counterexample of Bourgain, related to a well-known question of pointwise a.e. convergence for the solution of the linear Schrödinger equation, for initial data in a Sobolev space. This counterexample combines ideas from analysis and number theory, and the present paper demonstrates how to build such counterexamples from first principles, and then optimize them. 

   more » « less
5. CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples

   https://doi.org/10.1145/3372297.3417282  

   Wang, Yuxin; Ding, Zeyu; Kifer, Daniel; Zhang, Danfeng (October 2020, CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security)

   null (Ed.)

   We propose CheckDP, an automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Furthermore, it was able to automatically generate proofs for correct mechanisms for which no formal verification was reported before. CheckDP is built on static program analysis, allowing it to be more efficient and precise in catching infrequent events than sampling based counterexample generators (which run mechanisms hundreds of thousands of times to estimate their output distribution). Moreover, its sound approach also allows automatic verification of correct mechanisms. When evaluated on standard benchmarks and newer privacy mechanisms, CheckDP generates proofs (for correct mechanisms) and counterexamples (for incorrect mechanisms) within 70 seconds without any false positives or false negatives. 

   more » « less