Derandomization with Pseudorandomness
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866918092006752256 |
|---|---|
| author | Karayel, Emin |
| author_facet | Karayel, Emin |
| contents | 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 deep algebraic/analytic results involved. 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 space-optimal distinct elements algorithm by Blasiok from 2018, which relies on the combination of many derandomization techniques to achieve its optimality. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_16614 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Derandomization with Pseudorandomness Karayel, Emin Logic in Computer Science 03B35, 68W20 G.3; F.4.1 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 deep algebraic/analytic results involved. 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 space-optimal distinct elements algorithm by Blasiok from 2018, which relies on the combination of many derandomization techniques to achieve its optimality. |
| title | Derandomization with Pseudorandomness |
| topic | Logic in Computer Science 03B35, 68W20 G.3; F.4.1 |
| url | https://arxiv.org/abs/2404.16614 |