Dragan Bosnacki


  • 530 Citations
If you made any changes in Pure these will be visible here soon.

Personal profile


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.

Research profile

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. 

Academic background

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.

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Research Output 1998 2018

From concurrent state machines to reliable multi-threaded Java code

Zhang, D., 12 Apr 2018, Eindhoven: Technische Universiteit Eindhoven. 160 p.

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)Academic

Open Access

Model checking: recent improvements and applications

Bošnački, D. & Wijs, A., 1 Oct 2018, In : International Journal on Software Tools for Technology Transfer. 20, 5, p. 493–497

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
Model checking
1 Citation (Scopus)

Modeling the interference between shear and longitudinal waves under high intensity focused ultrasound propagation in bone

Modena, D., Baragona, M., Bošnački, D., Breuer, B. J. T., Elevelt, A., Maessen, R. T. H., Hilbers, P. A. J. & ten Eikelder, H. M. M., 4 Dec 2018, In : Physics in Medicine and Biology. 63, 23, 12 p., 235024

Research output: Contribution to journalArticleAcademicpeer-review

Bone and Bones
Hot Temperature
Magnetic Resonance Spectroscopy
1 Citation (Scopus)

Modular termination verification of single-threaded and multithreaded programs

Jacobs, B., Bosnacki, D. & Kuiper, R., 1 Aug 2018, In : ACM Transactions on Programming Languages and Systems. 40, 3, A12

Research output: Contribution to journalArticleAcademicpeer-review


HIFUtk: visual analytics for high intensity focused ultrasound simulation

Modena, D., van Dijk, E. V. M., Bosnacki, D., ten Eikelder, H. M. M. & Westenberg, M. A., 2017, Eurographics Workshop on Visual Computing for Biology and Medicine. Bruckner, S., Hennemuth, A., Kainz, B., Hotz, I., Merhof, D. & Rieder, C. (eds.). Geneve: The Eurographics Association, p. 73-82 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

human body

Activities 1999 1999

  • 1 Workshop, seminar, course or exhibition

11th Nordic Workshop on Programming Theory (NWPT'99), October 6-8, 1999, Uppsala, Sweden

Dragan Bosnacki (Organiser)
6 Oct 1999

Activity: Participating in or organising an event typesWorkshop, seminar, course or exhibitionScientific

Student theses

A computational biology framework: a data analysis tool to support biomedical engineers in their research

Author: Beishuizen, T., 29 Nov 2018

Supervisor: Bosnacki, D. (Supervisor 1), Cheplygina, V. (Supervisor 2), Hilbers, P. (Supervisor 2), Fletcher, G. (Supervisor 2) & Vanschoren, J. (Supervisor 2)

Student thesis: Master

Algorithms for gene regulatory networks reconstruction

Author: Maksimov, N., 31 Aug 2015

Supervisor: Bosnacki, D. (Supervisor 1)

Student thesis: Master


A parallel algorithm for comparing metabolic pathways

Author: Datema, R., 31 Aug 2006

Supervisor: Hilbers, P. (Supervisor 1), Bosnacki, D. (Supervisor 2), Zwaan, G. (Supervisor 2) & Mak, R. (Supervisor 2)

Student thesis: Master


Causal candidate genes identification for familial hypercholesterolemia family based on whole-genome sequencing

Author: Wang, Q., 31 Aug 2017

Supervisor: Hilbers, P. (Supervisor 1), van Riel, N. (Supervisor 2), Hovingh, K. (External person) (External coach), Bosnacki, D. (Supervisor 2) & Veta, M. (Supervisor 2)

Student thesis: Master

Finding maximal frequent subgraphs

Author: Wagemans, J., 30 Jun 2008

Supervisor: Zantema, H. (Supervisor 1) & Bosnacki, D. (Supervisor 2)

Student thesis: Master