Victor Khomenko

Formal Methods

Personal page

Research Interests

  • Formal Methods

  • Petri nets

Sample Projects:

  • Automatic Verification of Asynchronous Circuits: Asynchronous circuits (ACs) are circuits without clocks. ACs have been getting more and more attention in the last few years, as they often have lower power consumption and electro-magnetic emission, no problems with clock skew and related subtle issues, and are fundamentally more tolerant of voltage, temperature and manufacturing process variations. Though the listed advantages look rather attractive in the view of the current and anticipated microelectronics design challenges, correct and efficient ACs are notoriously difficult to design (there had been a few published asynchronous designs which subsequently turned out to be incorrect). You will be expected to write a tool for automatic verification of some standard correctness properties of asynchronous circuits, such as the absence of hazards and deadlocks. Good knowledge of mathematics and good programming skills are essential for this project.

  • Chess Endgame: The aim of this project is to develop software to play some chess endgames with few pieces remaining on the board. The project is available at several levels of difficulty. A detailed description is available at http://homepages.cs.ncl.ac.uk/victor.khomenko/teaching/projects/chess_endgame.rtf Good programming skills are essential for this project.

  • Computer Algebra System: The aim of this project is to develop software to perform symbolic transformations of algebraic expressions, such as simplification and differentiation. For example, the user should be able to give an expression to the system, e.g. sin(x^2+a), and ask it to differentiate it using x as the main variable. The system then should output, e.g. (2x+0)cos(x^2+a). Then the user can ask the system to simplify the expression, and get something like 2xcos(x^2+a). The project is available at several levels of difficulty; the level will be chosen depending on your degree program. Good mathematical background and programming skills are essential for this project.

  • Formal Verification of Petri Nets: For the research skills module: you should motivate the necessity of formal verification, describe the main challenges (in particular, the state space explosion), and give an overview of methods to cope with them, as well as an overview of the mainstream verification tools implementing each of these methods. For project modules: You will be expected to write a tool for EFFICIENT automatic verification of some standard correctness properties of Petri nets, such as the absence of deadlocks, reachability of a marking with specified properties, mutual exclusion, etc. Good knowledge of mathematics and good programming skills are essential for this project.

  • Minesweeper Assistant: The aim of this project is to develop software helping people (like me) who hate losing in Minesweeper (this game comes with Windows). The project is available at several levels of difficulty. A detailed description is available at http://homepages.cs.ncl.ac.uk/victor.khomenko/teaching/projects/Minesweeper%20Assistant.doc

  • System Area Planning: The aim of this project is to develop a system for area planning to be used by architects. It will allow the user to specify an area using measurements or selection from a map, via a GUI. Users can drag-and-drop items with predefined sizes into the area, such as housing units and roads. A more advanced version of the system will perform the layout optimization, trying, for example, to maximize the number of housing units on the site, or minimize the length of roads. This optimisation is subject to some constraints, including that each house must be adjacent to a road and the roads must be of a certain shape. The system will output a graphic representation of the solution to this optimization problem. Good mathematical background and programming skills are essential for this project.

Technologies & Programming Languages

I am comfortable supervising projects that make use of the following technologies and programming languages.

  • C++

Contact

TODO: Use this site to find project supervisors for your masters projects.