Certifying Safety and Termination Proofs for Integer Transition Systems
Marc Brockschmidt, Sebastiaan J.C. Joosten, René Thiemann, and Akihisa YamadaProceedings of the 15th International Workshop on Termination (WST 2016), pp. 4:1 – 4:5, 2016.
Abstract
We present a formalized certifier for safety proofs for integer transition
systems (ITSs), a formal language used to model C or Java programs. We also
report on our progress towards certifying termination proofs for ITSs.
BibTeX
@inproceedings{MBSJRTAY-WST16,
author = "Marc Brockschmidt and Sebastiaan J.C. Joosten and
Ren{\'e} Thiemann and Akihisa Yamada",
title = "Certifying Safety and Termination Proofs for Integer Transition
Systems",
booktitle = "Proceedings of the 15th International Workshop on Termination",
pages = "4:1-4:5",
year = 2016
}