Content by Florian Schanda
Florian Schanda
SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I
Today I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features,…
SPARK 2016 Supports Ravenscar!
The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write…
SPARK 2014 Rationale: Variables That Are Constant
The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables…
SPARK 2014 Rationale: Information Flow
In a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and…
Information Flo(w): Array Initialization in Loops
SPARK only supported array initialization using aggregates, as array initialization in loops raised a false alarm in flow analysis. Read on to learn…
SPARK 2014 Rationale: Data Dependencies
Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading…
SPARK 2014 Flow Analysis
We have nearly finished implementing a central component of the SPARK 2014 analysis tools: the flow analysis engine; so this is a good time to…