[CAC13] Extended abstract: Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq

Conférence Internationale avec comité de lecture : High Integrity Language Technology - ACM SIGAdaâ€™s Annual International Conference, November 2013, pp.2, Series ACM Digital Library, US,

Auteurs: P. Courtieu , M. Aponte , T. Crolard , Z. Zhang , Robby , J. Belt , J. Hatcliff , J. Guitton , T. Jennings

motcle:

Résumé: We present our project, and a small early development, of formailzing the semantics of SPARC in Coq.

Equipe: sys

Collaboration: CIS@K-STATE , ADACORE , ALTRAN

BibTeX

@inproceedings {
	CAC13,
	title	=	"{Extended abstract: Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq}",
	author	=	" P. Courtieu and M. Aponte and T. Crolard and Z. Zhang and Robby and J. Belt and J. Hatcliff and J. Guitton and T. Jennings ",
	booktitle	=	"{High Integrity Language Technology - ACM SIGAdaâ€™s Annual International Conference}",
	year	=	2013,
	month	=	"November",
	series	=	"ACM Digital Library",
	pages	=	"2",
	address	=	" US",
}