Exploració per autor "Larraz Hurtado, Daniel"Més informació

Ara es mostren els items 1-9 de 9

    • Automatic generation of loop invariants 

      Larraz Hurtado, Daniel (Universitat Politècnica de Catalunya, 2011-06)
      Projecte Final de Màster Oficial
      Accés obert
      CppInv works in two stages. Firstly, it parses a source code written in a subset of C++ and abstracts all execution paths of the program building a control flow graph associated to a transition system. Paths are expressed ...

    • Automatic program analysis using Max-SMT 

      Larraz Hurtado, Daniel (Universitat Politècnica de Catalunya, 2015-07-28)
      Tesi
      Accés obert
      This thesis addresses the development of techniques to build fully-automatic tools for analyzing sequential programs written in imperative languages like C or C++. In order to do the reasoning about programs, the approach ...

    • Compositional safety verification with Max-SMT 

      Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2015)
      Text en actes de congrés
      Accés obert
      We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop) and a postcondition, we show how to, using ...

    • Incomplete SMT techniques for solving non-linear formulas over the integers 

      Borralleras Andreu, Cristina; Larraz Hurtado, Daniel; Rodríguez Carbonell, Enric; Oliveras Llunell, Albert; Rubio Gimeno, Alberto (2019-08-01)
      Article
      Accés obert
      We present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas ...

    • Minimal-model-guided approaches to solving polynomial constraints and extensions 

      Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2014)
      Text en actes de congrés
      Accés obert
      In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear ...

    • Proving non-termination using max-SMT 

      Larraz Hurtado, Daniel; Nimkar, Kaustubh; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2014)
      Text en actes de congrés
      Accés obert
      We show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants - properties such ...

    • Proving termination of imperative programs using Max-SMT 

      Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2013)
      Text en actes de congrés
      Accés obert
      We show how Max-SMT can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different ...

    • Proving termination through conditional termination 

      Borralleras Andreu, Cristina; Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2017)
      Text en actes de congrés
      Accés obert
      We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine ...

    • Speeding up the constraint-based method in difference logic 

      Candeago, L.; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2016)
      Text en actes de congrés
      Accés obert
      Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of ...