SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

SPARKSMT - An SMTLIB processing tool written in SPARK - Part I

by Florian Schanda in Dev Projects, Formal Verification – April 21, 2016

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, I intend to focus on the how I have proved absence of run-time errors in the name table and lexer. I had two objectives: show absence of run-time errors, and do not write useless defensive code. Today's blog will be about the name table, a data structure found in many compilers that can map strings to a unique integer and back. The next blog post will talk about the lexical analyzer.