Viliam Holub

I am a researcher and a teacher at the University College Dublin in the School of Computer Science and Informatics, formerly from Distributed Systems Research Group, Charles University. My research interests cover formal verification and parallel and distributed model checking, however I am interest in many other fields of software engineering and computer science.

I studied Electronic Computer Systems within 1994-1998 where I got an electrotechnical background. Then I graduated in Software Engineering from Faculty of Mathematics and Physics, Charles University and finished my postgraduate study in the Department of Software Engineering.

I like programming and I programmed a lot so far. I'm fluent in C, C++, Perl, PHP, Java, and x86, I'm perfectly familiar (although haven't written so much code yet) with Python, Ruby, and ECMAScript, and I'm able to read a lot of others. I don't feel stuck in one programming language.

Currently I'm involved in a big-data start up Logentries.

viliam.holubREMOVE@ucd.ie - I read emails regularly. If you want to talk to me in person, please send me an email first.

• Run-Time Correlation Engine for System Monitoring and Testing,
  with T. Parsons, P. O'Sullivan, and J. Murphy;
  presents a monitoring and analysing engine for distributed component systems. RTCE aggregates, adapts, correlates, and stores events in real-time. Symptom matching is implemented as well.; Jan 2009
• Streaming State Space: A Method of Distributed Model Verification,
  with P. Tuma;
  discuss a new approach to distributed model verification. In contrast to common partitioning of the state space across nodes, we hand over the whole state space. While keeping the network load acceptable, the method scales well even in performance non-uniform clusters and allows to effectively store the state space on external storage devices; Jun 2007 [pdf | ps]
• Reducing Component Systems' Behavior Specification,
  with F. Plasil;
  presents a method of dealing with the state space explosion problem based on automatic modification of the specification. Symbolic manipulations with the specification are processed prior to the verification process and - while preserving errors of the model - significantly reduce the final state space which has to be traversed. Our experimental results show, that the method is vital a often produces better results than partial-order-reduction; Nov 2007 [pdf | ps]
• Identifying Representatives for Interfering Automata
  shows how to reduce the state space by identifying specific states of the model. The work is focused on Interfering Automata, a light-weight language for simulation of several popular formalisms; Mar 2007
• Implementation of a Linux Log-Structured File System with a Garbage Collector
  with M. Jambor, T. Hruby, J. Taus, and K. Krchak;
  presents details about the work of graduate students in the course Software project - a Linux implementation of log-structured filesystem; Jan 2007 [pdf | ps]
• On Distributed Verification of Generalized Interaction Models of Software Components;
  presented on doctoral symposium of 20th European Conference on Object-Oriented Programming (ECOOP 2006), it is a brief explanation of the initial ideas of distributed model verification based on streaming approach; Jul 2006 [pdf | ps]
• Exceptions in Component Interaction Protocols - Necessity,
  with F. Plasil;
  discuss how are exceptions interesting in interaction protocols and proposes an syntax enhancement of behavior protocols with respect to exceptions; Dec 2004 [pdf | ps]

• Lesser known C features contains a description of several C features

• Shash
  implementation of the Charikar's hash function for the detection of near-duplicate documents.
• Imagescure
  obfuscates images to aggravate automated recognition. This is useful for web maintainers to protect their services against automated scripts.
• MSIM
  is a "MIPS simulator" - a simulator of a complete computer used as a reference machine for the operating system course. It aims at a straightforward component model, which removes some obscuredness of real-life hardware, but still keeps its principles.
• LK
  aka "light kermit" is a terminal for an easy communication over the serial line. Quite useful to manage another computer in a case of network failure.
• CSSC
  lossy compresses style sheets by skipping comments, shrinking whitespaces, and similar allowed modifications. A one-day project; but works fine and may be useful for sites with huge commented css files.
• Atraktor
  creates random curly images as the one you can see on the top right corner of this page (in an unlikely case you have a graphics terminal and a css-capable browser, though).
• Removing accents in PHP
  small and useful function for removing accents from characters in UTF-8 strings.
• Murmur hash in Java
  implementation of the 32bit and 64bit Murmur hash 2.0 in Java, including jUnit tests.

• Promela highlighting for vim may be useful for all the vim-spin fans.
• Pictures a tiny collection of pictures
• Tech bugs, errors, worth reading, etc.
• LCD synchronization page