Title
The guardol language and verification system
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, then 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.
Year
DOI
Venue
2012
10.1007/978-3-642-28756-5_3
TACAS
Keywords
Field
DocType
automated verification support,correct network guard,verification system,tree-shaped data,guardol program,guardol language,difficult property,tree-structured data,domain-specific language,guardol system,smt-style decision procedure,ada code
Programming language,Computer science,Theoretical computer science,Guard (information security),Recursive functions,Higher-order logic,Verification system
Conference
Volume
ISSN
Citations 
7214
0302-9743
6
PageRank 
References 
Authors
0.53
13
4
Name
Order
Citations
PageRank
David Hardin1344.52
Konrad Slind257755.90
Michael W. Whalen3109670.54
Tuan Pham450373.75