loading...
An Algorithm for Automated Generation of Invariants for Loops with Conditionals
Timisoara, Romania September 25-September 29
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SYNASC.2005.19Seventh International Symposium on Sy ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Laura Ildikó Kovács, Tudor Jebelean, "An Algorithm for Automated Generation of Invariants for Loops with Conditionals," Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on, pp. 245-249, Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/SYNASC.2005.19,
author = {Laura Ildikó Kovács and Tudor Jebelean},
title = {An Algorithm for Automated Generation of Invariants for Loops with Conditionals},
journal ={Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on},
volume = {0},
year = {2005},
isbn = {0-7695-2453-2},
pages = {245-249},
doi = {http://doi.ieeecomputersociety.org/10.1109/SYNASC.2005.19},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on
TI - An Algorithm for Automated Generation of Invariants for Loops with Conditionals
SN - 0-7695-2453-2
SP245
EP249
A1 - Laura Ildikó Kovács,
A1 - Tudor Jebelean,
PY - 2005
KW - null
VL - 0
JA - Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on
ER -
 
Laura Ildikó Kovács, Johannes Kepler University and Institute e-Austria
Tudor Jebelean, Johannes Kepler University and Institute e-Austria
We present an algorithm that generates automatically (algebraic) invariant properties of a loop with conditionals. In the proposed algorithm program analysis is performed in order to transform the code into a form for which algebraic and combinatorial techniques can be applied to obtain invariant properties. These invariants are then used for verifying partial correctness of imperative programs in the Theorema system (www.theorema.org). The application of the method is demonstrated in few examples.
Citation:
Laura Ildikó Kovács, Tudor Jebelean, "An Algorithm for Automated Generation of Invariants for Loops with Conditionals," synasc, pp.245-249, Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.