AbstractMotivationModel-based approaches to safety and efficacy assessment of pharmacological drugs, treatment strategies or medical devices (In Silico Clinical Trial, ISCT) aim to decrease time and cost for the needed experimentations, reduce animal and human testing, and enable precision medicine. Unfortunately, in presence of non-identifiable models (e.g. reaction networks), parameter estimation is not enough to generate complete populations of Virtual Patients (VPs), i.e. populations guaranteed to show the entire spectrum of model behaviours (phenotypes), thus ensuring representativeness of the trial.ResultsWe present methods and software based on global search driven by statistical model checking that, starting from a (non-identifiable) quantitative model of the human physiology (plus drugs PK/PD) and suitable biological and medical knowledge elicited from experts, compute a population of VPs whose behaviours are representative of the whole spectrum of phenotypes entailed by the model (completeness) and pairwise distinguishable according to user-provided criteria. This enables full granularity control on the size of the population to employ in an ISCT, guaranteeing representativeness while avoiding over-representation of behaviours. We proved the effectiveness of our algorithm on a non-identifiable ODE-based model of the female Hypothalamic-Pituitary-Gonadal axis, by generating a population of 4 830 264 VPs stratified into 7 levels (at different granularity of behaviours), and assessed its representativeness against 86 retrospective health records from Pfizer, Hannover Medical School and University Hospital of Lausanne. The datasets are respectively covered by our VPs within Average Normalized Mean Absolute Error of 15%, 20% and 35% (90% of the latter dataset is covered within 20% error).Availability and implementation. Our open-source software is available at https://bitbucket.org/mclab/vipgeneratorSupplementary informationSupplementary data are available at Bioinformatics online.