A Caltech Library Service

Fast Automatic Verification of Large-Scale Systems with Lookup Tables

Arichega, Nikos and Dathathri, Sumanth and Vernekar, Shashank and Gao, Sicun and Shiraishi, Shin’Ichi and Murray, Richard M. (2017) Fast Automatic Verification of Large-Scale Systems with Lookup Tables. . (Unpublished)

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


Modern safety-critical systems are difficult to formally verify, largely due to their large scale. In particular, the widespread use of lookup tables in embedded systems across diverse industries, such as aeronautics and automotive systems, create a critical obstacle to the scalability of formal verification. This paper presents a novel approach for the formal verification of large-scale systems with lookup tables. We use a learning-based technique to automatically learn abstractions of the lookup tables and use the abstractions to then prove the desired property. If the verification fails, we propose a falsification heuristic to search for a violation of the specification. In contrast with previous work on lookup table verification, our technique is completely automatic, making it ideal for deployment in a production environment. To our knowledge, our approach is the only technique that can automatically verify large-scale systems lookup with tables. We illustrate the effectiveness of our technique on a benchmark which cannot be handled by the commercial tool SLDV, and we demonstrate the performance improvement provided by our technique.

Item Type:Report or Paper (Discussion Paper)
Murray, Richard M.0000-0002-5785-7481
Record Number:CaltechAUTHORS:20200131-144053728
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:101040
Deposited By: Tony Diaz
Deposited On:31 Jan 2020 22:58
Last Modified:31 Jan 2020 22:58

Repository Staff Only: item control page