Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

A Semantic Embedding of the Ag Dynamic Logic in PVS


Carlos López Pombo, Sam Owre, and Natarajan Shankar


Ag is a specification language presented as a syntactic sugaring of the First-Order Dynamic Logic of Fork Algebras. This language is particularly attractive due to its expressive power, easy-to-understand semantics, and the existence of a complete deductive system. We will briefly present the language together with a complete deductive calculus and some theoretical results about its expressive power. We then show how the higher-order logic theorem prover PVS can be used to build a semantic framework for reasoning about specifications written in Ag by encoding the semantics within this powerful general-purpose tool. We then illustrate how this semantic embedding can be used by means of a case study of a cache system specification.


BibTeX Entry

	AUTHOR = {Carlos L\'{o}pez Pombo and Sam Owre and Natarajan Shankar},
	TITLE = {A Semantic Embedding of the {Ag} Dynamic Logic in {PVS}},
	MONTH = oct,
	YEAR = 2004,
	NUMBER = {SRI-CSL-02-04},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available at
Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Wed 24 Nov 2010 14:07 PST
Maintainer: Sam Owre