loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
16th IEEE International Conference on Automated Software Engineering (ASE'01)
Automata-Based Verification of Temporal Properties on Running Programs
San Diego, California
November 26-November 29
ISBN: 0-7695-1426-X
ASCII Text
x 
 
Dimitra Giannakopoulou, Klaus Havelund, "Automata-Based Verification of Temporal Properties on Running Programs," Automated Software Engineering, International Conference on, pp. 412, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001.
 
 
BibTex
x
 
@article{ 10.1109/ASE.2001.989841,
author = {Dimitra Giannakopoulou and Klaus Havelund},
title = {Automata-Based Verification of Temporal Properties on Running Programs},
journal ={Automated Software Engineering, International Conference on},
volume = {0},
year = {2001},
isbn = {0-7695-1426-X},
pages = {412},
doi = {http://doi.ieeecomputersociety.org/10.1109/ASE.2001.989841},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Automated Software Engineering, International Conference on
TI - Automata-Based Verification of Temporal Properties on Running Programs
SN - 0-7695-1426-X
SP
EP
A1 - Dimitra Giannakopoulou,
A1 - Klaus Havelund,
PY - 2001
VL - 0
JA - Automated Software Engineering, International Conference on
ER -
 
Dimitra Giannakopoulou, NASA Ames Research Center
Klaus Havelund, NASA Ames Research Center
This paper presents an approach to checking a running program against Linear Temporal Logic (LTL) specifications. LTL is a widely used logic for expressing properties of programs viewed as sets of executions. Our approach consists of translating LTL formulae to finite-state automata, which are used as observers of the program behavior. The translation algorithm we propose modifies standard LTL to B?chi automata conversion techniques to generate automata that check finite program traces. The algorithm has been implemented in a tool, which has been integrated with the generic JPaX framework for runtime analysis of Java programs.
Citation:
Dimitra Giannakopoulou, Klaus Havelund, "Automata-Based Verification of Temporal Properties on Running Programs," ase, pp.412, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.