Home

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

 

Formal semantic specifications of Cyber-Physical System modeling languages

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. You can find more information about this work here.

Sahvy

Sahvy is a tool for verifying sample and hold systems composed of a continuous-time physical plant and a periodic discrete-time software controller.
For more information about the tool and to download it, please follow this link.

Formalized proof of the L* algorithm

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:

Angluin, D. (1987). Learning regular sets from queries and counterexamples. Information and computation, 75(2), 87-106.

and our formalized proof is downloadable from here (to be published yet).

NetworGame


NetworGame 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 here.

Bone shadow elimination


The topic of my MSc thesis was collarbone detection and bone shadow elimination. Discussion of the topic is found in the following paper:

Simko G., 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–491.

Smoke simulation

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 Navier-Stokes equations. More information coming soon.

Resume

Here is my resume, and my LaTeX style file used for producing it, based on Rob J Hyndman’s cv.sty.