University of Minnesota
Software Engineering Center
/

You are here

The Guardol Language and Verification System

Date of Publication: 
March 2012
Associated Research Groups: 
Publication Files: 
Abstract: 
Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.
Publisher: 
Springer-Verlag
Venue: 
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Tallinn, Estonia
bibtex: 
@inproceedings{Hardin12:guardol, Author = {David Hardin and Konrad Slind and Michael W. Whalen and Tuan-Hung Pham}, Title = {The Guardol Language and Verification System}, booktitle = {18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = {2012}, month = {April}, location = {Tallinn, Estonia} }