Newcastle University

Introduction

Victor obtained MSc with distinction in Computer Science, Applied Mathematics and Teaching of Mathematics and Computer Science in 1998 from Kiev Taras Shevchenko University, and PhD in Computing Science in 2003 from Newcastle University.

In January 2005 Victor became a Lecturer in this School, and then in September 2005 he obtained a Royal Academy of Engineering / EPSRC Post-doctoral Research Fellowship and worked on the DAVAC project. After the end of this award, in September 2010, he switched back to Lectureship.

Research Interests

My research is concentrated on the theory of distributed and concurrent systems, in particular on application of formal techniques to verification and synthesis of such systems. From September, 1999, I have been working on model checking of Petri nets and synthesis of asynchronous (self-timed) circuits using Petri net unfoldings.

Current Work

Currently I work on the Verification-Driven Asynchronous Design (VERDAD) project.

Esteem Indicators

5-years research fellowship from Royal Academy of Engineering and EPSRC.

Best paper award at ACSD'04 conference, and best paper selection at DATE'03, ACSD'03, ACSD'04, ACSD'06, ACSD'07, Petri Nets'08 and ACSD'09 conferences.

Invited speaker at UK Asynchronous Forum'06 and International Workshop on Petri nets and Software Engineering (PNSE'11).

Funding

I am the PI on the EPSRC-funded Verification-Driven Asynchronous Design (VERDAD) project.

