Controlling Polyvariance for Specialization-based Verification

• Autorzy: Fioravanti F. , Pettorossi A. , Proietti M. , Senni V.
• Języki publikacji: EN

Abstrakty

EN

Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise.

Słowa kluczowe

EN

constraint logic programming; generalization; polyvariance; program specialization; unfold/fold transformation; verification of infinite state reactive systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 124, nr 4
• Strony: 483--502
• Opis fizyczny: Bibliogr. 32 poz., wykr.

Twórcy

autor

Fioravanti F.

• University of Chieti-Pescara, Viale Pindaro 42, 65127 Pescara, Italy

autor

Pettorossi A.

• University of Rome Tor Vergata, Via del Politecnico 1, 00133 Rome, Italy

autor

Proietti M.

• IASI-CNR, Viale Manzoni 30, 00185 Rome, Italy

autor

Senni V.

• IMT Institute for Advanced Studies Lucca, Piazza San Ponziano 6, 55100 Lucca, Italy

Bibliografia

• [1] A. Annichini, A. Bouajjani, and M. Sighireanu. TReX: A tool for reachability analysis of complex systems. In Proc. of CAV 2001, Lecture Notes in Computer Science 2102, pages 368-372. Springer, 2001.
• [2] G. Banda and J. P. Gallagher. Analysis of linear hybrid systems in CLP. In Proc. of LOPSTR 2008, Lecture Notes in Computer Science 5438, pages 55-70. Springer, 2009.
• [3] G. Banda and J. P. Gallagher. Constraint-based abstract semantics for temporal logic: A direct approach to design and implementation. In Proc. of LPAR 2010, Lecture Notes in Artificial Intelligence 6355, pages 27-45. Springer, 2010.
• [4] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Acceleration from theory to practice. Int. J. on Software Tools for Technology Transfer, 10(5):401-424,2008.
• [5] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [6] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-Guided Abstraction Refinement. In Proc. of CAV 2000, Lecture Notes in Computer Science 1855, pages 154-169. Springer, 2000.
• [7] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. of the Fifth ACM Symposium on Principles of Programming Languages (POPL’78), pages 84-96. ACM Press, 1978.
• [8] S.-J. Craig and M. Leuschel. A compiler generator for constraint logic programs. In M. Broy and A. V Zamulin, editors, 5th Ershov Memorial Conference on Perspectives of Systems Informatics, PSI2003, Lecture Notes in Computer Science 2890, pages 148-161. Springer, 2003.
• [9] G. Delzanno and A. Podelski. Constraint-based deductive model checking. Int. J. on Software Tools for Technology Transfer, 3(3):250-270,2001.
• [10] N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1-2):69-116,1987.
• [11] E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Software Model Checking by Program Specialization. In Proc. of the 9th Italian Convention on Computational Logic (CILC’12), CEUR-WS Vol.857. 2012.
• [12] J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34(2):85- 107, 1997.
• [13] S. EtalleandM. Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166:101-146, 1996.
• [14] F. Fioravanti, A. Pettorossi, and M. Proietti. Automated strategies for specializing constraint logic programs. In Proc. ofLOPSTR ’00, Lecture Notes in Computer Science 2042, pages 125-146. Springer-Verlag, 2001.
• [15] F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying CTL properties of infinite state systems by specializing constraint logic programs. In Proc. ofVCL’01, Tech. Rep. DSSE-TR-2001-3, pages 85-96. University of Southampton, UK, 2001.
• [16] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Improving Reachability Analysis of Infinite State Systems by Specialization. In Proc. ofRP 2011, Lecture Notes in Computer Science 6945, pages 165-179. Springer, 2011.
• [17] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Generalization Strategies for the Verification of Infinite State Systems. Theory and Practice of Logic Programming. Available on CJO doi:10.1017/S1471068411000627. Cambridge, 2012.
• [18] G. Frehse. PHAVer: Algorithmic verification of hybrid systems past HyTech. In M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Lecture Notes in Computer Science 3414, pages 258-273. Springer, 2005.
• [19] L. Fribourg. Constraint logic programming applied to model checking. In A. Bossi, editor, Proc. of the 9th International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR ’99), Venezia, Italy, Lecture Notes in Computer Science 1817, pages 31-42. Springer-Verlag, 2000.
• [20] J. P. Gallagher. Tutorial on specialisation of logic programs. In Proc. of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM ’93, Copenhagen, Denmark, pages 88-98. ACM Press, 1993.
• [21] T. J. Hickey and D. A. Smith. Towards the partial evaluation of CLP languages. In Proc. of the 1991 ACM Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM ’91, New Haven, CT, USA, SIGPLAN Notices, 26, 9, pages 43-51. ACM Press, 1991.
• [22] J. Jaffar, M. Maher, K. Marriott, and P. Stuckey. The semantics of constraint logic programming. Journal of Logic Programming, 37:1-46, 1998.
• [23] N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
• [24] LASH. homepage: http://www.montefiore.ulg.ac.be/~boigelot/research/lash.
• [25] M. Leuschel and M. Bruynooghe. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming, 2(4&5):461-515,2002.
• [26] M. Leuschel, B. Martens, and D. De Schreye. Controlling generalization and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems, 20(1):208-258, 1998.
• [27] M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In Proceedings ofLOPSTR ’99, Lecture Notes in Computer Science 1817, pages 63-82. Springer, 2000.
• [28] J. W. Lloyd and J. C. Shepherdson. Partial evaluation in logic programming. Journal of Logic Programming, 11:217-242,1991.
• [29] MAP. The MAP transformation system web interface: http: //map. uniroma2. it/mapweb .
• [30] C. Ochoa, G. Puebla, and M. V Hermenegildo. Removing superfluous versions in polyvariant specialization of Prolog programs. In Proc. of LOPSTR ’05, Lecture Notes in Computer Science 3961, pages 80-97. Springer, 2006.
• [31] J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In Proc. of LOPSTR ’02, Lecture Notes in Computer Science 2664, pages 90-108. Springer, 2003.
• [32] T. Yavuz-Kahveci and T. Bultan. Action Language Verifier: An infinite-state model checker for reactive software specifications. Formal Methods in System Design, 35(3):325-367,2009.