{"id":{"repo_id":"gatech","oai_identifier":"oai:repository.gatech.edu:1853/58686"},"canonical_url":"https://search.dev.ndltd.org/etd/gatech/oai:repository.gatech.edu:1853/58686","repository":{"repo_id":"gatech","name":"Georgia Tech","base_url":"https://repository.gatech.edu/server/oai/request"},"display":{"title":"A model checker for Java bytecode, with novel applications","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Sahin, Burak"],"institution":"Georgia Institute of Technology","degree_name":null,"degree_level":"Masters","degree_discipline":null,"degree_department":"Computer Science","school":null,"contributors":[],"advisors":["Harris, William"],"committee_chairs":[],"committee_members":["Orso, Alessandro","Esmaeilzadeh, Hadi"],"year":2017,"date_issued":"2017-08-01","date_published":"2017-08-01","updated_at":"2026-07-27T19:49:22Z","subjects":["Program analysis","Program verification","Model checking","Formal methods","Interpolation"],"languages":["en_US"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1853/58686","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Harris, William"]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Orso, Alessandro","Esmaeilzadeh, Hadi"]},{"key":"dc:contributor.department","label":"Department","values":["Computer Science"]},{"key":"dc:creator","label":"Author","values":["Sahin, Burak"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2017-08-17T18:59:49Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2017-08-17T18:59:49Z"]},{"key":"dc:date.issued","label":"Date","values":["2017-08-01"]},{"key":"dc:publisher","label":"Institution","values":["Georgia Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Text"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Program analysis","Program verification","Model checking","Formal methods","Interpolation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en_US"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1853/58686"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M.S."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["A model checker for Java bytecode, with novel applications"]}]}],"canonical_facts":{"dc:contributor.advisor":["Harris, William"],"dc:contributor.committeemember":["Orso, Alessandro","Esmaeilzadeh, Hadi"],"dc:contributor.department":["Computer Science"],"dc:creator":["Sahin, Burak"],"dc:date.accessioned":["2017-08-17T18:59:49Z"],"dc:date.available":["2017-08-17T18:59:49Z"],"dc:date.issued":["2017-08-01"],"dc:description.abstract":["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."],"dc:description.degree":["M.S."],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/1853/58686"],"dc:language.iso":["en_US"],"dc:publisher":["Georgia Institute of Technology"],"dc:subject":["Program analysis","Program verification","Model checking","Formal methods","Interpolation"],"dc:title":["A model checker for Java bytecode, with novel applications"],"dc:type":["Text"],"thesis:degree_level":["Masters"]},"updated_at":"2026-07-27T19:49:22Z"}