Národní úložiště šedé literatury Nalezeno 3 záznamů.  Hledání trvalo 0.00 vteřin. 
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Modern software systems often use concurrent programs to improve performance and increase efficiency. However, ensuring the reliability and safety of such systems can be challenging due to the increased potential for bugs, including data races, to arise. In this thesis, we introduce a new static data race detector, DarC, designed for programs written in C using the Pthreads library. The proposed detector is implemented as an analyser plugin in Meta Infer, a static analysis framework with an emphasis on compositional, incremental, and consequently highly-scalable analysis. Our approach involves recording a set of accesses that occur in the analysed program along with information about the set of locks held during these accesses. The tool then identifies pairs of accesses that may lead to data races and reports them to the user. Our tool was successfully evaluated on a set of benchmarking programs as well as on real-life projects, showing its potential for effectively detecting data races in C programs.
Preprocesor Java bytecode pro verifikační nástroje
Šafařík, Tomáš ; Parízek, Pavel (vedoucí práce) ; Hnětynka, Petr (oponent)
Nástroje J2BP a PANDA umožňují verifikovat zkompilované Java programy. V současné době tyto nástroje nejsou schopny správně zpracovat programy s určitými sekvencemi instrukcí JVM bytecodu. Tyto sekvence instrukcí jsme popsali a navrhli jejich transformace. Na základě těchto návrhů jsme implementovali novou aplikaci BytecodeTransformer. Tato aplikace transformuje zkompilované Java programy a nahrazuje v nich problematické sekvence instrukcí bytecodu. Díky tomu se tedy rozšířila množina programů, které nástroje J2BP a PANDA dokážou verifikovat. Dále jsme vyhodnotili aplikaci BytecodeTransformer prostřednictvím našich i cizích Java programů. Tyto testy ukázaly správnou funkcionalitu implementované aplikace. Powered by TCPDF (www.tcpdf.org)
Preprocesor Java bytecode pro verifikační nástroje
Šafařík, Tomáš ; Parízek, Pavel (vedoucí práce) ; Hnětynka, Petr (oponent)
Nástroje J2BP a PANDA umožňují verifikovat zkompilované Java programy. V současné době tyto nástroje nejsou schopny správně zpracovat programy s určitými sekvencemi instrukcí JVM bytecodu. Tyto sekvence instrukcí jsme popsali a navrhli jejich transformace. Na základě těchto návrhů jsme implementovali novou aplikaci BytecodeTransformer. Tato aplikace transformuje zkompilované Java programy a nahrazuje v nich problematické sekvence instrukcí bytecodu. Díky tomu se tedy rozšířila množina programů, které nástroje J2BP a PANDA dokážou verifikovat. Dále jsme vyhodnotili aplikaci BytecodeTransformer prostřednictvím našich i cizích Java programů. Tyto testy ukázaly správnou funkcionalitu implementované aplikace. Powered by TCPDF (www.tcpdf.org)

Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.