Derandomization techniques are often used within advanced randomized algorithms. In particular, pseudorandom objects, such as hash families and expander graphs, are key components of such algorithms, but their verification presents a challenge. This work shows how such algorithms can be expressed and verified in Isabelle and presents a pseudorandom objects library that abstracts away the involved deep algebraic/analytic results. Moreover, it presents examples that show how the library eases and enables the verification of advanced randomized algorithms. Highlighting the value of this framework is that it was recently used to verify the optimal-space distinct elements algorithm by Blasiok from 2018, which relies on the combination of many derandomization techniques to achieve its optimality.

翻译：去随机化技术常用于高级随机算法中。特别是，诸如哈希族和展开图之类的伪随机对象是此类算法的关键组成部分，但其验证存在挑战。本工作展示了如何在Isabelle中表达和验证此类算法，并提出一个伪随机对象库，该库抽象化了涉及的深层代数/分析结果。此外，通过示例展示了该库如何简化并支持高级随机算法的验证。该框架的价值在于，它最近被用于验证Blasiok在2018年提出的最优空间不同元素算法，该算法依赖多种去随机化技术的结合以实现其最优性。