A model checker for Java bytecode, with novel applications

In this work, we have designed and developed an automated static program analysis tool which can check whether the given program satisfies the required safety properties for the Java bytecode. Using the combination of model checker and symbolic execution with lazy abstraction, we have been successful to validate whether a program satisfies the given properties or not.

Level thesis:degree_level

Masters

Department dc:contributor.department

Computer Science

Grantor dc:publisher

Georgia Institute of Technology

Year dc:date.issued

2017

Author dc:creator

• Sahin, Burak

Advisor dc:contributor.advisor

• Harris, William

Committee members dc:contributor.committeemember

• Orso, Alessandro
• Esmaeilzadeh, Hadi

• Program analysis
• Program verification
• Model checking
• Formal methods
• Interpolation

Language dc:language.iso

en_US

Handle dc:identifier.uri

http://hdl.handle.net/1853/58686

OAI identifier oai:identifier

oai:repository.gatech.edu:1853/58686