Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6876208 | Theoretical Computer Science | 2014 | 16 Pages |
Abstract
For this purpose, we investigate the use of program specifications in QIF. We present criteria for specification admissibility and a program analysis that replaces exhaustive program exploration with symbolic execution, while incorporating user-supplied (but machine-checked) specifications. This kind of program analysis allows to trade automation for scalability, e.g., to programs with unbounded loops. Furthermore, we show how symbolic projection and counting, based in this instance on symbolic manipulation of polyhedra, avoid subsequent leak enumeration and enable precise QIF for programs with large leaks.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Vladimir Klebanov,