• Mokhov A, Khomenko V, Alekseyev A, Yakovlev A. Algebra of Parametrised Graphs. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2011. School of Computing Science Technical Report Series 1307.
• Khomenko V, Mokhov A. An Algorithm for Direct Construction of Complete Merged Processes. In: Applications and Theory of Petri Nets: 32nd International Conference (PETRI NETS). 2011, Newcastle upon Tyne, UK: Springer Verlag.
• Mokhov A, Khomenko V, Yakovlev A. Flat Arbiters. Fundamenta Informaticae 2011, 108(1-2), 63-90.
• Alekseyev A, Khomenko V, Mokhov A, Wist D, Yakovlev A. Improved parallel composition of labelled Petri nets. In: 11th International Conference on Application of Concurrency to System Design (ACSD). 2011, Kanazawa, Japan: IEEE.
• Khomenko V. Logic Decomposition of Asynchronous Circuits Using STG Unfoldings. In: 17th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC). 2011, Cornell University, Ithaca, New York, USA: IEEE.
• Madalinski A, Khomenko V. Predictability Verification with Parallel LTL-X Model Checking Based on Petri Net Unfoldings. School of Computing Science, Newcastle University, 2011. CS-TR-1276. Submitted.
• Madalinski A, Khomenko V. Predictability Verification with Parallel LTL-X Model Checking Based on Petri Net Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2011. School of Computing Science Technical Report Series 1276.
• Khomenko V. A New Type of Behaviour-Preserving Transition Insertions in Unfolding Prefixes. In: 5th International Conference on Graph Transformation (ICGT). 2010, Twente, The Netherlands: Springer Verlag.
• Khomenko V. A New Type of Behaviour-Preserving Transition Insertions in Unfolding Prefixes. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2010. School of Computing Science Technical Report Series 1189.
• Madalinski A, Khomenko V. Diagnosability Verification with Parallel LTL-X Model Checking Based on Petri Net Unfoldings. In: Conference on Control and Fault-Tolerant Systems (SysTol). 2010, Nice, France: IEEE Computing Society Press.
• Khomenko V. Logic Decomposition of Asynchronous Circuits Using STG Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2010. School of Computing Science Technical Report Series 1215.
• Banks R, Khomenko V, Steggles LJ. Modelling Genetic Regulatory Networks. In:Koch, I., Reisig, W., Schreiber, R., ed. Modelling in Systems Biology: the Petri Net Approach.London:Springer-Verlag,2010, pp. 73-100.
• Mokhov A, Khomenko V, Sokolov D, Yakovlev A. On Dual-Rail Control Logic for Enhanced Circuit Robustness. Newcastle upon Tyne: School of Electrical, Electronic & Computer Engineering, Newcastle University, 2010. School of Electrical, Electronic & Computer Engineering Technical Report Series NCL-EECE-MSD-TR-2010-162.
• Banks R, Khomenko V, Steggles LJ. A Case for Using Signal Transition Graphs for Analysing and Refining Genetic Networks. In: Electronic Notes in Theoretical Computer Science: Second International Meeting on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC).2009,Iasi, Romania:Elsevier B.V.
• Meyer R, Khomenko V, Strazny T. A Practical Approach to Verification of Mobile Systems Using Net Unfoldings. Fundamenta Informaticae 2009, 94(3-4), 439-471.
• Khomenko V. A Usable Reachability Analyser. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2009. School of Computing Science Technical Report Series 1140.
• Khomenko V. A Usable Reachability Analyser. In: 21st UK Asynchronous Forum. 2009, Bristol, UK: Computer Science Department, University of Bristol.
• Khomenko V, Meyer R. Checking pi-Calculus Structural Congruence is Graph Isomorphism Complete. In: 9th International Conference on Application of Concurrency to System Design (ACSD). 2009, Augsburg, Germany: IEEE Computer Society.
• Khomenko V. Efficient Automatic Resolution of Encoding Conflicts Using STG Unfoldings. IEEE Transactions on Very Large Scale Integration (VLSI) Systems 2009, 17(7), 855-868.
• Mokhov A, Khomenko V, Yakovlev A. Flat Arbiters. In: 9th International Conference on Application of Concurrency to System Design (ACSD).2009,Augsburg, Germany:IEEE Computer Society
• Alekseyev A, Poliakov I, Khomenko V, Yakovlev A. Optimisation of Balsa control path using STG resynthesis. In: 21st UK Asynchronous Forum. 2009, Bristol, UK: Computer Science Department, University of Bristol.
• Khomenko V, Schaefer M, Vogler W, Wollowski R. STG Decomposition Strategies in Combination with Unfolding. Acta Informatica 2009, 46(6), 433-474.
• Poliakov I, Khomenko V, Yakovlev A. WORKCRAFT - A Framework for Interpreted Graph Models. In: 30th International Conference on Applications and Theory of Petri Nets.2009,Paris, France:Springer-Verlag
• Banks R, Khomenko V, Steggles J. A Case for Using Signal Transition Graphs for Analysing and Refining Genetic Networks. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2008. School of Computing Science Technical Report Series 1086.
• Meyer R, Khomenko V, Strazny T. A Practical Approach to Verification of Mobile Systems Using Net Unfoldings. In: Applications and Theory of Petri Nets: 29th International Conference.2008,Xi'an, China:Springer-Verlag
• Meyer R, Khomenko V, Strazny T. A Practical Approach to Verification of Mobile Systems Using Net Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2008. School of Computing Science Technical Report Series 1064.
• Khomenko V, Meyer R. Checking pi-Calculus Structural Congruence is Graph Isomorphism Complete. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2008. School of Computing Science Technical Report Series 1100.
• Khomenko V. Derivation of Monotonic Covers for standard-C implementation using STG unfoldings. In: 14th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC).2008,Newcastle upon Tyne, UK:IEEE
• Khomenko V, Schaefer M, Vogler W. Output-Determinacy and Asynchronous Circuit Synthesis. Fundamenta Informaticae 2008,88 4 541-579.
• Khomenko V, Madalinski A, Yakovlev A. Resolution of Encoding Conflicts by Signal Insertion and Concurrency Reduction Based on STG Unfoldings. Fundamenta Informaticae 2008,86 3 299-323.
• Chatain T, Khomenko V. A Note on the Well-Foundedness of Adequate Orders Used for Truncating Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2007. School of Computing Science Technical Report Series 998.
• Khomenko V. Behaviour-Preserving Transition Insertions in Unfolding Prefixes. In: 28th International Conference on Petri Nets and Other Models of Concurrency (ICATPN).2007,Siedlce, Poland:Springer
• Khomenko V, Schaefer M. Combining Decomposition and Unfolding for STG Synthesis. In: 28th International Conference on Petri Nets and Other Models of Concurrency (ICATPN).2007,Siedlce, Poland:Springer
• Khomenko V, Schaefer M. Combining Decomposition and Unfolding for STG Synthesis. Augsburg, Germany: Institute of Computer Science, University of Augsburg, 2007. 2007-01.
• Khomenko V. Efficient Automatic Resolution of Encoding Conflicts Using STG Unfoldings. In: 7th International Conference on Application of Concurrency to System Design (ACSD 2007). 2007, Bratislava, Slovak Republic: IEEE Computer Society.
• Khomenko V. Efficient Automatic Resolution of Encoding Conflicts Using STG Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2007. School of Computing Science Technical Report Series 995.
• Chatain T, Khomenko V. On the well-foundedness of adequate orders used for construction of complete unfolding prefixes. Information Processing Letters 2007, 104(4), 129-136.
• Khomenko V, Schaefer M, Vogler W. Output-Determinacy and Asynchronous Circuit Synthesis. In: 7th International Conference on Application of Concurrency to System Design (ACSD 2007). 2007, Bratislava, Slovak Republic: IEEE Computer Society.
• Khomenko V, Schaefer M, Vogler W. Output-Determinacy and Asynchronous Circuit Synthesis. Augsburg, Germany: Institute of Computer Science, University of Augsburg, 2007. 2007-02.
• Khomenko V, Koutny M. Verification of bounded Petri nets using integer programming. Formal Methods in System Design 2007, 30(2), 143-176.
• Khomenko V, Koutny M, Niaouris A. Applying Petri Net Unfoldings for Verification of Mobile Systems. In: Fourth International Workshop on Modelling of Objects, Components and Agents (MOCA'06). 2006, Turku, Finland: Universität Hamburg, Department Informatik.
• Khomenko V, Koutny M, Niaouris A. Applying Petri Net Unfoldings for Verification of Mobile Systems. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2006. School of Computing Science Technical Report Series 953.
• Madalinski A, Khomenko V, Yakovlev A. Interactive Resolution of Encoding Conflicts in Asynchronous Circuits Based on STG Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2006. School of Computing Science Technical Report Series 944.
• Khomenko V, Koutny M, Yakovlev A. Logic Synthesis for Asynchronous Circuits Based on STG Unfoldings and Incremental SAT. Fundamenta Informaticae 2006, 70(1-2), 49-73.
• Khomenko V, Kondratyev A, Koutny M, Vogler W. Merged processes: A new condensed representation of Petri net behaviour. Acta Informatica 2006, 43(5), 307-330.
• Khomenko V, Madalinski A, Yakovlev A. Resolution of encoding conflicts by signal insertion and concurrency reduction based on STG unfoldings. In: 6th International Conference on Application of Concurrency to System Design (ACSD 2006). 2006, Turku, Finland: IEEE.
• Schaefer M, Vogler W, Wollowski R, Khomenko V. Strategies for Optimised STG Decomposition. In: 6th International Conference on Application of Concurrency to System Design (ACSD 2006). 2006, Turku, Finland: IEEE Computer Society.
• Khomenko V. Derivation of Set and Reset Covers for gC Elements and Standard C Implementation Using STG Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2005. School of Computing Science Technical Report Series 930.
• Khomenko V, Kondratyev A, Koutny M, Vogler W. Merged processes - A new condensed representation of Petri net behaviour. In: Concurrency Theory: 16th International Conference (CONCUR). 2005, San Francisco, CA, USA: Springer.
• Khomenko V, Kondratyev A, Koutny M, Vogler W. Merged Processes - a New Condensed Representation of Petri Net Behaviour. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2005. School of Computing Science Technical Report Series 884.
• Iliasov A, Khomenko V, Koutny M, Romanovsky A. On specification and verification of location-based fault tolerant mobile systems. In: Rigorous Engineering of Fault Tolerant Systems (REFT). 2005, Newcastle upon Tyne: Springer Berlin / Heidelberg.
• Khomenko V. Shortest Violation Traces in Model Checking Based on Petri Net Unfoldings and SAT. In: Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT). 2005, Newcastle upon Tyne, UK: School of Computing Science, Newcastle University.
• Khomenko V. Computing Shortest Violation Traces in Model Checking Based on Petri Net Unfoldings and SAT. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2004. School of Computing Science Technical Report Series 841.
• Khomenko V, Koutny M, Yakovlev A. Detecting State Encoding Conflicts in STG Unfoldings Using SAT. Fundamenta Informaticae 2004, 62(2), 221-241.
• Khomenko V, Koutny M, Yakovlev A. Logic synthesis for asynchronous circuits based on petri net unfoldings and incremental SAT. In: 4th International Conference on Application of Concurrency to System Design (ACSD 2004). 2004, Hamilton, Ontario, Canada: IEEE.
• Khomenko V, Koutny M, Yakovlev A. Logic synthesis for asynchronous circuits based on STG unfoldings and incremental SAT. In: 4th International Conference on Application of Concurrency to System Design (ACSD 2004). 2004, Hamilton, Canada: Fundamenta Informaticae: IOS Press.
• Schröter C, Khomenko V. Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. In: Computer Aided Verification: 16th International Conference (CAV 2004). 2004, Boston, MA: Springer Verlag.
• Khomenko V, Madalinski A, Yakovlev A. Resolution of Encoding Conflicts by Signal Insertion and Concurrency Reduction Based on STG Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2004. School of Computing Science Technical Report Series 858.
• Carmona J, Cortadella J, Khomenko V, Yakovlev A. Synthesis of asynchronous hardware from Petri nets. In: Desel, J., Reisig, W., Rozenberg, G., ed. Lectures on Concurrency and Petri Nets: Advances in Petri Nets. Berlin: Springer, 2004, pp. 183-205.
• Khomenko V. Weasel Words, Genetic Algorithms and Coarse Acknowledgements. Technical Journal 2004, 18(1), 78-85.
• Khomenko V, Koutny M. Branching processes of high-level Petri nets. In: Tools and Algorithms for the Construction and Analysis of Systems: 9th International Conference (TACAS). 2003, Warsaw, Poland: Springer.
• Khomenko V, Koutny M. Branching Processes of High-Level Petri Nets. In: 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS). 2003, Warsaw, Poland: Springer-Verlag.
• Khomenko V, Koutny M, Vogler W. Canonical prefixes of Petri net unfoldings. Acta Informatica 2003, 40(2), 95-118.
• Khomenko V, Koutny M, Yakovlev A. Detecting State Coding Conflicts in STG Unfoldings Using SAT. In: 3rd International Conference on Application of Concurrency to System Design (ACSD 2003). 2003, Guimaraes, Portugal: IEEE Computer Society.
• Khomenko V, Koutny M, Yakovlev A. Logic Synthesis Avoiding State Space Explosion. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2003. School of Computing Science Technical Report Series 813.
• Madalinski A, Bystrov A, Khomenko V, Yakovlev A. Visualisation and resolution of encoding conflicts in asynchronous circuit design. In: 6th Conference on Design and Test in Europe (DATE03). 2003, Munich, Germany: IEE Proceedings: Computers and Digital Techniques.
• Madalinski A, Bystrov A, Khomenko V, Yakovlev A. Visualization and Resolution of Coding Conflicts in Asynchronous Circuit Design. IET Computers & Digital Techniques 2003, 150(5), 285-293.
• Khomenko V. [PhD Thesis] Model Checking Based on Prefixes of Petri Net Unfoldings. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2003.
• Letichevskii A, Khomenko V. A Rewriting Machine and Optimization of Strategies of Term Rewriting. Cybernetics and Systems Analysis 2002, 38(5), 637-649.
• Khomenko V, Koutny M. Branching Processes of High-Level Petri Nets. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2002. Department of Computing Science Technical Report Series 763.
• Khomenko VV, Koutny MS, Vogler W. Canonical Prefixes of Petri Net Unfoldings. In: 14th International Conference on Computer Aided Verification (CAV 2002). 2002, Copenhagen, Denmark: Springer-Verlag.
• Khomenko V, Koutny M, Yakovlev A. Detecting State Coding Conflicts in STG Unfoldings Using SAT. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2002. Department of Computing Science Technical Report Series 778.
• Khomenko V, Koutny M, Yakovlev A. Detecting State Coding Conflicts in STGs Using Integer Programming. In: Design, Automation and Test in Europe Conference and Exposition (DATE). 2002, Paris, France: IEEE Computer Society Press.
• Heljanko K, Khomenko V, Koutny M. Parallelisation of the Petri net unfolding algorithm. In: Tools and Algorithms for the Construction and Analysis of Systems: 8th International Conference (TACAS). 2002, Grenoble, France: Springer.
• Koutny M, Khomenko V. An Efficient Algorithm for Unfolding Petri Nets. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2001. Department of Computing Science Technical Report Series 726.
• Khomenko V, Koutny M, Vogler W. Canonical Prefixes of Petri-Net Unfoldings. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2001. Department of Computing Science Technical Report Series 741.
• Heljanko K, Khomenko V, Koutny M. Parallelisation of the Petri Net Unfolding Algorithm. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2001. Department of Computing Science Technical Report Series 733.
• Khomenko V, Koutny M. Towards an Efficient Algorithm for Unfolding Petri Nets. In: 12th International Conference on Concurrency Theory (CONCUR). 2001, Aalborg, Denmark: Springer-Verlag.
• Koutny M, Khomenko V. Linear Programming Deadlock Checking Using Partial Order Dependencies. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2000. Department of Computing Science Technical Report Series 695.
• Khomenko V, Koutny M. LP Deadlock Checking Using Partial Order Dependencies. In: 11th International Conference on Concurrency Theory (CONCUR). 2000, University Park, Pennsylvania, USA: Springer-Verlag.
• Khomenko V, Koutny M. Verification of Bounded Petri Nets Using Integer Programming. Newcastle upon Tyne: Department of Computing Science, University of Newcastle upon Tyne, 2000. Department of Computing Science Technical Report Series 711.