- -

Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Lucas;Gutiérrez - ...
Tamaño: 630.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: LucGut_AutomaticS ...
Tamaño: 1016.Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Lucas Alba, Salvador es_ES
dc.contributor.author Gutiérrez Gil, Raúl es_ES
dc.date.accessioned 2019-07-25T20:01:39Z
dc.date.available 2019-07-25T20:01:39Z
dc.date.issued 2018 es_ES
dc.identifier.issn 0168-7433 es_ES
dc.identifier.uri http://hdl.handle.net/10251/124228
dc.description.abstract [EN] In program analysis, the synthesis of models of logical theories representing the program semantics is often useful to prove program properties. We use order-sorted first- order logic as an appropriate framework to describe the semantics and properties of programs as given theories. Then we investigate the automatic synthesis of models for such theories. We use convex polytopic domains as a flexible approach to associate different domains to different sorts. We introduce a framework for the piecewise definition of functions and predicates. We develop its use with linear expressions (in a wide sense, including linear transformations represented as matrices) and inequalities to specify functions and predicates. In this way, algorithms and tools from linear algebra and arithmetic constraint solving (e.g., SMT) can be used as a backend for an efficient implementation. es_ES
dc.description.sponsorship Partially supported by the EU (FEDER), projects TIN2015-69175-C4-1-R, and GV PROMETEOII/2015/ 013. R. Gutiérrez also supported by Juan de la Cierva Fellowship JCI-2012-13528.
dc.language Inglés es_ES
dc.publisher Springer-Verlag es_ES
dc.relation.ispartof Journal of Automated Reasoning es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Logical models es_ES
dc.subject Order-sorted first-order logic es_ES
dc.subject Program analysis es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s10817-017-9419-3 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//JCI-2012-13528/ES/JCI-2012-13528/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Lucas Alba, S.; Gutiérrez Gil, R. (2018). Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories. Journal of Automated Reasoning. 60(4):465-501. https://doi.org/10.1007/s10817-017-9419-3 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion http://doi.org/10.1007/s10817-017-9419-3 es_ES
dc.description.upvformatpinicio 465 es_ES
dc.description.upvformatpfin 501 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 60 es_ES
dc.description.issue 4 es_ES
dc.relation.pasarela S\341589 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Ministerio de Economía y Empresa es_ES
dc.description.references Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10. LNCS, vol. 6486, pp. 201–208 (2011) es_ES
dc.description.references Alarcón, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Proceedings of PROLE’09, pp. 255–264 (2009) es_ES
dc.description.references Albert, E., Genaim, S., Gutiérrez, R.: A Transformational Approach to Resource Analysis with Typed-Norms. Revised Selected Papers from LOPSTR’13. LNCS, vol. 8901, pp 38–53 (2013) es_ES
dc.description.references de Angelis, E., Fioravante, F., Pettorossi, A., Proietti, M.: Proving correctness of imperative programs by linearizing constrained Horn clauses. Theory Pract. Log. Program. 15(4–5), 635–650 (2015) es_ES
dc.description.references de Angelis, E., Fioravante, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions by program specialization. In: Proceedings of PPDP’15, pp. 91–102. ACM Press, New York (2015) es_ES
dc.description.references Aoto, T.: Solution to the problem of zantema on a persistent property of term rewriting systems. J. Funct. Log. Program. 2001(11), 1–20 (2001) es_ES
dc.description.references Barwise, J.: An Introduction to First-Order Logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977) es_ES
dc.description.references Barwise, J.: Axioms for Abstract Model Theory. Ann. Math. Log. 7, 221–265 (1974) es_ES
dc.description.references Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. Springer, Berlin (1998) es_ES
dc.description.references Birkhoff, G., Lipson, J.D.: Heterogeneous algebras. J. Comb. Theory 8, 115–133 (1970) es_ES
dc.description.references Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Proceedings of CAV’08. LNCS, vol. 5123, pp. 294–298 (2008) es_ES
dc.description.references Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn-clause solvers for program verification. In: Fields of Logic and Computation II—Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. LNCS, vol. 9300, pp. 24–51 (2015) es_ES
dc.description.references Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn-clauses. In: Proceedings of SAS’13. LNCS vol. 7935, pp. 105–125 (2013) es_ES
dc.description.references Bjørner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Proceedings of SMT’12, EPiC Series in Computing, vol. 20, pp. 3–11 (2013) es_ES
dc.description.references Bliss, G.A.: Algebraic Functions. Dover (2004) es_ES
dc.description.references Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: On Lexicographic Termination Ordering With Space Bound Certifications. Revised Papers from PSI 2001. LNCS, vol. 2244, pp. 482–493 (2001) es_ES
dc.description.references Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002) es_ES
dc.description.references Borralleras, C., Lucas, S., Oliveras, A., Rodríguez, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. J. Autom. Reason. 48, 107–131 (2012) es_ES
dc.description.references Bürckert, H.-J., Hollunder, B., Laux, A.: On Skolemization in constrained logics. Ann. Math. Artif. Intell. 18, 95–131 (1996) es_ES
dc.description.references Burstall, R.M., Goguen, J.A.: Putting Theories together to make specifications. In: Proceedings of IJCAI’77, pp. 1045–1058. William Kaufmann (1977) es_ES
dc.description.references Caplain, M.: Finding invariant assertions for proving programs. In: Proceedings of the International Conference on Reliable Software, pp. 165–171. ACM Press, New York (1975) es_ES
dc.description.references Chang, C.L., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Orlando (1973) es_ES
dc.description.references Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude—A High-Performance Logical Framework. LNCS 4350, (2007) es_ES
dc.description.references Cohn, A.G.: Improving the expressiveness of many sorted logic. In: Proceedings of the National Conference on Artificial Intelligence, pp. 84–87. AAAI Press, Menlo Park (1983) es_ES
dc.description.references Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2006) es_ES
dc.description.references Cooper, D.C.: Programs for mechanical program verification. Mach. Intell. 6, 43–59 (1971). Edinburgh University Press es_ES
dc.description.references Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91–99 (1972) es_ES
dc.description.references Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretations. In: Proceedings of SOFSEM’10. LNCS, vol. 5901, pp. 283–295 (2010) es_ES
dc.description.references Cousot, P., Cousot, R., Mauborgne, L.: Logical abstract domains and interpretations. In: The Future of Sofware Engineering, pp. 48–71. Springer, New York (2011) es_ES
dc.description.references Cousot, P., Halbwachs, N.: Automatic Discovery of linear restraints among variables of a program. In: Conference Record of POPL’78, pp. 84–96. ACM Press, New York (1978) es_ES
dc.description.references Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990) es_ES
dc.description.references Elspas, B., Levitt, K.N., Waldinger, R.J., Waksman, A.: An assessment of techniques for proving program correctness. Comput. Surv. 4(2), 97–147 (1972) es_ES
dc.description.references van Emdem, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733–742 (1976) es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Proceedings of IJCAR’06. LNCS, vol. 4130, pp. 574–588 (2006) es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008) es_ES
dc.description.references Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–32 (1967) es_ES
dc.description.references Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Proceedings of RTA’08. LNCS, vol. 5117, pp. 110–125 (2008) es_ES
dc.description.references Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving termination by dependency pairs and inductive theorem proving. J. Autom. Reason. 47, 133–160 (2011) es_ES
dc.description.references Fuhs, C., Kop, C.: Polynomial interpretations for higher-order rewriting. In: Proceedings of RTA’12. LIPIcs, vol. 15, pp. 176–192 (2012) es_ES
dc.description.references Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series, (1998) es_ES
dc.description.references Gaboardi, M., Péchoux, R.: On bounding space usage of streams using interpretation analysis. Sci. Comput. Program. 111, 395–425 (2015) es_ES
dc.description.references Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Proceedings of CADE’15. LNCS, vol. 9195, pp. 105–108 (2015) es_ES
dc.description.references Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting—a general methodology for analyzing logic programs. In: Proceedings of the PPDP’12, pp. 1–12. ACM Press (2012) es_ES
dc.description.references Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7 (2011) es_ES
dc.description.references Gnaedig, I.: Termination of Order-sorted Rewriting. In: Proceedings of ALP’92. LNCS, vol. 632, pp. 37–52 (1992) es_ES
dc.description.references Goguen, J.A.: Order-Sorted Algebra. Semantics and Theory of Computation Report 14, UCLA (1978) es_ES
dc.description.references Goguen, J.A., Burstall, R.M.: Some fundamental algebraic tools for the semantics of computation. Part 1: comma categories, colimits, signatures and theories. Theoret. Comput. Sci. 31, 175–209 (1984) es_ES
dc.description.references Goguen, J.A., Burstall, R.M.: Some fundamental algebraic tools for the semantics of computation. Part 2 signed and abstract theories. Theoret. Comput. Sci. 31, 263–295 (1984) es_ES
dc.description.references Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87. LNCS, vol. 250, pp. 1–22 (1987) es_ES
dc.description.references Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology, pp. 80–149. Prentice Hall (1978) es_ES
dc.description.references Goguen, J.A., Meseguer, J.: Remarks on remarks on many-sorted equational logic. Sigplan Notices 22(4), 41–48 (1987) es_ES
dc.description.references Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 217–273 (1992) es_ES
dc.description.references Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Boston (2000) es_ES
dc.description.references Grebenshikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI’12, pp. 405–416. ACM Press (2012) es_ES
dc.description.references Gulwani, S., Tiwari, A.: Combining Abstract Interpreters. In: Proceedings of PLDI’06, pp. 376–386. ACM Press (2006) es_ES
dc.description.references Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Proceedings of CAV’15, Part I. LNCS, vol. 9206, pp. 343–361 (2015) es_ES
dc.description.references Gutiérrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE’16, pp. 215–230 (2016). http://zenon.dsic.upv.es/ages/ es_ES
dc.description.references Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv. 8(3), 331–353 (1976) es_ES
dc.description.references Hayes, P.: A logic of actions. Mach. Intell. 6, 495–520 (1971). Edinburgh University Press, Edinburgh es_ES
dc.description.references Heidergott, B., Olsder, G.J., van der Woude, J.: Max plus at work. A course on max-plus algebra and its applications. In: Modeling and Analysis of Synchronized Systems, Princeton University Press (2006) es_ES
dc.description.references Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proceedings of IJCAR 2008. LNCS, vol. 5195, pp. 364–379 (2008) es_ES
dc.description.references Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–583 (1969) es_ES
dc.description.references Hodges, W.: Elementary Predicate Logic. Handbook of Philosophical Logic, vol. 1, pp. 1–131. Reidel Publishing Company (1983) es_ES
dc.description.references Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997) es_ES
dc.description.references Hofbauer, D.: Termination proofs by context-dependent interpretation. In: Proceedings of RTA’01. LNCS, vol. 2051, pp. 108–121 (2001) es_ES
dc.description.references Hofbauer, D.: Termination proofs for ground rewrite systems. interpretations and derivational complexity. Appl. Algebra Eng. Commun. Comput. 12, 21–38 (2001) es_ES
dc.description.references Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proceedings of RTA’89. LNCS, vol. 355, pp. 167–177 (1989) es_ES
dc.description.references Hull, T.E., Enright, W.H., Sedgwick, A.E.: The correctness of numerical algorithms. In: Proceedings of PAAP’72, pp. 66–73 (1972) es_ES
dc.description.references Igarashi, S., London, R.L., Luckham, D.: Automatic program verification I: a logical basis and its implementation. Acta Inform. 4, 145–182 (1975) es_ES
dc.description.references Iwami, M.: Persistence of termination of term rewriting systems with ordered sorts. In: Proceedings of 5th JSSST Workshop on Programming and Programming Languages, Shizuoka, Japan, pp. 47–56. (2003) es_ES
dc.description.references Iwami, M.: Persistence of termination for non-overlapping term rewriting systems. In: Proceedings of Algebraic Systems, Formal Languages and Conventional and Unconventional Computation Theory, Kokyuroku RIMS, University of Kyoto, vol. 1366, pp. 91–99 (2004) es_ES
dc.description.references Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188–206 (1976) es_ES
dc.description.references Langford, C.H.: Review: Über deduktive Theorien mit mehreren Sorten von Grunddingen. J. Symb. Log. 4(2), 98 (1939) es_ES
dc.description.references Lankford, D.S.: Some approaches to equality for computational logic: a survey and assessment. Memo ATP-36, Automatic Theorem Proving Project, University of Texas, Austin, TX es_ES
dc.description.references London, R.L.: The current state of proving programs correct. In: Proceedings of ACM’72, vol. 1, pp. 39–46. ACM (1972) es_ES
dc.description.references Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Inform. Appl. 39(3), 547–586 (2005) es_ES
dc.description.references Lucas, S.: Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving. Electron. Proc. Theor. Comput. Sci. 200, 32–47 (2015) es_ES
dc.description.references Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA’16. LNCS, vol. 9942, pp. 1–21 (2016) es_ES
dc.description.references Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inform. Proces. Lett. 95, 446–453 (2005) es_ES
dc.description.references Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC’14. LNAI, vol. 8884, pp. 7–18 (2014) es_ES
dc.description.references Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proceedings of PPDP’08 , pp. 108–119. ACM Press (2008) es_ES
dc.description.references Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP’14, pp. 111–122. ACM Digital Library (2014) es_ES
dc.description.references Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017) es_ES
dc.description.references Manna, Z.: The correctness of programs. J. Comput. Syst. Sci. 3, 119–127 (1969) es_ES
dc.description.references Manna, Z.: Properties of programs and the first-order predicate calculus. J. ACM 16(2), 244–255 (1969) es_ES
dc.description.references Manna, Z.: Termination of programs represented as interpreted graphs. In: Proceedings of AFIPS’70, pp. 83–89 (1970) es_ES
dc.description.references Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, pp. 789–792 (1970) es_ES
dc.description.references Manna, Z., Pnueli, A.: Formalization of properties of functional programs. J. ACM 17(3), 555–569 (1970) es_ES
dc.description.references Marion, Y.-I., Péchoux, R.: Sup-interpretations, a semantic method for static analysis of program resources. ACM Trans. Comput. Log. 10(4), 27 (2009) es_ES
dc.description.references Martí-Oliet, N., Meseguer, J., Palomino, M.: Theoroidal maps as algebraic simulations. Revised Selected Papers from WADT’04. LNCS, vol. 3423, pp. 126–143 (2005) es_ES
dc.description.references McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine. Part I. Commun. ACM 3(4), 184–195 (1960) es_ES
dc.description.references Meseguer, J.: General logics. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium’87, pp. 275–329. North-Holland (1989) es_ES
dc.description.references Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Revised Selected Papers from LOPSTR’15. LNCS, vol. 9527, pp. 36–53 (2015) es_ES
dc.description.references Middeldorp, A.: Matrix interpretations for polynomial derivational complexity of rewrite systems. In: Proceedings of LPAR’12. LNCS, vol. 7180, p. 12 (2012) es_ES
dc.description.references Monin, J.-F.: Understanding Formal Methods. Springer, London (2003) es_ES
dc.description.references Montenegro, M., Peña, R., Segura, C.: Space consumption analysis by abstract interpretation: inference of recursive functions. Sci. Comput. Program. 111, 426–457 (2015) es_ES
dc.description.references de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011) es_ES
dc.description.references Naur, P.: Proof of algorithms by general snapshots. Bit 6, 310–316 (1966) es_ES
dc.description.references Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Proceedings of RTA’11. LIPICS, vol. 10, pp. 251–266 (2011) es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002) es_ES
dc.description.references Ölveczky, P.C., Lysne, O.: Order-sorted termination: the unsorted way. In: Proceedings of ALP’96. LNCS, vol. 1139, pp. 92–106 (1996) es_ES
dc.description.references Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of java bytecode by term rewriting. In: Proceedings of RTA’10. LIPICS, vol. 6, pp. 259–276 (2010) es_ES
dc.description.references Péchoux, R.: Synthesis of sup-interpretations: a survey. Theoret. Comput. Sci. 467, 30–52 (2013) es_ES
dc.description.references Podelski, A., Rybalchenko, A.: Transition invariants. In: IEEE Computer Society Proceedings of LICS’04, pp. 32–41 (2004) es_ES
dc.description.references Prestel, A., Delzell, C.N.: Positive Polynomials. From Hilbert’s 17th Problem to Real Algebra. Springer, Berlin (2001) es_ES
dc.description.references Robinson, D.J.S.: A Course in Linear Algebra with Applications, 2nd edn. World Scientific Publishing, Co, Singapore (2006) es_ES
dc.description.references Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Proceedings of CAV’13, vol. 8044, pp. 347–363 (2013) es_ES
dc.description.references Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Amsterdam (1986) es_ES
dc.description.references Schmidt, A.: Über deduktive Theorien mit mehreren Sorten von Grunddingen. Matematische Annalen 115(4), 485–506 (1938) es_ES
dc.description.references Schmidt-Schauss, M.: Computational Aspects Of An Order-Sorted Logic With Term Declarations. PhD Thesis, Fachbereich Informatik der Universität Kaiserslautern (1988) es_ES
dc.description.references Shapiro, S.: Foundations without Foundationalism: A Case for Second-Order Logic. Clarendon Press, New York (1991) es_ES
dc.description.references Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979) es_ES
dc.description.references Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961) es_ES
dc.description.references Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951) es_ES
dc.description.references Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inform. Process. Lett. 25, 141–143 (1987) es_ES
dc.description.references Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, University Mathematics Laboratory, Cambridge, pp. 67–69 (1949) es_ES
dc.description.references Urban, C.: The abstract domain of segmented ranking functions. In: Proceeding of SAS’13. LNCS, vol. 7935, pp. 43–62 (2013) es_ES
dc.description.references Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Proceedings of TACAS’16. LNCS, vol. 9636, pp. 54–70 (2016) es_ES
dc.description.references Waldmann, J.: Matrix interpretations on polyhedral domains. In: Proceedings of RTA’15. LIPICS, vol. 26, pp. 318–333 (2015) es_ES
dc.description.references Waldmann, J., Bau, A., Noeth, E.: Matchbox termination prover. http://github.com/jwaldmann/matchbox/ (2014) es_ES
dc.description.references Walther, C.: A mechanical solution of schubert’s steamroller by many-sorted resolution. Aritif. Intell. 26, 217–224 (1985) es_ES
dc.description.references Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105–116 (1952) es_ES
dc.description.references Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17, 23–50 (1994) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem