Access Restriction

Author Slind, Konrad L. ♦ Whalen, Michael W. ♦ Hardin, David S. ♦ Pham, Tuang-Hung
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword Domain specific language ♦ Cross-domain systems ♦ Formal verification
Abstract Guardol is a domain-specific language focused on the creation of high-assurance network guards and the specification of guard properties. 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.
Description Affiliation: Rockwell Collins, Cedar Rapids, IA, USA (Hardin, David S.) || Rockwell Collins, Bloomington, MN, USA (Slind, Konrad L.) || University of Minnesota, Minneapolis, MN, USA (Whalen, Michael W.; Pham, Tuang-Hung)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1989-04-01
Publisher Place New York
Journal ACM SIGAda Ada Letters (ALET)
Volume Number 32
Issue Number 3
Page Count 10
Starting Page 53
Ending Page 62

Open content in new tab

   Open content in new tab
Source: ACM Digital Library