Skip to main content
Conference ProceedingsOPEN ACCESS

A tool for symbolic program verification and abstraction

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1993) 697 LNCS 71-84
DOI: 10.1007/3-540-56922-7_7
24Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

We give the description of a verification tool taking boolean programs of guarded commands as input; internal representation of programs are sets of Binary Decision Diagrams (BDD) (one for each guarded command). It allows to construct an abstract program of the same form obtained using an abstraction relation given by a boolean expression on “concrete”’ and “abstract” variables. The tool allows the verification of CTL formulas on programs. We illustrate its possibilities on an example.

Cite

CITATION STYLE

APA

Graf, S., & Loiseaux, C. (1993). A tool for symbolic program verification and abstraction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 697 LNCS, pp. 71–84). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free