2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM) (2012)
Riva del Garda, Italy Italy
Sept. 23, 2012 to Sept. 24, 2012
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SCAM.2012.25
This tool paper describes the design and implementation of an interactive environment for discovering and browsing information flow in SPARK programs. SPARK is a subset of Ada that has been used in a number of industrial contexts for implementing certified safety and security critical systems. SPARK requires explicit specification of information flow properties in the form of procedure contracts. To write such contracts, developers need to understand the data and control dependencies in the program. Our tool Bakar Alir, implemented as an Eclipse Plug-in, utilizes classic slicing and chopping techniques to assist developers in writing information flow contracts.
IDE support, slicing, chopping, spark
Hariharan Thiagarajan, John Hatcliff, Jason Belt, Robby, "Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK", 2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM), vol. 00, no. , pp. 132-137, 2012, doi:10.1109/SCAM.2012.25