Static detection of implementation errors using formal code specification

Iman Saleh, Gregory Kulczycki, M. Brian Blake, Yi Wei

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


The software engineering community suggests that formal specification of source code facilitates the verification that can help to identify hidden functional errors. In this work, we investigate the impact of various levels of formal specification on the ability to statically detect errors in code. Our goal is to quantify the return on investment with regards to the effectiveness of identifying errors versus the overhead of specifying software at various levels of detail. We looked at common algorithms and data structures implemented using C# and specified using Spec#. We selectively omitted various parts of the specification to come up with five different levels of specification, from unspecified to highly-specified. For each level of specification, we injected errors into the classes using a fault injection tool. Experimentation using a verifier showed that over 80% of the errors were detected from the highest specification levels while the levels in between generated mixed results. To the best of our knowledge, our study is the first to quantitatively measure the effect of formal methods on code quality. We believe that our work can help convince skeptics that formal methods can be practically integrated into programming activities to produce code with higher quality even with partial specification.

Original languageEnglish (US)
Title of host publicationSoftware Engineering and Formal Methods - 11th International Conference, SEFM 2013, Proceedings
Number of pages15
StatePublished - Oct 24 2013
Event11th International Conference on Software Engineering and Formal Methods, SEFM 2013 - Madrid, Spain
Duration: Sep 25 2013Sep 27 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8137 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other11th International Conference on Software Engineering and Formal Methods, SEFM 2013


  • Experimentation
  • Formal Methods
  • Mutation Testing

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science


Dive into the research topics of 'Static detection of implementation errors using formal code specification'. Together they form a unique fingerprint.

Cite this