A verification condition visualizer

Madiha Jami; Andrew Ireland

doi:10.1007/978-3-319-12154-3_5

A verification condition visualizer

Madiha Jami, Andrew Ireland^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer
Pages	72-86
Number of pages	15
Volume	8471
ISBN (Print)	9783319121536
DOIs	https://doi.org/10.1007/978-3-319-12154-3_5
Publication status	Published - 1 Jan 2014
Event	6th International Conference on Verified Software: Theories, Tool and Experiments - Vienna, United Kingdom Duration: 17 Jul 2014 → 18 Jul 2014

Publication series

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

Conference

Conference	6th International Conference on Verified Software: Theories, Tool and Experiments
Abbreviated title	VSTTE 2014
Country/Territory	United Kingdom
City	Vienna
Period	17/07/14 → 18/07/14

ASJC Scopus subject areas

General Computer Science
Theoretical Computer Science

Access to Document

10.1007/978-3-319-12154-3_5

Download pdf
he final publication is available at Springer via https://link.springer.com/chapter/10.1007%2F978-3-319-12154-3_5
Accepted author manuscript, 433 KBLicence: All Rights Reserved

Andrew Ireland
- A.Irelandhw.acuk
- School of Mathematical & Computer Sciences - Professor
- School of Mathematical & Computer Sciences, Computer Science - Professor
Person: Academic (Research & Teaching)

Cite this

Jami, M., & Ireland, A. (2014). A verification condition visualizer. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8471, pp. 72-86). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8471). Springer. https://doi.org/10.1007/978-3-319-12154-3_5

Jami, Madiha ; Ireland, Andrew. / A verification condition visualizer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8471 Springer, 2014. pp. 72-86 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ba092ba5eb4e4028aac16f0cbaeaf625,

title = "A verification condition visualizer",

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.",

author = "Madiha Jami and Andrew Ireland",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-319-12154-3_5",

language = "English",

isbn = "9783319121536",

volume = "8471",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "72--86",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

note = "6th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2014 ; Conference date: 17-07-2014 Through 18-07-2014",

}

Jami, M & Ireland, A 2014, A verification condition visualizer. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 8471, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8471, Springer, pp. 72-86, 6th International Conference on Verified Software: Theories, Tool and Experiments, Vienna, United Kingdom, 17/07/14. https://doi.org/10.1007/978-3-319-12154-3_5

A verification condition visualizer. / Jami, Madiha; Ireland, Andrew.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8471 Springer, 2014. p. 72-86 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8471).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A verification condition visualizer

AU - Jami, Madiha

AU - Ireland, Andrew

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-12154-3_5

DO - 10.1007/978-3-319-12154-3_5

M3 - Conference contribution

AN - SCOPUS:84909592612

SN - 9783319121536

VL - 8471

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 72

EP - 86

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer

T2 - 6th International Conference on Verified Software: Theories, Tool and Experiments

Y2 - 17 July 2014 through 18 July 2014

ER -

Jami M, Ireland A. A verification condition visualizer. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8471. Springer. 2014. p. 72-86. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-12154-3_5

A verification condition visualizer

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Fingerprint

Profiles

Andrew Ireland

Cite this