×

zbMATH — the first resource for mathematics

Higher-order quantifier elimination, counter simulations and fault-tolerant systems. (English) Zbl 07356977
Summary: We develop quantifier elimination procedures for fragments of higher order logic arising from the formalization of distributed systems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of pre/post images and of projections. We show in particular that our procedures are quite effective in producing counter abstractions that can be model-checked using standard SMT technology. In fact, very often in the current literature verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. In this work, we supply logical foundations to this practice, by our technique for second order quantifier elimination. We implemented our procedure for a simplified (but still expressive) subfragment and we showed that our method is able to successfully handle verification benchmarks from various sources with interesting performances.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Software:
ETPS; SeaHorn; ByMC; nuXmv; Mcmt
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS, pp. 313-321 (1996)
[2] Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers. In: TACAS, volume 4424 of LNCS, pp. 721-736 (2007) · Zbl 1186.68312
[3] Alberti, F., Ghilardi, S., Orsini, A., Pagani, E.: Counter abstractions in model checking of distributed broadcast algorithms: Some case studies. In: Proceedings of CILC, CEUR Proceedings, pp. 102-117 (2016)
[4] Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments. In: Proceedings of the IJCAR, volume 9706 of Lecture Notes in Computer Science, pp. 65-81 (2016) · Zbl 06623254
[5] Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods in System Design (2017) · Zbl 1377.68125
[6] Alberti, F.; Ghilardi, S.; Sharygina, N., Decision procedures for flat array properties, J. Autom. Reason., 54, 4, 327-352 (2015) · Zbl 1356.03049
[7] Andrews, PB, An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series (2002), Dordrecht: Kluwer, Dordrecht
[8] Babaoglu, O., Toueg, S.: Non-blocking atomic commitment. In: Distributed Systems, 2nd edn., pp. 147-168, Sape Mullender Ed., Addison-Wesley (1993)
[9] Ben-Or, M.: Another advantage of free choice: completely asynchronous agreement protocols. In: Proceedings of the PODC, pp. 27-30 (1983)
[10] Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: Proceedings of the PODC, pp. 244-253 (2007) · Zbl 1283.68079
[11] Bjørner, N., von Gleissenthall, K., Rybalchenko, A.: Cardinalities and universal quantifiers for verifying parameterized systems. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2016)
[12] Bracha, G.; Toueg, S., Asynchronous consensus and broadcast protocols, JACM, 32, 4, 824-840 (1985) · Zbl 0628.68024
[13] Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: CAV, pp. 334-342 (2014)
[14] Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: Stabilization, Safety, and Security of Distributed Systems, LNCS. pp. 120-134. Springer, Berlin (2011)
[15] Charron-Bost, B.; Schiper, A., Uniform consensus is harder than consensus, J. Algorithms, 51, 1, 15-37 (2004) · Zbl 1078.68157
[16] Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. In: Distributed Computing, pp. 49-71 (2009) · Zbl 1267.68151
[17] Cimatti, A., Griggio, A.: Software model checking via IC3. In: CAV, pp. 277-293 (2012)
[18] Delzanno, G., Constraint-based verification of parameterized cache coherence protocols, Form. Methods Syst. Design, 23, 3, 257-301 (2003) · Zbl 1073.68518
[19] Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Proceedings of CSL, volume 1683 of LNCS, pp. 50-66 (1999) · Zbl 0944.68139
[20] Dijkstra, EW; Genuys, F., Cooperating sequential processes, Programming Languages (1968), New York: Academic Press, New York
[21] Dragoj, C., Henzinger, T., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: Proceedings of the VMCAI (2014) · Zbl 1428.68371
[22] Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of LICS, pp. 352-359. IEEE Computer Society (1999)
[23] Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Proceedings of the TACAS, 2008. Full paper at https://www.researchgate.net/publication/220852375_On_Verifying_Fault_Tolerance_of_Distributed_Protocols · Zbl 1134.68317
[24] Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191-202 (2002) · Zbl 1323.68371
[25] Gabbay, D.M., Schmidt, R., Szalas, A.: Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications. ACM Digital Library (2008) · Zbl 1165.03011
[26] Ghilardi, S., Pagani, E.: Counter simulations via higher order quantifier elimination: a preliminary report. In: Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 Sept. 2017, pp. 39-53 (2017)
[27] Ghilardi, S., Pagani, E.: Second order quantifier elimination: towards verification applications. In: Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, December 6-8, 2017, pp. 36-50 (2017)
[28] Ghilardi, S.; Ranise, S., Backward reachability of array-based systems by SMT solving: termination and Invariant Synthesis, Log. Methods Comput. Sci., 1, 2 (2010) · Zbl 1213.68379
[29] Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: IJCAR, pp. 22-29 (2010) · Zbl 1291.68257
[30] Guerraoui, R., On the hardness of failure-sensitive agreement problems, Inf. Process. Lett., 79, 99-104 (2001) · Zbl 1052.68013
[31] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: CAV, pp. 343-361 (2015)
[32] Hoder, K., Bjørner, N.: Generalized property directed reachability. In: SAT, pp. 157-171 (2012) · Zbl 1273.68229
[33] Hoder, K., Bjørner, N., de Moura, L.: \( \mu\) Z—an efficient engine for fixed points with constraints. In: CAV, pp. 457-462 (2011)
[34] John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 201-209 (2013, Aug)
[35] John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Proceedings of the International SPIN Symposium on Model Checking of Software, volume 7976 of Lecture Notes in Computer Science, pp. 209-226. Springer, Berlin (2013, July)
[36] Konnov, I.: ByMC: Byzantine Model Checker. http://forsyte.at/software/bymc/, last visit: July 17 (2018)
[37] Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. In: Proceedings of CONCUR, LNCS, pp. 125-140 (2014) · Zbl 1417.68136
[38] Konnov, I.V., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Perspectives of System Informatics—10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers, pp. 6-21 (2015) · Zbl 1461.68115
[39] Konnov, IV; Veith, H.; Widder, J., On the completeness of bounded model checking for threshold-based distributed algorithms: reachability, Inf. Comput., 252, 95-109 (2017) · Zbl 1355.68176
[40] Koopmann, P., Rudolph, S., Schmidt, R.A., Wernhard, C. (eds.): Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, December 6-8, 2017, volume 2013 of CEUR Workshop Proceedings. CEUR-WS.org (2017)
[41] Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: Automated Deduction—CADE-22. In: 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, pp. 199-213 (2009) · Zbl 1250.68193
[42] Kuncak, V.; Nguyen, HH; Rinard, M., Deciding boolean algebra with Presburger arithmetic, J. Autom. Reas., 36, 3, 213-239 (2006) · Zbl 1112.03011
[43] Kuncak, V., Nguyen, H.H., Rinard, M.: An Algorithm for deciding BAPA: boolean algebra with Presburger arithmetic. In: Proceedings of CADE-20, volume 3632 of LNCS (July 2005) · Zbl 1102.03303
[44] Lambek, J., Scott, P.J.: Introduction to higher order categorical logic, volume 7 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1988. Reprint of the 1986 original · Zbl 0596.03002
[45] Lynch, NA, Distributed Algorithms (1996), Burlington: Morgan Kaufmann, Burlington · Zbl 0877.68061
[46] Maric, O., Sprenger, C., Basin, D.A.: Cutoff bounds for consensus algorithms. In: Computer Aided Verification—29th International Conference, CAV 2017, Heidelberg, July 24-28, 2017, Proceedings, Part II, pp. 217-237 (2017)
[47] Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of the ISCA (1984). https://dl.acm.org/citation.cfm?id=808204
[48] Pease, M.; Shostak, R.; Lamport, L., Reaching agreement in the presence of faults, JACM, 27, 2, 228-234 (1980) · Zbl 0434.68031
[49] Presburger, M., Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt (1929), Warszawa: Kluwer, Warszawa · JFM 56.0825.04
[50] Raynal, M.: Fault-tolerant Agreement in Synchronous Message-Passing Systems. Morgan & Claypool—Synthesis Lectures on Distributed Computing Theory series (2010)
[51] Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Proceedings of the CAV, pp. 198-216 (2015) · Zbl 1381.68059
[52] Schweikhart, N.: Arithmetic, first-order logic, and counting quantifiers. In: ACM TOCL, pp. 1-35 (2004)
[53] Solihin, Y., Fundamentals of Parallel Computer Architecture Multichip and Multicore Systems (2008), Raleigh: Solihin Publishing & Consulting LLC, Raleigh
[54] Srikanth, TK; Toueg, S., Optimal clock synchronization, JACM, 34, 3, 626-645 (1987)
[55] Srikanth, TK; Toueg, S., Simulating authenticated broadcasts to derive simple fault-tolerant algorithms, Distrib. Comput., 2, 2, 80-94 (1987)
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.