Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published April 2017 | public
Book Section - Chapter Open

Osiris: A Tool for Abstraction and Verification of Control Software with Lookup Tables


Some industrial systems are difficult to formally verify 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 Osiris, a tool that automatically computes abstractions of lookup tables. Osiris uses these abstractions to verify a property in first order logic. If the verification fails, Osiris uses a falsification heuristic to search for a violation of the specification. We validate our technique on a public benchmark of an adaptive cruise controller with lookup tables.

Additional Information

© 2017 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Attached Files

Accepted Version - main.pdf


Files (787.1 kB)
Name Size Download all
787.1 kB Preview Download

Additional details

August 19, 2023
August 19, 2023