AAAI Publications, Twenty-Seventh AAAI Conference on Artificial Intelligence

Font Size: 
A First-Order Logic Based Framework for Verifying Simulations
Hui Meen Nyew, Nilufer Onder, Soner Onder, Zhenlin Wang

Last modified: 2013-06-29


Modern science relies on simulation techniques for understanding phenomenon, exploring design options, or evaluating models. Assuring the correctness of simulators is a key problem where a multitude of solutions ranging from manual inspection to formal verification are applicable. Formal verification incorporates the rigor necessary but not all simulators are generated from formal specifications. Manual inspection is readily available but lacks the rigor and is prone to errors. In this paper, we describe an automated verification system (AVS) where the constraints that the system must adhere to are specified by the user in general purpose first-order logic. AVS translates these constraints into a verification program that scans the simulator traceand verifies that no constraints are violated. Computer microarchitecture simulations were successfully used to demonstrate the proposed approach. This paper describes the preliminary results and discusses how artificial intelligence techniques can be used to facilitate effective run-time verification of simulators.


Runtime Verification;Constraint Satisfaction Problem; Data Stream Mining;First-Order Logic

Full Text: PDF