@inproceedings{AAmanPohjola_RM_19, address = {Portland, Oregon}, author = {{\AA}man Pohjola, Johannes and Rostedt, Henrik and Myreen, Magnus}, booktitle = {Proceedings of the 10th International Conference on Interactive Theorem Proving}, date = {2019-9-5}, doi = {https://doi.org/10.4230/LIPIcs.ITP.2019.26}, isbn = {9783959771221}, keywords = {Program verification; non-termination; liveness; {Hoare} logic}, month = sep, pages = {32:1-19}, paperurl = {https://trustworthy.systems/publications/full_text/AAmanPohjola_RM_19.pdf}, publisher = {LIPIcs}, title = {Characteristic Formulae for Liveness Properties of Non-terminating {CakeML} Programs}, volume = {141}, year = {2019} }