-
HornFuzz: Fuzzing CHC solvers
Authors:
Anzhela Sukhanova,
Valentyn Sobol
Abstract:
Many advanced program analysis and verification methods are based on solving systems of Constrained Horn Clauses (CHC). Testing CHC solvers is very important, as correctness of their work determines whether bugs in the analyzed programs are detected or missed. One of the well-established and efficient methods of automated software testing is fuzzing: analyzing the reactions of programs to random i…
▽ More
Many advanced program analysis and verification methods are based on solving systems of Constrained Horn Clauses (CHC). Testing CHC solvers is very important, as correctness of their work determines whether bugs in the analyzed programs are detected or missed. One of the well-established and efficient methods of automated software testing is fuzzing: analyzing the reactions of programs to random input data. Currently, there are no fuzzers for CHC solvers, and fuzzers for SMT solvers are not efficient in CHC solver testing, since they do not consider CHC specifics. In this paper, we present HornFuzz, a mutation-based gray-box fuzzing technique for detecting bugs in CHC solvers based on the idea of metamorphic testing. We evaluated our fuzzer on one of the highest performing CHC solvers, Spacer, and found a handful of bugs in Spacer. In particular, some discovered problems are so serious that they require fixes with significant changes to the solver.
△ Less
Submitted 8 June, 2023; v1 submitted 7 June, 2023;
originally announced June 2023.
-
TiCo: Transformation Invariance and Covariance Contrast for Self-Supervised Visual Representation Learning
Authors:
Jiachen Zhu,
Rafael M. Moraes,
Serkan Karakulak,
Vlad Sobol,
Alfredo Canziani,
Yann LeCun
Abstract:
We present Transformation Invariance and Covariance Contrast (TiCo) for self-supervised visual representation learning. Similar to other recent self-supervised learning methods, our method is based on maximizing the agreement among embeddings of different distorted versions of the same image, which pushes the encoder to produce transformation invariant representations. To avoid the trivial solutio…
▽ More
We present Transformation Invariance and Covariance Contrast (TiCo) for self-supervised visual representation learning. Similar to other recent self-supervised learning methods, our method is based on maximizing the agreement among embeddings of different distorted versions of the same image, which pushes the encoder to produce transformation invariant representations. To avoid the trivial solution where the encoder generates constant vectors, we regularize the covariance matrix of the embeddings from different images by penalizing low rank solutions. By jointly minimizing the transformation invariance loss and covariance contrast loss, we get an encoder that is able to produce useful representations for downstream tasks. We analyze our method and show that it can be viewed as a variant of MoCo with an implicit memory bank of unlimited size at no extra memory cost. This makes our method perform better than alternative methods when using small batch sizes. TiCo can also be seen as a modification of Barlow Twins. By connecting the contrastive and redundancy-reduction methods together, TiCo gives us new insights into how joint embedding methods work.
△ Less
Submitted 23 June, 2022; v1 submitted 21 June, 2022;
originally announced June 2022.
-
A New Model for the Collective Beam-Beam Interaction
Authors:
J. A. Ellison,
A. V. Sobol,
M Vogt
Abstract:
The Collective Beam-Beam interaction is studied in the framework of maps with a ``kick-lattice'' model in the 4-D phase space of the transverse motion. A novel approach to the classical method of averaging is used to derive an approximate map which is equivalent to a flow within the averaging approximation. The flow equation is a continuous-time Vlasov equation which we call the averaged Vlasov…
▽ More
The Collective Beam-Beam interaction is studied in the framework of maps with a ``kick-lattice'' model in the 4-D phase space of the transverse motion. A novel approach to the classical method of averaging is used to derive an approximate map which is equivalent to a flow within the averaging approximation. The flow equation is a continuous-time Vlasov equation which we call the averaged Vlasov equation, the new model of this paper. The power of this approach is evidenced by the fact that the averaged Vlasov equation has exact equilibria and the associated linearized equations have uncoupled azimuthal Fourier modes. The equation for the Fourier modes leads to a Fredholm integral equation of the third kind and the setting is ready-made for the development of a weakly nonlinear theory to study the coupling of the pi and sigma modes. The pi and sigma eigenmodes are calculated from the third kind integral equation. These results are compared with the kick-lattice model using our weighted macroparticle tracking code and a newly developed, density tracking, parallel, Perron-Frobenius code.
△ Less
Submitted 24 November, 2006;
originally announced November 2006.
