A Framework for the Verification of Parameterized Infinite-state Systems

• Autorzy: Alberti F. , Ghilardi S. , Sharygina N.

Identyfikatory

DOI

10.3233/FI-2017-1458

• Języki publikacji: EN

Abstrakty

EN

We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application domains, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.

Słowa kluczowe

EN

infinite-state systems; software model-checking; arrays; quantifiers; satisfiability modulo theories

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 1
• Strony: 1--24
• Opis fizyczny: Bibliogr. 43 poz., rys., tab., wykr.

Twórcy

autor

Alberti F.

• Network Support System, Eolo SpA, via Gran San Bernardo, 12, 21052 Busto Arsizio, Italy

autor

Ghilardi S.

• Department of Mathematics, Università degli Studi di Milano, via Saldini, 50, 20133 Milano, Italy

autor

Sharygina N.

• Faculty of Informatics, Università della Svizzera Italiana, via G. Buffi, 13, CH-6900 Lugano, Switzerland

Bibliografia

• [1] Alberti F, Ghilardi S, Sharygina N. Booster: An Acceleration-Based Verification Framework for Array Programs. In: Cassez F, Raskin J (eds.), Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science. Springer, 2014 pp. 18-23. doi: 10.1007/978-3-319-11936-6_2.
• [2] Alberti F, Ghilardi S, Sharygina N. A Framework for the Verification of Parameterized Infinite-State Systems. In: Giordano L, Gliozzi V, Pozzato GL (eds.), Proceedings of the 29th Italian Conference on Computational Logic, Torino, Italy, June 16-18, 2014., volume 1195 of CEUR Workshop Proceedings CEUR-WS.org, 2014 pp. 303-308.
• [3] Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N. An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design, 2014; 45 (1): 63-109. doi: 10.1007/s 10703-014-0209-9.
• [4] Alberti F, Ghilardi S, Sharygina N. Definability of Accelerated Relations in a Theory of Arrays and Its Applications. In: Fontaine P, Ringeissen C, Schmidt RA (eds.), Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science. Springer, 2013 pp. 23-39. doi: 10.1007/978-3-642-40885-4_3.
• [5] Alberti F, Ghilardi S, Sharygina N. Decision Procedures for Flat Array Properties. In: Ábráham E. Havelund K (eds.), Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science. Springer, 2014 pp. 15-30. doi: 10.1007/978-3-642-54862-8_2.
• [6] McMillan K. Lazy Abstraction with Interpolants. In: Ball T, Jones RB (eds.), Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science. Springer, 2006 pp. 123-136. doi: 10.1007/11817963_14.
• [7] Conchon S., Goel A, Krstic S, Mebsout A, Zaïdi F. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In: Madhusudan and Seshia [43], 2012 pp. 718-724. doi: 10.1007/978-3-642-31424-7_55.
• [8] Conchon S., Goel A, Krstic S, Mebsout A, Zaïdi F. Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 2013, pp. 61-68. URL http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=6679392.
• [9] Halbwachs N, Péron M. Discovering properties about arrays in simple programs. In: Gupta R, Amarasinghe SP (eds.), Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. ACM, 2008 pp. 339-348. URL http://doi.acm.org/10.1145/1379022.1375623.
• [10] Dillig I., Dillig T, Aiken A. Fluid Updates: Beyond Strong vs. Weak Updates. In: Gordon AD (ed.), Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6012 of Lecture Notes in Computer Science, pp. 246-266. Springer, 2010. URL http://dx.doi.org/10.1007/978-3-642-11957-6_14.
• [11] Cousot P, Cousot R, Logozzo F. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. In: POPL. 2011; 46 (1): 105-118. doi: 10.1145/1925844.1926399.
• [12] De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Verifying Array Programs by Transforming Verification Conditions. In: McMillan KL, Rival X (eds.), Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceed- volume 8318 of Lecture Notes in Computer Science. Springer, 2014 pp. 182-202. doi: 10.1007/978-3-642-54013-4_11.
• [13] Seghir M, Podelski A, Wies T. Abstraction Refinement for Quantified Array Assertions. In: Palsberg J, Su Z (eds.), Static Analysis, 16th International Symposium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings, volume 5673 of Lecture Notes in Computer Science. Springer, 2009 pp. 3-19. doi: 10.1007/978-3-642-03237-0_3.
• [14] Lahiri S, Bryant R. Predicate abstraction with indexed predicates. ACM Trans. Comput. Log., 2007; 9 (1). doi: 10.1145/1297658.1297662.
• [15] Srivastava S, Gulwani S. Program verification using templates over predicate abstraction. In: Hind M., Diwan A (eds.), Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009. ACM, 2009 pp. 223-234. doi: 10.1145/1542476.1542501.
• [16] Larraz D, Rodriguez-Carbonell E, Rubio A. SMT-Based Array Invariant Generation. In: Giacobazzi R, Berdine J, Mastroeni I (eds.), Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, volume 7737 of Lecture Notes in Computer Science. Springer, 2013 pp. 169-188. doi: 10.1007/978-3-642-35873-9_12.
• [17] Bjømer N, McMillan K, Rybalchenko A. On Solving Universally Quantified Horn Clauses. In: Logozzo F, Fähndrich M (eds.), Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science. Springer, 2013 pp. 105-125. doi: 10.1007/978-3-642-38856-9_8.
• [18] Comon H, Jurski Y. Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. In: Hu AJ, Vardi MY (eds.), Computer Aided Verification, 10th International Conference, CAV’98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science. Springer, 1998 pp. 268-279. doi: 10.1007/BFb0028751.
• [19] Bozga M, Iosif R, Lakhnech Y. Flat Parametric Counter Automata. Fundam. Inform., 2009; 91 (2): 275-303. doi: 10.3233/FI-2009-0044.
• [20] Bozga M, Gîrlea C, Iosif R. Iterating Octagons. In: Kowalewski S, Philippou A (eds.), Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK. March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science. Springer, 2009 pp. 337-351. doi: 10.1007/978-3-642-00768-2_29.
• [21] Finkel A, Leroux J. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In: Agrawal M, Seth A (eds.), FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002, Proceedings, volume 2556 of Lecture Notes in Computer Science. Springer, 2002 pp. 145-156. doi: 10.1007/3-540-36206-1_14.
• [22] Bozga M, Iosif R, Konecný F. Fast Acceleration of Ultimately Periodic Relations. In: Touili T, Cook B, Jackson P (eds.), Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh. UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science. Springer, 2010 pp. 227-242. doi: 10.1007/978-3-642-14295-6_23.
• [23] Bozga M, Habermehl P, Iosif R, Konecný F, Vojnar T. Automatic Verification of Integer Array Programs. In: Bouajjani A, Maler O (eds.), Computer Aided Verification, 21st International Conference, CAV 2009. Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science. Springer, 2009 pp. 157-172. doi: 10.1007/978-3-642-02658-4_15.
• [24] Gurfinkel A, Chaki S, Sapra S. Efficient Predicate Abstraction of Program Summaries. In: Bobaru MG. Havelund K, Holzmann GJ, Joshi R (eds.), NASA Formal Methods - Third International Symposium. NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, volume 6617 of Lecture Notes in Computer Science. Springer, 2011 pp. 131-145. doi: 10.1007/978-3-642-20398-5_11.
• [25] Gulwani S, Tiwari A. Combining abstract interpreters. In: Schwartzbach MI, Ball T (eds.), Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa. Ontario, Canada, June 11-14, 2006. ACM, 2006 pp. 376-386. doi: 10.1145/1133981.1134026.
• [26] Cousot P, Cousot R. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Graham RM, Harrison MA, Sethi R (eds.), Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles California, USA, January 1977. ACM, 1977 pp. 238-252. doi: 10.1145/512950.512973.
• [27] Bagnara R, Hill P, Mazzi E, Zaffanella E. Widening Operators for Weakly-Relational Numeric Abstractions. In: Hankin C, Siveroni I (eds.), Static Analysis, 12th International Symposium, SAS 2005, London UK, September 7-9, 2005, Proceedings, volume 3672 of Lecture Notes in Computer Science. Springe: 2005 pp. 3-18. doi: 10.1007/11547662_3.
• [28] Logozzo F, Fähndrich M. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. Sci. Comput. Program., 2010; 75 (9): 796-807. doi: 10.1016/j.scico.2009.04.004.
• [29] De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Program verification via iterated specialization. Sci. Comput. Program., 2014; 95: 149-175. doi: 10.1016/j.scico.2014.05.017.
• [30] Cousot P, Halbwachs N. Automatic Discovery of Linear Restraints Among Variables of a Program, In: Aho AV, Zilles SN, Szymanski TG (eds.), Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978. ACM Press, 1978 pp. 84-96. doi: 10.1145/512760.512770.
• [31] Bagnara R. Hill P, Ricci E, Zaffanella E. Precise Widening Operators for Convex Polyhedra. In: Cousot R (ed.) Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings, volume 2694 of Lecture Notes in Computer Science. Springer, 2003 pp. 337-354. doi: 10.1007/3-540-44898-5_19.
• [32] Alberti F., Ghilardi S, Sharygina N. Decision Procedures for Flat Array Properties. J. Autom. Reasoning, 2015; 54 (4): 327-352. doi: 10.1007/s10817-015-9323-7.
• [33] de Moura L., Bjørner N. Z3: An Efficient SMT Solver. In: Ramakrishnan CR, Rehof J (eds.), Tools and Algorithms for the Construction and Analysis of Systems 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science Springer, 2008 pp. 337-340. doi: 10.1007/978-3-540-78800-3_24.
• [34] Alberti F., Ghilardi S, Sharygina N. Monotonic Abstraction Techniques: from Parametric to Software Model Checking. In: Bersani MM, Bresolin D, Ferrucci L, Mazzara M (eds.), Proceedings First on Logics and Model-checking for Self-* Systems, MOD* 2014, Bertinoro, Italy, 12th September 2014., volume 168 of EPTCS. 2014 pp. 1-11. doi: 10.4204/EPTCS.168.1.
• [35] Biere A., Cimatti A, Clarke E, Zhu Y. Symbolic Model Checking without BDDs. In: Cleaveland R (ed.), Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS’99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, volume 1579 of Lecture Notes in Computer Science. Springer, 1999 pp. 193-207. doi: 10.1007/3-540-49059-0_14.
• [36] Abdulla P, Cerans K, Jonsson B, Tsay Y. General Decidability Theorems for Infinite-State Systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA. July 27-30, 1996. IEEE Computer Society, 1996 pp. 313-321. doi: 10.1109/LICS. 1996.561359.
• [37] Abdulla P, Delzanno G, Rezine A. Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods in System Design, 2009; 34 (2): 126-156. doi: 10.1007/s10703-008-0062-9.
• [38] Abdulla P, Delzanno G, Henda N, Rezine A. Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). In: Grumberg O, Huth M (eds.), Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science. Springer, 2007 pp. 721-736. doi: 10.1007/978-3-540-71209-1_56.
• [39] Alberti F. Bruttomesso R, Ghilardi S, Ranise S, Sharygina N. Lazy Abstraction with Interpolants for Arrays. In: Bjørner N, Voronkov A (eds.), Logic for Programming, Artificial Intelligence, and Reasoning – 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of Lecture Notes in Computer Science. Springer, 2012 pp. 46-61. doi: 10.1007/978-3-642-28717-6_7.
• [40] Alberti F., Bruttomesso R, Ghilardi S, Ranise S, Sharygina N. SAFARI: SMT-Based Abstraction for Arrays with Interpolants. In: Madhusudan and Seshia [43], 2012 pp. 679-685. doi: 10.1007/978-3-642-31424-7_49.
• [41] Ghilardi S, Ranise S. MCMT: A Model Checker Modulo Theories. In: Giesl J, Hähnle R (eds.), Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science. Springer, 2010 pp. 22-29. doi: 10.1007/978-3-642-14203-1_3.
• [42] Alberti F, Monniaux D. Polyhedra to the rescue of array interpolates. In: Wainwright RL, Corchado JM, Bechini A, Hong J (eds.), Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13-17, 2015. ACM, 2015 pp. 1745-1750. doi: 10.1145/2695664.2695784.
• [43] Madhusudan P, Seshia S (eds.). Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science. Springer, 2012. doi: 10.1007/978-3-642-31424-7.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).