Computing devices and information systems have become ubiquitous. As their use broadens, a host of diverse requirements and considerations about their behaviours arise. This in turns creates a need for software analysis tools. In particular we are interested in techniques that are formal, static, and systematic.

Because of well-known impossibility results (e.g. Rice’s theorem), we cannot hope for a single “one-size-fits-all” approach. Indeed, as soon as a verification framework gets expressive enough, it become algorithmically intractable. The workaround is to rely instead on a variety of specialised analysis tools. The drawback is that any serious system analysis requires several such tools, and more often than not ends up developing ad-hoc variants of existing tools to better exploit the specifics of the system under study.

Therefore we believe new tools, models, and techniques for system analysis will continue being developed for the foreseeable future, in order to tackle new systems, new considerations, and new programming features. For these reasons, we want to provide better frameworks for building verification tools. More specifically, we are interested in ways to combine existing tools to produce new ones. Doing so, we wish to be able to derive the correctness of the composite tool from that of its constituting elements.

In this talk, I will propose such a framework, and argue it is able to capture a broad class of verification models, as well as useful proof techniques. This talk will be based on unpublished ongoing work.

The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a very hard problem in the discrepancy community. Indeed, provably optimal point sets were known, up to now, only for up to 6 points in dimension 2 and up to two points in higher dimensions.
In this talk, we will present different approaches to construct low discrepancy point sets. We first introduce mathematical programming formulations to construct point sets with optimal $L_{\infty}$ star discrepancy values in dimension 2 for up to 21 points and up to 8 points in dimension 3. We show that these optimal sets have a far lower discrepancy than the previous references. More importantly, they present a very different structure. [PAMS: doi.org/10.1090/bproc/254]
We will then discuss extensions of this approach to obtain good, but not provably optimal, point sets and show that there is much room for improvement over state-of-the-art constructions. We also show that additional symmetry requirements can be satisfied at very small loss in discrepancy value.
Finally, we will discuss some recent advances using graph neural networks by Rusch et al. [PNAS: https://www.pnas.org/doi/10.1073/pnas.2409913121] and how we outperform these constructions using classic optimization approaches [PNAS: https://www.pnas.org/doi/abs/10.1073/pnas.2424464122].
The presentation is based on joint work with François Clément (University of Washington, US), Kathrin Klamroth (University of Wuppertal, Germany), and Luís Paquete (University of Coimbra, Portugal).