dc.contributor.advisor | Kofroň, Jan | |
dc.creator | Zimen, Martin | |
dc.date.accessioned | 2023-11-06T22:36:30Z | |
dc.date.available | 2023-11-06T22:36:30Z | |
dc.date.issued | 2023 | |
dc.identifier.uri | http://hdl.handle.net/20.500.11956/184306 | |
dc.description.abstract | NumPy programs can be hard to debug. Due to the dynamic nature of Python, a bug can manifest itself after a long time of run time. This causes the computation to crash, ditching all the progress. Existing static analysis tools can't detect NumPy-specific errors. We propose a solution that uses data-flow analysis combined with symbolic execution to detect ndarray shape mismatch errors. With a dynamic set of symbols, our method tracks ndarray dimensions and constraints between them throughout the program. It uses an SMT solver to solve the constraints and locate the bug. Our implementation understands core NumPy constructs and detects some shape mismatch errors for 1D and 2D ndarrays. | en_US |
dc.description.abstract | NumPy programy se těžko ladí. Kvůli dynamické povaze Pythonu se chyba často projeví až poté, co program delší dobu běží. Výpočet poté spadne a všechen výpočet je ztracen. Existující nástroje statické analýzy nedokážou poznat chyby specifické pro NumPy. Použili jsme data-flow analýzu zkombi- novanou se symbolickým vykonáváním programu k detekování chyb plynoucí z nevyhovujících tvarů matic. Naše metoda pomocí dynamické množiny sym- bolů sleduje ve vstupním program rozměry matic a vztahy mezi nimi. Ná- sledně pomocí SMT vyhodnotí, jestli jsou vztahy splnitelné, nebo jestli došlo k chybě a kde. Naše implementace rozumí základním NumPy konstrukcím a detekuje některé chyby pro pole a matice. | cs_CZ |
dc.language | Čeština | cs_CZ |
dc.language.iso | cs_CZ | |
dc.publisher | Univerzita Karlova, Matematicko-fyzikální fakulta | cs_CZ |
dc.subject | statická analýza|NumPy|data-flow analýza|symbolic execution | cs_CZ |
dc.subject | static analysis|NumPy|data-flow analysis|symbolic execution | en_US |
dc.title | Statická analýza NumPy programů | cs_CZ |
dc.type | bakalářská práce | cs_CZ |
dcterms.created | 2023 | |
dcterms.dateAccepted | 2023-09-07 | |
dc.description.department | Katedra distribuovaných a spolehlivých systémů | cs_CZ |
dc.description.department | Department of Distributed and Dependable Systems | en_US |
dc.description.faculty | Matematicko-fyzikální fakulta | cs_CZ |
dc.description.faculty | Faculty of Mathematics and Physics | en_US |
dc.identifier.repId | 257503 | |
dc.title.translated | Static Analysis of NumPy Programs | en_US |
dc.contributor.referee | Blicha, Martin | |
thesis.degree.name | Bc. | |
thesis.degree.level | bakalářské | cs_CZ |
thesis.degree.discipline | Informatika se specializací Systémové programování | cs_CZ |
thesis.degree.discipline | Computer Science with specialisation in Systems Programming | en_US |
thesis.degree.program | Informatika | cs_CZ |
thesis.degree.program | Computer Science | en_US |
uk.thesis.type | bakalářská práce | cs_CZ |
uk.taxonomy.organization-cs | Matematicko-fyzikální fakulta::Katedra distribuovaných a spolehlivých systémů | cs_CZ |
uk.taxonomy.organization-en | Faculty of Mathematics and Physics::Department of Distributed and Dependable Systems | en_US |
uk.faculty-name.cs | Matematicko-fyzikální fakulta | cs_CZ |
uk.faculty-name.en | Faculty of Mathematics and Physics | en_US |
uk.faculty-abbr.cs | MFF | cs_CZ |
uk.degree-discipline.cs | Informatika se specializací Systémové programování | cs_CZ |
uk.degree-discipline.en | Computer Science with specialisation in Systems Programming | en_US |
uk.degree-program.cs | Informatika | cs_CZ |
uk.degree-program.en | Computer Science | en_US |
thesis.grade.cs | Velmi dobře | cs_CZ |
thesis.grade.en | Very good | en_US |
uk.abstract.cs | NumPy programy se těžko ladí. Kvůli dynamické povaze Pythonu se chyba často projeví až poté, co program delší dobu běží. Výpočet poté spadne a všechen výpočet je ztracen. Existující nástroje statické analýzy nedokážou poznat chyby specifické pro NumPy. Použili jsme data-flow analýzu zkombi- novanou se symbolickým vykonáváním programu k detekování chyb plynoucí z nevyhovujících tvarů matic. Naše metoda pomocí dynamické množiny sym- bolů sleduje ve vstupním program rozměry matic a vztahy mezi nimi. Ná- sledně pomocí SMT vyhodnotí, jestli jsou vztahy splnitelné, nebo jestli došlo k chybě a kde. Naše implementace rozumí základním NumPy konstrukcím a detekuje některé chyby pro pole a matice. | cs_CZ |
uk.abstract.en | NumPy programs can be hard to debug. Due to the dynamic nature of Python, a bug can manifest itself after a long time of run time. This causes the computation to crash, ditching all the progress. Existing static analysis tools can't detect NumPy-specific errors. We propose a solution that uses data-flow analysis combined with symbolic execution to detect ndarray shape mismatch errors. With a dynamic set of symbols, our method tracks ndarray dimensions and constraints between them throughout the program. It uses an SMT solver to solve the constraints and locate the bug. Our implementation understands core NumPy constructs and detects some shape mismatch errors for 1D and 2D ndarrays. | en_US |
uk.file-availability | V | |
uk.grantor | Univerzita Karlova, Matematicko-fyzikální fakulta, Katedra distribuovaných a spolehlivých systémů | cs_CZ |
thesis.grade.code | 2 | |
uk.publication-place | Praha | cs_CZ |
uk.thesis.defenceStatus | O | |