{"677284":{"#nid":"677284","#data":{"type":"news","title":"Award-winning Software Tool Uses Innovative Approach","body":[{"value":"\u003Cp\u003ESchool of Computer Science Professor \u003Ca href=\u0022https:\/\/vganesh1.github.io\/\u0022\u003E\u003Cstrong\u003EVijay Ganesh\u003C\/strong\u003E\u003C\/a\u003E is leading the way in the innovation of SMT solvers, a class of tools key to software engineering, security, and trustworthy artificial intelligence (AI).\u003C\/p\u003E\u003Cp\u003EGanesh and his student, John Lu, have been working on their own solver, Z3-alpha, for several years. It recently won several categories at \u003Ca href=\u0022https:\/\/smt-comp.github.io\/2024\/\u0022\u003E\u003Cstrong\u003ESMT-COMP 2024\u003C\/strong\u003E\u003C\/a\u003E, a competition held to determine the best solvers from around the world.\u003C\/p\u003E\u003Cp\u003ESMT solvers are automated logical reasoning tools used widely to test and analyze programs. They are also used to identify potential security issues.\u003C\/p\u003E\u003Cp\u003E\u201cSMT solvers are like a Swiss Army Knife for all kinds of tasks for software engineering and trustworthy AI. You need a tool that can understand and analyze formulas obtained from analysis of programs,\u201d Ganesh said.\u003C\/p\u003E\u003Cp\u003EThe Z3-alpha solver is derived from the z3 solver from Microsoft Research, but Ganesh and Lu implemented machine learning (ML) into their solver to automatically synthesize strategies, making it more efficient.\u003C\/p\u003E\u003Cp\u003EGanesh said the solver illustrates one of his biggest research goals: effectively combining the fields of automated reasoning and ML.\u003C\/p\u003E\u003Cp\u003E\u201cWith this solver, we\u2019re using ML to make automated reasoning more efficient. In another line of research, we are going in the reverse direction by using automated reasoning to analyze, test, and improve ML models,\u201d he said.\u003C\/p\u003E\u003Cp\u003EUsing ML with SMT solvers this way is a relatively new line of research that Ganesh has been working on. He said this is among the first known instances of the successful use of machine learning for SMT solver strategy synthesis.\u003C\/p\u003E\u003Cp\u003EGanesh said they want to work to further improve the Z3-alpha solver and apply these ML techniques to other solvers.\u003C\/p\u003E","summary":"","format":"limited_html"}],"field_subtitle":"","field_summary":[{"value":"\u003Cp\u003ESchool of Computer Science Professor \u003Ca href=\u0022https:\/\/vganesh1.github.io\/\u0022\u003E\u003Cstrong\u003EVijay Ganesh\u003C\/strong\u003E\u003C\/a\u003E is leading the way in the innovation of SMT solvers, a class of tools key to software engineering, security, and trustworthy artificial intelligence (AI). His solver recently won several categories at \u003Ca href=\u0022https:\/\/smt-comp.github.io\/2024\/\u0022\u003E\u003Cstrong\u003ESMT-COMP 2024\u003C\/strong\u003E\u003C\/a\u003E, a competition held to determine the best solvers from around the world.\u003C\/p\u003E","format":"limited_html"}],"field_summary_sentence":[{"value":"School of Computer Science Professor Vijay Ganesh is leading the way in the innovation of SMT solvers, a class of tools key to software engineering, security, and trustworthy artificial intelligence (AI)."}],"uid":"36532","created_gmt":"2024-10-02 20:50:33","changed_gmt":"2024-10-02 20:56:21","author":"Morgan Usry","boilerplate_text":"","field_publication":"","field_article_url":"","dateline":{"date":"2024-10-02T00:00:00-04:00","iso_date":"2024-10-02T00:00:00-04:00","tz":"America\/New_York"},"extras":[],"hg_media":{"675201":{"id":"675201","type":"image","title":"Vijay Ganesh_86A0209.jpg","body":null,"created":"1727902245","gmt_created":"2024-10-02 20:50:45","changed":"1727902245","gmt_changed":"2024-10-02 20:50:45","alt":"Vijay Ganesh","file":{"fid":"258802","name":"Vijay Ganesh_86A0209.jpg","image_path":"\/sites\/default\/files\/2024\/10\/02\/Vijay%20Ganesh_86A0209.jpg","image_full_path":"http:\/\/hg.gatech.edu\/\/sites\/default\/files\/2024\/10\/02\/Vijay%20Ganesh_86A0209.jpg","mime":"image\/jpeg","size":47498,"path_740":"http:\/\/hg.gatech.edu\/sites\/default\/files\/styles\/740xx_scale\/public\/2024\/10\/02\/Vijay%20Ganesh_86A0209.jpg?itok=78ZtABVs"}}},"media_ids":["675201"],"groups":[{"id":"47223","name":"College of Computing"},{"id":"1188","name":"Research Horizons"},{"id":"50875","name":"School of Computer Science"}],"categories":[{"id":"153","name":"Computer Science\/Information Technology and Security"},{"id":"135","name":"Research"}],"keywords":[{"id":"10199","name":"Daily Digest"},{"id":"187915","name":"go-researchnews"},{"id":"187812","name":"artificial intelligence (AI)"}],"core_research_areas":[{"id":"193655","name":"Artificial Intelligence at Georgia Tech"}],"news_room_topics":[],"event_categories":[],"invited_audience":[],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[{"value":"\u003Cp\u003EMorgan Usry, Communications Officer at the School of Computer Science\u003C\/p\u003E","format":"limited_html"}],"email":["morgan.usry@cc.gatech.edu"],"slides":[],"orientation":[],"userdata":""}}}