University of Minnesota
Software Engineering Center
/

You are here

David Hardin

Recent Publications

The Guardol Language and Verification System

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.

Introduction to the Guardol Language and Verification System

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.

Pages