Paper Info
Title
Formalization of the DE2 language
Abstract
We formalized the DE2 hierarchical, occurrence-oriented finite state machine (FSM) language, and have developed a proof theory allowing the mechanical verification of FSM descriptions. Using the ACL2 functional logic, we have defined a predicate for detecting the well-formedness of DE2 expressions. Furthermore, we have defined a symbolic simulator for DE2 expressions which also serves as a formal cycle-based semantics for the DE2 language. DE2 is deeply embedded within ACL2, and the DE2 language includes an annotation facility that can be used by programs that manipulate DE2 descriptions. The DE2 user may also specify and prove the correctness of programs that generate DE2 descriptions. We have used DE2 to mechanically verify components of the TRIPS microprocessor implementation.
Year
DOI
Venue
2005
10.1007/11560548_5
CHARME
Keywords
Field
DocType
finite state machine,proof theory
Programming language,Expression (mathematics),Computer science,Correctness,Proof theory,Finite-state machine,Theoretical computer science,Predicate (grammar),ACL2,Semantics,Hardware description language
Conference
Volume
ISSN
ISBN
3725
0302-9743
3-540-29105-9
Citations 
PageRank 
References 
11
0.80
9
Authors
2
Name
Order
Citations
PageRank
Warren A. Hunt123013.86
Erik Reeber2865.58