A tool for symbolic program verification and abstraction
| Autor: | Susanne Graf, Claire Loiseaux |
|---|---|
| Rok vydání: | 1993 |
| Předmět: |
Theoretical computer science
Program analysis Relation (database) Binary decision diagram Computer science Computer Science::Logic in Computer Science Symbolic trajectory evaluation Computer Science::Programming Languages Boolean expression Construct (python library) Representation (mathematics) Abstraction (linguistics) |
| Zdroj: | Computer Aided Verification ISBN: 9783540569220 CAV |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|