|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
|
|
|
Static Analysis Using Facebook Infer Focused on Deadlock Detection
Marcin, Vladimír ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
|
|
|
Static Analysis Using Facebook Infer Focused on Deadlock Detection
Marcin, Vladimír ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.
|
guest ::
