Skip to main content
Conference ProceedingsOPEN ACCESS

The Guardol language and verification system

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2012) 7214 LNCS 18-32
DOI: 10.1007/978-3-642-28756-5_3
7Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

This article is free to access.

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. © 2012 Springer-Verlag Berlin Heidelberg.

Cite

CITATION STYLE

APA

Hardin, D., Slind, K., Whalen, M., & Pham, T. H. (2012). The Guardol language and verification system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7214 LNCS, pp. 18–32). https://doi.org/10.1007/978-3-642-28756-5_3

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free