Summary
• We are developing a simulator for SDL
specifications
• We are using ACL2 for the development and
verification of the simulator
• The goal is to provide a framework for
verification of SDL specifications using a
theorem prover
• The simulator also helps in testing of
implementations: acts as a test driver and
helps compute expected results for test cases