Symbolic Simulation: An ACL2 Approach

Executable formal speci cation can allow engineers to test (or simulate) the speci ed system on concrete data before the system is implemented. This is beginning to gain acceptance and is just the formal analogue of the standard practice of building simulators in conventional programming languages such as C. A largely unexplored but potentially very useful next step is symbolic simulation, the \execution" of the formal speci cation on indeterminant data. With the right interface, this need not require much additional training of the engineers using the tool. It allows many tests to be collapsed into one. Furthermore, it familiarizes ing engineer with the abstractions and notation used in the design, thus allowing team members to speak clearly to one another. We illustrate these ideas with a formal speci cation of a simple computing machine in ACL2. We sketch some requirements on the interface, which we call a symbolic spreadsheet.

• Type: Conference
• Year: 1998
• Where: FMCAD
• Authors: J. Strother Moore
• Keywords: Executable Formal Speci, FMCAD 1998, Formal Analogue, Formal Methods, Formal Speci Cation