TY - GEN
T1 - The Guardol language and verification system
AU - Hardin, David
AU - Slind, Konrad
AU - Whalen, Michael
AU - Pham, Tuan Hung
PY - 2012/4/9
Y1 - 2012/4/9
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84859325635&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84859325635&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-28756-5_3
DO - 10.1007/978-3-642-28756-5_3
M3 - Conference contribution
AN - SCOPUS:84859325635
SN - 9783642287558
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 18
EP - 32
BT - Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings
T2 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Y2 - 24 March 2012 through 1 April 2012
ER -