zbMATH — the first resource for mathematics

Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. (English) Zbl 1452.68116
Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 58-75 (2017).
Summary: Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA. In this paper, we present a counterexample-guided abstraction refinement (CEGAR) approach that leverages linearization techniques from differential calculus to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The results of an empirical evaluation confirm the validity and potential of this approach.
For the entire collection see [Zbl 1360.68015].
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Full Text: DOI
[1] Ábrahám, E., Corzilius, F., Loup, U., Sturm, T.: A lazy SMT-solver for a non-linear subset of real algebra. In: Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum f A1/4r Informatik (2010)
[2] Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 128-133. ACM (2015) · Zbl 1364.68244
[3] Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193-207. Springer, Heidelberg (1999). doi:10.1007/3-540-49059-0_14
[4] Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831-848. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_55
[5] Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D.: Interpolation-based verification of floating-point programs with abstract CDCL. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 412-432. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_22
[6] Brat, G., Bushnell, D., Davies, M., Giannakopoulou, D., Howar, F., Kahsai, T.: Verifying the safety of a flight-critical system. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 308-324. Springer, Heidelberg (2015). doi:10.1007/978-3-319-19249-9_20
[7] Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334-342. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_22
[8] Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347-366. Springer, Cham (2016). doi:10.1007/978-3-319-41591-8_24
[9] Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46-61. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_4 · Zbl 1368.68245
[10] Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52-67. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_4
[11] Cimatti, A., Mover, S., Tonetta, S.: A quantifier-free SMT encoding of non-linear hybrid automata. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 187-195. IEEE (2012)
[12] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition-preliminary report. SIGSAM Bull. 8(3), 80-90 (1974). http://doi.acm.org/10.1145/1086837.1086852
[13] Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24
[14] Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737-744. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_49
[15] Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543-560 (2003) · Zbl 1271.68215
[16] Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208-214. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_14 · Zbl 1381.68268
[17] Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: Proceedings of the 13th International Workshop on Satisfiability Modulo Theories (SMT), pp. 373-384 (2015)
[18] Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157-171. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_13 · Zbl 1273.68229
[19] Hueschen, R.M.: Development of the Transport Class Model (TCM) aircraft simulation from a sub-scale Generic Transport Model (GTM) simulation. Technical report, NASA Langley Research Center (2011)
[20] Jovanović, D., Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339-354. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_27 · Zbl 1358.68257
[21] Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Form. Methods Syst. Des. 48(3), 175-205 (2016) · Zbl 1358.68072
[22] Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \({\delta }\)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200-205. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_15
[23] Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240-255. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_17 · Zbl 1348.68141
[24] Mahdi, A., Scheibler, K., Neubauer, F., Fränzle, M., Becker, B.: Advancing software model checking beyond linear arithmetic theories. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 186-201. Springer, Heidelberg (2016). doi:10.1007/978-3-319-49052-6_12
[25] Maréchal, A., Fouilhé, A., King, T., Monniaux, D., Périn, M.: Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166-184. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_8 · Zbl 06559857
[26] McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1-13. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_1 · Zbl 1278.68184
[27] Nuzzo, P., Puggelli, A., Seshia, S.A., Sangiovanni-Vincentelli, A.: CalCS: SMT solving for non-linear convex constraints. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pp. 71-80. FMCAD Inc. (2010)
[28] Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. MBMV 13, 231-241 (2013)
[29] Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127-144. Springer, Heidelberg (2000). doi:10.1007/3-540-40922-X_8
[30] Tiwari, A.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.