Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK
- 1 September 2012
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2012 IEEE 12th International Working Conference on Source Code Analysis and Manipulation
- p. 132-137
- https://doi.org/10.1109/scam.2012.25
Abstract
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.Keywords
This publication has 7 references indexed in Scilit:
- Slicing concurrent Java programs using Indus and KaveriInternational Journal on Software Tools for Technology Transfer, 2007
- Efficient path conditions in dependence graphs for software safety analysisACM Transactions on Software Engineering and Methodology, 2006
- Bogor: A Flexible Framework for Creating Software Model CheckersPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Efficient path conditions in dependence graphsPublished by Association for Computing Machinery (ACM) ,2002
- BanderaPublished by Association for Computing Machinery (ACM) ,2000
- Precise interprocedural choppingPublished by Association for Computing Machinery (ACM) ,1995
- Interprocedural slicing using dependence graphsPublished by Association for Computing Machinery (ACM) ,1988