Learning to verify branching time properties
By
We present a new model checking algorithm for verifying computation tree logic (CTL) properties. To our knowledge, this is the first CTL model checking algorithm for infinite state systems that can also handle fairness constraints. Our technique is based on using language inference to learn the fixpoints necessary for checking a CTL formula instead of computing them iteratively as is done in traditional model checking. This allows us to analyze infinite or large state-space systems where the traditional iterations may not converge or may take too long to converge. Our procedure is guaranteed to terminate with the correct answer if fixpoints needed for all subformulas of the CTL property are regular. We have extended our L EVER tool to use the technique presented in this paper and demonstrate its effectiveness by verifying a number of parametric and integer systems.
BibTeX
@inproceedings{conf/kbse/VardhanV05,
author = "Vardhan, Abhay and Viswanathan, Mahesh",
editor = "Redmiles, David F. and Ellman, Thomas and Zisman,
Andrea",
title = "Learning to verify branching time properties",
booktitle = "ASE",
crossref = "conf/kbse/2005",
ee = "http://doi.acm.org/10.1145/1101908.1101961",
keywords = "formal methods, software engineering",
pages = "325-328",
year = "2005",
}
@proceedings{conf/kbse/2005,
editor = "Redmiles, David F. and Ellman, Thomas and Zisman,
Andrea",
title = "20th IEEE/ACM International Conference on Automated
Software Engineering (ASE 2005), November 7-11, 2005, Long Beach,
CA, USA",
publisher = "ACM",
year = "2005",
}