@article{Shankar, author = {Beyene, Tewodros and Herrera, Christian and Nigam, Vivek}, title = {Verification of Ada Programs with AdaHorn}, journal = {Ada User Journal}, volume = {40}, number = {2}, pages = {103-108}, year = {2019}, abstract = {We propose AdaHorn , a model checker for verification of Ada programs with respect to correctness properties given as assertions. AdaHorn translates an Ada program together with its assertion into a set of Constrained Horn Clauses, and feeds it to a Horn constraints solver. We evaluate the performance of AdaHorn on a set of Ada programs inspired by C programs from the software verification competition (SV-COMP). Our experimental results show that AdaHorn outputs correct results in more cases than GNATProve, which is a widely used Ada verification framework.}, }