Top

Published in:

2016 | OriginalPaper | Chapter

Finite Model Finding Using the Logic of Equality with Uninterpreted Functions

Authors : Amirhossein Vakili, Nancy A. Day

Published in: FM 2016: Formal Methods

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The problem of finite model finding, finding a satisfying model for a set of first-order logic formulas for a finite scope, is an important step in many verification techniques. In MACE-style solvers, the problem is mapped directly to a SAT problem. We investigate an alternative solution of mapping the problem to the logic of equality with uninterpreted functions (EUF), a decidable logic with many well-supported tools (e.g., SMT solvers). EUF reasoners take advantage of the typed functional structures found in the formulas to improve performance. The challenge is that EUF reasoning is not inherently finite scope. We present an algorithm for mapping a finite model finding problem to an equisatisfiable EUF problem. We present results that show our method has better overall performance than existing tools on a range of problems.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Automated Mutual Explicit Induction Proof in Separation Logic

next chapter GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking

Available at: rebrand.ly/fortress.

We use “type” and “sort” interchangeably in this paper.

In SMT-LIB, this constraint is written simply as: \(\texttt {(distinct}\ a_1\ a_2\ a_3\texttt {)}\).

Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Publishing Company, Amsterdam (1954)MATH

Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14 CrossRef

Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015)

Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories, Frontiers. In: Artificial Intelligence and Applications, vol. 185, chap. 26, pp. 825–885. IOS Press, Amsterdam (2009)

Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1), 58–74 (2009)MathSciNetCrossRefMATH

Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_11 CrossRef

Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_7 CrossRef

Claessen, K., Sörensson, N.: New techniques that improve mace-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)

El Ghazi, A.A., Taghdiri, M.: Analyzing Alloy constraints using an SMT solver: a case study. In: International Workshop on Automated Formal Methods (2010)

10.

Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, New York (1990)CrossRefMATH

11.

Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press, Cambridge (2012)

12.

Khurshid, S., Marinov, D.: TestEra: specification-based testing of Java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)CrossRef

13.

Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008)MATH

14.

McCune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problem. Technical report, Argonne National Laboratory (1994)

15.

McCune, W.: Prover9 and Mace4 (2005–2010). http://www.cs.unm.edu/~mccune/prover9

16.

McCune, W.: Mace4 reference manual and guide. CoRR cs.SC/0310055 (2003)

17.

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 CrossRef

18.

Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_42 CrossRef

19.

Samimi, H.: Schfer, M., Artzi, S., Millstein, T., Tip, F., Hendren, L: Automated repair of HTML generation errors in PHP applications using string constraint solving. In: International Conference on Software Engineering (ICSE), pp. 277–287 (2012)

20.

Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)MathSciNetCrossRefMATH

21.

Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Autom. Softw. Eng. 14(1), 87–121 (2007)CrossRef

22.

Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_49 CrossRef

23.

Vakili, A., Day, N.A.: Temporal logic model checking in alloy. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 150–163. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30885-7_11 CrossRef

24.

Zhang, H., Zhang, J.: MACE4 and SEM: a comparison of finite model generators. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 101–130. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36675-8_5 CrossRef

25.

Zhang, J., Zhang, H.: Sem: A system for enumerating models. In: International Joint Conference on Artificial Intelligence (IJCAI)

Title: Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Authors: Amirhossein Vakili
Nancy A. Day
Publisher: Springer International Publishing
Book: FM 2016: Formal Methods
Print ISBN: 978-3-319-48988-9

Electronic ISBN: 978-3-319-48989-6

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-48989-6_41

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner