Relating the Genetic Code, Nature’s amazing invention, with the Gray Code, a pure human artifact, yet again proves Galileo right: The Grand Book is written in the language of mathematics.
Dragan Bosnacki is an assistant professor at the TU/e department of Biomedical Engineering. His current main research interests are in (Big) Data and Health, and modelling of High Intensity Focused Ultrasound (HIFU) for cancer therapies. His previous work includes algorithms for reconstruction of biological networks and various applications of formal verification techniques in biology and medicine.
Dr. Bosnacki has an extensive track record in formal verification of hardware and software, in particular in model checking. He has developed several improvements of state space reduction techniques, like partial-order reduction and symmetry reduction, and contributed several improvements of the probably most prominent model checking tool SPIN. Currently he serves as a steering committee chair of the SPIN symposiums. He has also co-pioneered the areas of multi-core and GPU model checking, which cover parallel model checking techniques on shared memory systems. Recently he has worked in separation logic and its applications in the tool VeriFast.
Dragan Bosnacki obtained both his BSc in Electrical Engineering and his MSc in Computer Science from Sts. Cyril and Methodius University in Skopje (Macedonia). From 1990 to 1997 he was a Teaching and Research Assistant at the Institute of Informatics at the same university. He then moved to Eindhoven University of Technology (TU/e, The Netherlands) for his PhD studies. In 2001 he obtained his PhD at the Department of Mathematics and Computer Science under supervision of Jos Baeten and Dennis Dams. Since 2000 he has been an Assistant Professor at the TU/e departments of Biomedical Engineering and Mathematics and Computer Science.
Modeling the interference between shear and longitudinal waves under high intensity focused ultrasound propagation in bonePhysics in Medicine and Biology (2018)
Model checkingInternational Journal on Software Tools for Technology Transfer (2018)
Modular termination verification of single-threaded and multithreaded programsACM Transactions on Programming Languages and Systems (2018)
Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy (2017)
HIFUtk: Visual Analytics for High Intensity Focused Ultrasound SimulationEurographics Workshop on Visual Computing for Biology and Medicine (2017)
- Radiation physics
- Bachelor final project Computational Biology
- DBL Computational biology
No ancillary activities