Hardin, DavidSlind, KonradWhalen, MichaelPham, Hung T.2020-12-102020-12-102011The Fifth Annual Layered Assurance Workshop (LAW 2011)https://hdl.handle.net/11299/217401Associated research group: Critical Systems Research GroupGuardol 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.Report