Abstract
The application of predicate abstraction to parameterized systems requires the use of quantified predicates. These predicates cannot be found automatically by existing techniques and are tedious for the user to provide. In this work we demonstrate a method of discovering most of these predicates automatically by analyzing spurious abstract counter-example traces. Since predicate discovery for unbounded state systems is an undecidable problem, it can fail on some problems. The method has been applied to a simplified version of the Ad hoc On-Demand Distance Vector Routing protocol where it successfully discovers all required predicates.
This work was supported by National Science Foundation under grant number 0121403 and DARPA contract 00-C-8015. The content of this paper does not necessarily reflect the position or the policy of the Government and no official endorsement should be inferred.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
David L. Dill Aaron Stump, Clark W. Barrett. CVC: a cooperating validity checker. In Conference on Computer Aided Verification, Lecture notes in Computer Science. Springer-Verlag, 2002.
R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation 118(1), pages 142–157, 1995.
F. Balarin and A. L. Sangiovanni-Vincentelli. An iterative approach to language containment. In 5th International Conference on Computer-Aided Verification, pages 29–40. Springer-Verlag, 1993.
Thomas Ball and Sriram K. Rajamani. The SLAM project: debugging system software via static analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1–3. ACM Press, 2002.
Saddek Bensalem, Yassine Lakhnech, and Sam Owre. InVeSt: A tool for the verification of invariants. In 10th International Conference on Computer-Aided Verification, pages 505–510. Springer-Verlag, 1998.
Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter. Formal verification of standards for distance vector routing protocols, August 1999. Presented in the Recent Research Session at Sigcomm 1999.
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154–169. Springer-Verlag, 2000.
Michael A. Colón and Tomás E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Conference on Computer-Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 293–304. Springer-Verlag, 1998.
Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 51–60. IEEE Computer Society, 2001. June 2001, Boston, USA.
C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 2002.
Susanne Graf and Hassen Saïdi. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Conference on Computer Aided Verification, volume 1254 of Lecture notes in Computer Science, pages 72–83. Springer-Verlag, 1997. June 1997, Haifa, Israel.
Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, and Sam Owre. Incremental verification by abstraction. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TAC AS 2001, pages 98–112, Genova, Italy, 2001. Springer-Verlag.
D. Lessens and Hassen Saïdi. Automatic verification of parameterized networks of processes by abstraction. Electronic Notes of Theoretical Computer Science (ENTCS), 1997.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
Charles E. Perkins and Elizabeth M. Royer. Ad Hoc On-Demand Distance Vector (AODV) Routing. In Workshop on Mobile Computing Systems and Applications, pages 90–100. ACM Press, February 1999.
Charles E. Perkins, Elizabeth M. Royer, and Samir Das. Ad Hoc On-Demand Distance Vector (AODV) Routing. Available at http://www.ietf.org/internet-drafts/draft-ietf-manet-aodv-05.txt, 2000.
A. P. Sistla and S. M. German. Reasoning with many processes. In Symp. on Logic in Computer Science, Ithaca, pages 138–152. IEEE Computer Society, June 1987.
Rupak Majumdar Thomas A Henzinger, Ranjit Jhala and Gregoire Sutre. Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages. ACM Press, 2002.
A. Tiwari, H. Rueβ, H. Saïdi, and N. Shankar. A technique for invariant generation. In Tiziana Margaria and Wang Yi, editors, TACAS 2001-Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 113–127, Genova, Italy, apr 2001. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Das, S., Dill, D.L. (2002). Counter-Example Based Predicate Discovery in Predicate Abstraction. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_2
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive