Název: Preprocesor Java bytecode pro verifikační nástroje
Překlad názvu: Java Bytecode Preprocessor for Program Verification Tools
Autoři: Šafařík, Tomáš ; Parízek, Pavel (vedoucí práce) ; Hnětynka, Petr (oponent)
Typ dokumentu: Diplomové práce
Rok: 2016
Jazyk: cze
Abstrakt: [cze] [eng]
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) Both J2BP and PANDA tools verify compiled Java programs. By now, these tools are not able to process some programs with specific JVM bytecode instruction sequences in the correct way. We described these instruction sequences and proposed their transformations. We developed the new application, called BytecodeTransformer, based on these propositions. This application transforms compiled Java programs and replaces the problematic instruction sequences with some others. Usage of BytecodeTransformer enlarges the set of programs that can be verified by both J2BP and PANDA. We also evaluated BytecodeTransformer on several Java programs, including own tests and well-known open-source programs. These tests demonstrated the correct functionality of BytecodeTransformer. Powered by TCPDF (www.tcpdf.org)
Klíčová slova: bytecode; Java; JVM; transformace kódu; verifikace programů; bytecode; code transformation; Java; JVM; program verification

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/78434

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-490717


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce