A verification condition visualizer

Madiha Jami, Andrew Ireland*

*Corresponding author for this work

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

2 Citations (Scopus)
88 Downloads (Pure)

Abstract

When first encountering data structures such as arrays, records and pointers programmers are often presented with pictorial representations. The use of pictures to describe data structures and their manipulation can help establish basic programming intuitions. The same is true of program proving where pictures are frequently used within the literature to describe program properties such as loop invariants. Here we report on an experimental prototype of a visualization tool that translates verification conditions arising from array based code into pictures. While initially aimed at supporting teaching, we have received positive feedback from users of program proving tools within industry.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Pages72-86
Number of pages15
Volume8471
ISBN (Print)9783319121536
DOIs
Publication statusPublished - 1 Jan 2014
Event6th International Conference on Verified Software: Theories, Tool and Experiments - Vienna, United Kingdom
Duration: 17 Jul 201418 Jul 2014

Publication series

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

Conference

Conference6th International Conference on Verified Software: Theories, Tool and Experiments
Abbreviated titleVSTTE 2014
Country/TerritoryUnited Kingdom
CityVienna
Period17/07/1418/07/14

ASJC Scopus subject areas

  • General Computer Science
  • Theoretical Computer Science

Fingerprint

Dive into the research topics of 'A verification condition visualizer'. Together they form a unique fingerprint.

Cite this