Abstract: This talk shall be in the domain of Formal Methods. It shall briefly highlight one of the techniques in this area and a domain it is applied to. The technique is based out of ideas from symbolic simulation. And the area where it will be applied is to Error Correction coding schemes. Hope you guys will get to witness a day in the life of a Formal Verification Engineer -- the non insta version!

Abstract: We study a one-parameter family of zero-sum games arising from electoral competition with abstention. Two parties choose positions on a policy line; voters vote for the nearest party within a tolerance radius and otherwise abstain, while parties compete on plurality.

For general voter densities, the existence of a pure-strategy Nash equilibrium need not be monotone in the tolerance radius: an equilibrium may exist, disappear, and later reappear. We identify a geometric property of the winning correspondence, called centripetal structure, that behaves differently: once it appears, it persists as tolerance increases and guarantees a pure-strategy Nash equilibrium.

Preprint: (joint work with Aman Ray, BA, 3rd year, MSE) https://arxiv.org/pdf/2608.03788