University of Minnesota
Software Engineering Center

You are here

Introduction to the Guardol Language and Verification System

Date of Publication: 
December 2011
Associated Research Groups: 
Publication Files: 
Guardol is a high-level programming language intended to facilitate the construction of correct network guards. The Guardol system generates Ada code from Guardol programs. It also provides specification and automated verification support: guard specifications are formally translated to SMT format and passed to a new decision procedure dealing with functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.
The Fifth Annual Layered Assurance Workshop (LAW 2011)