SHF: SMALL: Collaborative Research: Modular ACL2

University Of Oklahoma Norman Campus, Norman OK

Investigators

Abstract

Reliability is extremely important for some software and hardware applications. One approach is to use a programming language with a mechanized logic---a so-called theorem-prover---to prove theorems that establish some critical behavioral characteristics. Among theorem-provers, ACL2 has found use with several industrial suppliers of high assurance software and hardware. ACL2 does not support component-oriented software development, however, making it difficult to use with large and complex projects. This research project has three goals: to add a pragmatic module system to ACL2; to equip it with a hygienic macro system; and to investigate a type system that accommodates ACL2's programming idioms. The project team employs a cyclic, three-step exploration method. The first step is to adapt constructs from existing, similar languages to ACL2, especially a logical meaning consistent with the theorem prover of ACL2. The second step is to explore the pragmatics of the design with a wide range of examples. The third step is to add implementations to a pedagogic, interactive development environment for ACL2 and to evaluate their usefulness in software engineering courses. The results of this last step are used to re-start the cycle. The work will contribute to the dissemination of theorem provers in classrooms and industry. The research team expects to expose college students to the use of theorem proving in the design and development of complex systems with dozens, and possibly hundreds, of reliable components. The team also hopes to improve the ability of industrial ACL2 programmers to tackle complex component-oriented systems.