uberSpark is an innovative system architecture and programming principle for compositional verification of security properties of commodity (extensible) system software written in C and Assembly.
uberSpark has been used to build and verify security invariants of the uber eXtensible Micro-Hypervisor Framework (<https://uberxmhf.org>) and several of its extensions, and demonstrating only minor performance overhead with low verification costs.
Visit: <https://uberspark.org> for more information on how to download, build, install, contribute and get involved.
The formatted documentation can be read online at: <https://uberspark.org/docs/toc.html>
Documentation sources are within docs/
## Contact and Maintainer Amit Vasudevan (<https://hypcode.org>)
The uberSpark project comprises multiple open source licenses. See COPYING for details.