cl-banner

Certifying Safety and Termination Proofs for Integer Transition Systems

Marc Brockschmidt, Sebastiaan J.C. Joosten, René Thiemann, and Akihisa Yamada

Proceedings 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. 

 

  PDF

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
}
Nach oben scrollen