Montenegro Montes, ManuelNieva Soto, SusanaPeña Marí, Ricardo VicenteSegura Díaz, Clara María2023-06-172023-06-172020-01-211529-378510.1145/3362740https://hdl.handle.net/20.500.14352/7066A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, since programmers can use them to specify pre- and postconditions of their programs, while the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, since the logical predicates within liquid types are constrained to a quantifier-free logic in order to maintain decidability. In this paper we extend liquid types by allowing them to contain quantified properties on arrays, so that they can be used to infer invariants on array-related programs (for example, implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations.engjournal articlehttps://dl.acm.org/doi/10.1145/3362740open accessDependent TypesLiquid TypesInvariant SynthesisTipos dependientesTipos LiquidSíntesis de InvariantesLenguajes de programaciónProgramación de ordenadores (Informática)SoftwareLógica simbólica y matemática (Matemáticas)1203.23 Lenguajes de Programación1203.23 Lenguajes de Programación3304.16 Diseño Lógico1102.14 Lógica Simbólica