Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Industrial-Strength Model-Based Testing of Safety-Critical Systems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Finite Model Finding Using the Logic of Equality with Uninterpreted Functions

verfasst von : Amirhossein Vakili, Nancy A. Day

Erschienen in: FM 2016: Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Automated Mutual Explicit Induction Proof in Separation Logic
Nächstes Kapitel GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Fußnoten
2
We use “type” and “sort” interchangeably in this paper.
 
3
In SMT-LIB, this constraint is written simply as: \(\texttt {(distinct}\ a_1\ a_2\ a_3\texttt {)}\).
 
Literatur
1.
Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Publishing Company, Amsterdam (1954)MATH
2.
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
3.
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015)
4.
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)
5.
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
6.
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
7.
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
8.
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)
9.
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.
16.
McCune, W.: Mace4 reference manual and guide. CoRR cs.SC/0310055 (2003)
17.
18.
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.
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)
Metadaten
Titel
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
verfasst von
Amirhossein Vakili
Nancy A. Day
Copyright-Jahr
2016
Buch
FM 2016: Formal Methods

Print ISBN: 978-3-319-48988-9

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

Copyright-Jahr: 2016

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