Blog Posts by Florian Schanda
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,…
Florian Schanda
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…
Florian Schanda
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…
Florian Schanda
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…
Florian Schanda
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…
Florian Schanda
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…
Florian Schanda
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…