{"id":34,"date":"2014-02-10T17:13:50","date_gmt":"2014-02-10T22:13:50","guid":{"rendered":"https:\/\/my.vanderbilt.edu\/simko\/?page_id=34"},"modified":"2014-04-02T01:43:55","modified_gmt":"2014-04-02T06:43:55","slug":"home","status":"publish","type":"page","link":"https:\/\/my.vanderbilt.edu\/simko\/","title":{"rendered":"Home"},"content":{"rendered":"<p><strong>Gabor Simko<\/strong><br \/>\nGraduate Research Assistant<br \/>\nInstitute for Software Integrated Systems<br \/>\nVanderbilt University<\/p>\n<p>Research areas<\/p>\n<ul>\n<li>Formal specification of languages<\/li>\n<li>Formal verification<\/li>\n<li>Domain Specific Modeling Languages<\/li>\n<li>Embedded software, Cyber-Physical Systems, Hybrid Systems<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h1>Formal semantic specifications of Cyber-Physical System modeling languages<\/h1>\n<p><a href=\"https:\/\/my.vanderbilt.edu\/simko\/specification\/\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-large wp-image-102\" src=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/cps-650x126.png\" alt=\"\" width=\"640\" height=\"124\" srcset=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/cps-650x126.png 650w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/cps-300x58.png 300w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/cps.png 1338w\" sizes=\"auto, (max-width: 640px) 100vw, 640px\" \/><\/a><\/p>\n<p>Cyber-Physical Systems (CPS) are integration of computational and physical systems. CPS-s have many safety-critical applications, such as traffic control, aviation, power and chemical plants, or medical devices. In order to support the development of safe CPS-s, we need to unambiguously define the semantics of the modeling languages used for designing them.\u00a0You can find more information about <a href=\"https:\/\/my.vanderbilt.edu\/simko\/specification\/\">this work here<\/a>.<\/p>\n<h1>Sahvy<\/h1>\n<p><a href=\"https:\/\/my.vanderbilt.edu\/simko\/sahvy\/\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-large wp-image-101\" src=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/acc1-650x165.png\" alt=\"\" width=\"640\" height=\"162\" srcset=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/acc1-650x165.png 650w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/acc1-300x76.png 300w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/acc1.png 1142w\" sizes=\"auto, (max-width: 640px) 100vw, 640px\" \/><\/a><\/p>\n<p>Sahvy is a tool for verifying sample and hold systems composed of a continuous-time physical plant and a periodic discrete-time software controller.<br \/>\nFor more information about the tool and to download it, please follow <a href=\"https:\/\/my.vanderbilt.edu\/simko\/sahvy\/\">this link<\/a>.<\/p>\n<h1>Formalized proof of the L* algorithm<\/h1>\n<p>I have formalized the proof for the original L* algorithm developed by Dana Angluin for learning an unknown automaton by examples using the PVS interactive theorem prover. The algorithm is described in the following paper:<\/p>\n<div style=\"margin-bottom: 15px;padding-left: 50px\">Angluin, D. (1987). Learning regular sets from queries and counterexamples. Information and computation, 75(2), 87-106.<\/div>\n<p>and our formalized proof is downloadable from here (to be published yet).<\/p>\n<h1>NetworGame<\/h1>\n<p><a href=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/NetworGame2.png\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter size-medium wp-image-104\" src=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/NetworGame2-300x195.png\" alt=\"\" width=\"300\" height=\"195\" srcset=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/NetworGame2-300x195.png 300w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/NetworGame2-650x423.png 650w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/NetworGame2.png 1251w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><br \/>\nNetworGame is a tool for running 2-player game theoretical simulations on arbitrary graphs. NetworGame has been used for analyzing nodes in protein structures and protein-protein interaction networks. Please see the official site of the tool <a href=\"http:\/\/www.linkgroup.hu\/NetworGame.php\">here<\/a>.<\/p>\n<h1>Bone shadow elimination<\/h1>\n<p><a href=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/boneshadow.png\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter size-large wp-image-106\" src=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/boneshadow-650x167.png\" alt=\"\" width=\"640\" height=\"164\" srcset=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/boneshadow-650x167.png 650w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/boneshadow-300x77.png 300w, https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/boneshadow.png 1490w\" sizes=\"auto, (max-width: 640px) 100vw, 640px\" \/><\/a><br \/>\nThe topic of my MSc thesis was collarbone detection and bone shadow elimination. Discussion of the topic is found in the following paper:<\/p>\n<div style=\"margin-bottom: 15px;padding-left: 50px\"><strong>Simko G.<\/strong>, Orban G., Maday P., Horvath G. (2009). Elimination of clavicle shadows to help automatic lung nodule detection on chest radiographs. In: 4th European Conference of the International Federation for Medical and Biological Engineering (EMBEC). Springer, pp.488\u2013491.<\/div>\n<h1>Smoke simulation<\/h1>\n<p><a href=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/bloggif_533bafe943bba.gif\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter size-full wp-image-128\" src=\"https:\/\/cdn.vanderbilt.edu\/t2-my\/my-prd\/wp-content\/uploads\/sites\/1327\/2014\/02\/bloggif_533bafe943bba.gif\" alt=\"\" width=\"250\" height=\"156\" \/><\/a><\/p>\n<p>While working at the Hungarian Academy of Sciences (MTA SZTAKI), I developed a grid-based smoke simulator that calculated the dynamics of the smoke based on the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Navier%E2%80%93Stokes_equations\">Navier-Stokes equations<\/a>. More information coming soon.<\/p>\n<h1>Resume<\/h1>\n<p>Here is my <a href=\"http:\/\/1drv.ms\/1fFzL6j\">resume<\/a>,\u00a0and my <a href=\"http:\/\/1drv.ms\/1j0d1pw\">LaTeX style file<\/a> used for producing it, based on\u00a0Rob J Hyndman&#8217;s cv.sty.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Gabor Simko Graduate Research Assistant Institute for Software Integrated Systems Vanderbilt University Research areas Formal specification of languages Formal verification Domain Specific Modeling Languages Embedded software, Cyber-Physical Systems, Hybrid Systems &nbsp; Formal semantic specifications of Cyber-Physical System modeling languages Cyber-Physical &hellip; <a href=\"https:\/\/my.vanderbilt.edu\/simko\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":2720,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"onecolumn-page.php","meta":{"footnotes":""},"class_list":["post-34","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/pages\/34","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/users\/2720"}],"replies":[{"embeddable":true,"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/comments?post=34"}],"version-history":[{"count":17,"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/pages\/34\/revisions"}],"predecessor-version":[{"id":130,"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/pages\/34\/revisions\/130"}],"wp:attachment":[{"href":"https:\/\/my.vanderbilt.edu\/simko\/wp-json\/wp\/v2\/media?parent=34"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}