[CAC15] Formal Methods for Critical Systems: A verified implementation of nested procedures

Conférences invitées : International Conference on Applied Research in Computer Science and Engineering (ICAR'15), October 2015, pp.1, Lebanon, (DOI: 10.1109/ARCSE.2015.7338125)

Auteurs: T. Crolard , M. Aponte , P. Courtieu , J. Lawall

motcle:

Résumé: This project is part of a broad effort to develop a formal representation of SPARK Ada programs suitable for supporting machine-verified static analyses and translations. In collaboration with SAnToS Labs (Kansas State University) and AdaCore (the GNAT Pro Company), we have previously formalised the dynamic semantics for small subset of the SPARK Ada language, including the encoding of some run-time checks. In this talk, we'll focus on Ada procedures and, to be more specific, on the semantics of nested and mutually recursive procedures. In particular, we'll present a proof-of-concept formalisation of an abstract P-machine and we'll describe some of the meta-theory we have checked with the Coq proof assistant.

BibTeX

@inproceedings {
	CAC15,
	title	=	"{Formal Methods for Critical Systems: A verified implementation of nested procedures}",
	author	=	" T. Crolard and M. Aponte and P. Courtieu and J. Lawall ",
	booktitle	=	"{International Conference on Applied Research in Computer Science and Engineering (ICAR'15)}",
	year	=	2015,
	month	=	"October",
	pages	=	"1",
	address	=	" Lebanon",
	doi	=	"10.1109/ARCSE.2015.7338125",
}