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)
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)
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)
[+]
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)
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)
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)
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)
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)
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)
Barwise, J.: An Introduction to First-Order Logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977)
Barwise, J.: Axioms for Abstract Model Theory. Ann. Math. Log. 7, 221–265 (1974)
Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. Springer, Berlin (1998)
Birkhoff, G., Lipson, J.D.: Heterogeneous algebras. J. Comb. Theory 8, 115–133 (1970)
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)
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)
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)
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)
Bliss, G.A.: Algebraic Functions. Dover (2004)
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)
Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)
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)
Bürckert, H.-J., Hollunder, B., Laux, A.: On Skolemization in constrained logics. Ann. Math. Artif. Intell. 18, 95–131 (1996)
Burstall, R.M., Goguen, J.A.: Putting Theories together to make specifications. In: Proceedings of IJCAI’77, pp. 1045–1058. William Kaufmann (1977)
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)
Chang, C.L., Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Orlando (1973)
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)
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)
Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2006)
Cooper, D.C.: Programs for mechanical program verification. Mach. Intell. 6, 43–59 (1971). Edinburgh University Press
Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91–99 (1972)
Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretations. In: Proceedings of SOFSEM’10. LNCS, vol. 5901, pp. 283–295 (2010)
Cousot, P., Cousot, R., Mauborgne, L.: Logical abstract domains and interpretations. In: The Future of Sofware Engineering, pp. 48–71. Springer, New York (2011)
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)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
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)
van Emdem, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733–742 (1976)
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)
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008)
Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–32 (1967)
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)
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)
Fuhs, C., Kop, C.: Polynomial interpretations for higher-order rewriting. In: Proceedings of RTA’12. LIPIcs, vol. 15, pp. 176–192 (2012)
Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series, (1998)
Gaboardi, M., Péchoux, R.: On bounding space usage of streams using interpretation analysis. Sci. Comput. Program. 111, 395–425 (2015)
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)
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)
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)
Gnaedig, I.: Termination of Order-sorted Rewriting. In: Proceedings of ALP’92. LNCS, vol. 632, pp. 37–52 (1992)
Goguen, J.A.: Order-Sorted Algebra. Semantics and Theory of Computation Report 14, UCLA (1978)
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)
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)
Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87. LNCS, vol. 250, pp. 1–22 (1987)
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)
Goguen, J.A., Meseguer, J.: Remarks on remarks on many-sorted equational logic. Sigplan Notices 22(4), 41–48 (1987)
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)
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)
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)
Gulwani, S., Tiwari, A.: Combining Abstract Interpreters. In: Proceedings of PLDI’06, pp. 376–386. ACM Press (2006)
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)
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/
Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv. 8(3), 331–353 (1976)
Hayes, P.: A logic of actions. Mach. Intell. 6, 495–520 (1971). Edinburgh University Press, Edinburgh
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)
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)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–583 (1969)
Hodges, W.: Elementary Predicate Logic. Handbook of Philosophical Logic, vol. 1, pp. 1–131. Reidel Publishing Company (1983)
Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge (1997)
Hofbauer, D.: Termination proofs by context-dependent interpretation. In: Proceedings of RTA’01. LNCS, vol. 2051, pp. 108–121 (2001)
Hofbauer, D.: Termination proofs for ground rewrite systems. interpretations and derivational complexity. Appl. Algebra Eng. Commun. Comput. 12, 21–38 (2001)
Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proceedings of RTA’89. LNCS, vol. 355, pp. 167–177 (1989)
Hull, T.E., Enright, W.H., Sedgwick, A.E.: The correctness of numerical algorithms. In: Proceedings of PAAP’72, pp. 66–73 (1972)
Igarashi, S., London, R.L., Luckham, D.: Automatic program verification I: a logical basis and its implementation. Acta Inform. 4, 145–182 (1975)
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)
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)
Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188–206 (1976)
Langford, C.H.: Review: Über deduktive Theorien mit mehreren Sorten von Grunddingen. J. Symb. Log. 4(2), 98 (1939)
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
London, R.L.: The current state of proving programs correct. In: Proceedings of ACM’72, vol. 1, pp. 39–46. ACM (1972)
Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Inform. Appl. 39(3), 547–586 (2005)
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)
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)
Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inform. Proces. Lett. 95, 446–453 (2005)
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)
Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proceedings of PPDP’08 , pp. 108–119. ACM Press (2008)
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)
Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017)
Manna, Z.: The correctness of programs. J. Comput. Syst. Sci. 3, 119–127 (1969)
Manna, Z.: Properties of programs and the first-order predicate calculus. J. ACM 16(2), 244–255 (1969)
Manna, Z.: Termination of programs represented as interpreted graphs. In: Proceedings of AFIPS’70, pp. 83–89 (1970)
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)
Manna, Z., Pnueli, A.: Formalization of properties of functional programs. J. ACM 17(3), 555–569 (1970)
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)
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)
McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine. Part I. Commun. ACM 3(4), 184–195 (1960)
Meseguer, J.: General logics. In: Ebbinghaus, H.D., et al. (eds.) Logic Colloquium’87, pp. 275–329. North-Holland (1989)
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)
Middeldorp, A.: Matrix interpretations for polynomial derivational complexity of rewrite systems. In: Proceedings of LPAR’12. LNCS, vol. 7180, p. 12 (2012)
Monin, J.-F.: Understanding Formal Methods. Springer, London (2003)
Montenegro, M., Peña, R., Segura, C.: Space consumption analysis by abstract interpretation: inference of recursive functions. Sci. Comput. Program. 111, 426–457 (2015)
de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
Naur, P.: Proof of algorithms by general snapshots. Bit 6, 310–316 (1966)
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)
Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002)
Ölveczky, P.C., Lysne, O.: Order-sorted termination: the unsorted way. In: Proceedings of ALP’96. LNCS, vol. 1139, pp. 92–106 (1996)
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)
Péchoux, R.: Synthesis of sup-interpretations: a survey. Theoret. Comput. Sci. 467, 30–52 (2013)
Podelski, A., Rybalchenko, A.: Transition invariants. In: IEEE Computer Society Proceedings of LICS’04, pp. 32–41 (2004)
Prestel, A., Delzell, C.N.: Positive Polynomials. From Hilbert’s 17th Problem to Real Algebra. Springer, Berlin (2001)
Robinson, D.J.S.: A Course in Linear Algebra with Applications, 2nd edn. World Scientific Publishing, Co, Singapore (2006)
Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Proceedings of CAV’13, vol. 8044, pp. 347–363 (2013)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Amsterdam (1986)
Schmidt, A.: Über deduktive Theorien mit mehreren Sorten von Grunddingen. Matematische Annalen 115(4), 485–506 (1938)
Schmidt-Schauss, M.: Computational Aspects Of An Order-Sorted Logic With Term Declarations. PhD Thesis, Fachbereich Informatik der Universität Kaiserslautern (1988)
Shapiro, S.: Foundations without Foundationalism: A Case for Second-Order Logic. Clarendon Press, New York (1991)
Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979)
Smullyan, R.M.: Theory of Formal Systems. Princeton University Press, Princeton (1961)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)
Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inform. Process. Lett. 25, 141–143 (1987)
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)
Urban, C.: The abstract domain of segmented ranking functions. In: Proceeding of SAS’13. LNCS, vol. 7935, pp. 43–62 (2013)
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)
Waldmann, J.: Matrix interpretations on polyhedral domains. In: Proceedings of RTA’15. LIPICS, vol. 26, pp. 318–333 (2015)
Waldmann, J., Bau, A., Noeth, E.: Matchbox termination prover. http://github.com/jwaldmann/matchbox/ (2014)
Walther, C.: A mechanical solution of schubert’s steamroller by many-sorted resolution. Aritif. Intell. 26, 217–224 (1985)
Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105–116 (1952)
Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17, 23–50 (1994)
[-]
![[Cerrado]](/themes/UPV/images/candado.png)
