Showing 1–22 of 22 results for author: Rubio, A

FootBots: A Transformer-based Architecture for Motion Prediction in Soccer

Authors: Guillem Capellera, Luis Ferraz, Antonio Rubio, Antonio Agudo, Francesc Moreno-Noguer

Abstract: Motion prediction in soccer involves capturing complex dynamics from player and ball interactions. We present FootBots, an encoder-decoder transformer-based architecture addressing motion prediction and conditioned motion prediction through equivariance properties. FootBots captures temporal and social dynamics using set attention blocks and multi-attention block decoder. Our evaluation utilizes t… ▽ More Motion prediction in soccer involves capturing complex dynamics from player and ball interactions. We present FootBots, an encoder-decoder transformer-based architecture addressing motion prediction and conditioned motion prediction through equivariance properties. FootBots captures temporal and social dynamics using set attention blocks and multi-attention block decoder. Our evaluation utilizes two datasets: a real soccer dataset and a tailored synthetic one. Insights from the synthetic dataset highlight the effectiveness of FootBots' social attention mechanism and the significance of conditioned motion prediction. Empirical results on real soccer data demonstrate that FootBots outperforms baselines in motion prediction and excels in conditioned tasks, such as predicting the players based on the ball position, predicting the offensive (defensive) team based on the ball and the defensive (offensive) team, and predicting the ball position based on all players. Our evaluation connects quantitative and qualitative findings. https://youtu.be/9kaEkfzG3L8 △ Less

Submitted 28 June, 2024; originally announced June 2024.

Comments: Published as a conference paper at IEEE ICIP 2024

Modeling glycemia in humans by means of Grammatical Evolution

Authors: J. Ignacio Hidalgo, J. Manuel Colmenar, José L. Risco-Martín, Alfredo Cuesta-Infante, Esther Maqueda, Marta Botella, José Antonio Rubio

Abstract: Diabetes mellitus is a disease that affects to hundreds of millions of people worldwide. Maintaining a good control of the disease is critical to avoid severe long-term complications. In recent years, several artificial pancreas systems have been proposed and developed, which are increasingly advanced. However there is still a lot of research to do. One of the main problems that arises in the (sem… ▽ More Diabetes mellitus is a disease that affects to hundreds of millions of people worldwide. Maintaining a good control of the disease is critical to avoid severe long-term complications. In recent years, several artificial pancreas systems have been proposed and developed, which are increasingly advanced. However there is still a lot of research to do. One of the main problems that arises in the (semi) automatic control of diabetes, is to get a model explaining how glycemia (glucose levels in blood) varies with insulin, food intakes and other factors, fitting the characteristics of each individual or patient. This paper proposes the application of evolutionary computation techniques to obtain customized models of patients, unlike most of previous approaches which obtain averaged models. The proposal is based on a kind of genetic programming based on grammars known as Grammatical Evolution (GE). The proposal has been tested with in-silico patient data and results are clearly positive. We present also a study of four different grammars and five objective functions. In the test phase the models characterized the glucose with a mean percentage average error of 13.69\%, modeling well also both hyper and hypoglycemic situations. △ Less

Submitted 27 April, 2023; originally announced May 2023.

Journal ref: Applied Soft Computing, 20, pp. 40-53, 2014

An Automotive Case Study on the Limits of Approximation for Object Detection

Authors: Martí Caro, Hamid Tabani, Jaume Abella, Francesc Moll, Enric Morancho, Ramon Canal, Josep Altet, Antonio Calomarde, Francisco J. Cazorla, Antonio Rubio, Pau Fontova, Jordi Fornt

Abstract: The accuracy of camera-based object detection (CBOD) built upon deep learning is often evaluated against the real objects in frames only. However, such simplistic evaluation ignores the fact that many unimportant objects are small, distant, or background, and hence, their misdetections have less impact than those for closer, larger, and foreground objects in domains such as autonomous driving. Mor… ▽ More The accuracy of camera-based object detection (CBOD) built upon deep learning is often evaluated against the real objects in frames only. However, such simplistic evaluation ignores the fact that many unimportant objects are small, distant, or background, and hence, their misdetections have less impact than those for closer, larger, and foreground objects in domains such as autonomous driving. Moreover, sporadic misdetections are irrelevant since confidence on detections is typically averaged across consecutive frames, and detection devices (e.g. cameras, LiDARs) are often redundant, thus providing fault tolerance. This paper exploits such intrinsic fault tolerance of the CBOD process, and assesses in an automotive case study to what extent CBOD can tolerate approximation coming from multiple sources such as lower precision arithmetic, approximate arithmetic units, and even random faults due to, for instance, low voltage operation. We show that the accuracy impact of those sources of approximation is within 1% of the baseline even when considering the three approximate domains simultaneously, and hence, multiple sources of approximation can be exploited to build highly efficient accelerators for CBOD in cars. △ Less

Submitted 13 April, 2023; originally announced April 2023.

Journal ref: Journal of Systems Architecture, Volume 138, 2023, 102872, ISSN 1383-7621

Quantum Embedding Method for the Simulation of Strongly Correlated Systems on Quantum Computers

Authors: Max Rossmannek, Fabijan Pavošević, Angel Rubio, Ivano Tavernelli

Abstract: Quantum computing has emerged as a promising platform for simulating strongly correlated systems in chemistry, for which the standard quantum chemistry methods are either qualitatively inaccurate or too expensive. However, due to the hardware limitations of the available noisy near-term quantum devices, their application is currently limited only to small chemical systems. One way for extending th… ▽ More Quantum computing has emerged as a promising platform for simulating strongly correlated systems in chemistry, for which the standard quantum chemistry methods are either qualitatively inaccurate or too expensive. However, due to the hardware limitations of the available noisy near-term quantum devices, their application is currently limited only to small chemical systems. One way for extending the range of applicability can be achieved within the quantum embedding approach. Herein, we employ the projection-based embedding method for combining the variational quantum eigensolver (VQE) algorithm, although not limited to, with density functional theory (DFT). The developed VQE-in-DFT method is then implemented efficiently on a real quantum device and employed for simulating the triple bond breaking process in butyronitrile. The results presented herein show that the developed method is a promising approach for simulating systems with a strongly correlated fragment on a quantum computer. The developments as well as the accompanying implementation will benefit many different chemical areas including the computer aided drug design as well as the study of metalloenzymes with a strongly correlated fragment. △ Less

Submitted 6 February, 2023; originally announced February 2023.

Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version)

Authors: Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio

Abstract: Efficiency is a fundamental property of any type of program, but it is even more so in the context of the programs executing on the blockchain (known as smart contracts). This is because optimizing smart contracts has direct consequences on reducing the costs of deploying and executing the contracts, as there are fees to pay related to their bytes-size and to their resource consumption (called gas… ▽ More Efficiency is a fundamental property of any type of program, but it is even more so in the context of the programs executing on the blockchain (known as smart contracts). This is because optimizing smart contracts has direct consequences on reducing the costs of deploying and executing the contracts, as there are fees to pay related to their bytes-size and to their resource consumption (called gas). Optimizing memory usage is considered a challenging problem that, among other things, requires a precise inference of the memory locations being accessed. This is also the case for the Ethereum Virtual Machine (EVM) bytecode generated by the most-widely used compiler, \texttt{solc}, whose rather unconventional and low-level memory usage challenges automated reasoning. This paper presents a static analysis, developed at the level of the EVM bytecode generated by \texttt{solc}, that infers write memory accesses that are needless and thus can be safely removed. The application of our implementation on more than 19,000 real smart contracts has detected about 6,200 needless write accesses in less than 4 hours. Interestingly, many of these writes were involved in memory usage patterns generated by \texttt{solc} that can be greatly optimized by removing entire blocks of bytecodes. To the best of our knowledge, existing optimization tools cannot infer such needless write accesses, and hence cannot detect these inefficiencies that affect both the deployment and the execution costs of Ethereum smart contracts. △ Less

Submitted 11 January, 2023; originally announced January 2023.

Probabilistic Resistive Switching Device modeling based on Markov Jump processes

Authors: Vasileios Ntinas, Antonio Rubio, Georgios Ch. Sirakoulis

Abstract: In this work, a versatile mathematical framework for multi-state probabilistic modeling of Resistive Switching (RS) devices is proposed for the first time. The mathematical formulation of memristor and Markov jump processes are combined and, by using the notion of master equations for finite-states, the inherent probabilistic time-evolution of RS devices is sufficiently modeled. In particular, the… ▽ More In this work, a versatile mathematical framework for multi-state probabilistic modeling of Resistive Switching (RS) devices is proposed for the first time. The mathematical formulation of memristor and Markov jump processes are combined and, by using the notion of master equations for finite-states, the inherent probabilistic time-evolution of RS devices is sufficiently modeled. In particular, the methodology is generic enough and can be applied for $N$ states; as a proof of concept, the proposed framework is further stressed for both two-state RS paradigm, namely $N=2$, and multi-state devices, namely $N=4$. The presented I-V results demonstrate in a qualitative and quantitative manner, adequate matching with other modeling approaches. △ Less

Submitted 14 September, 2020; originally announced September 2020.

Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers

Authors: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio

Abstract: We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists in deciding the satisfiability of ground formulas with integer polynomial constraints. Following previous work, we propose to solve SMT(QF-NIA) instances by reducing them to linear arithmetic: non-linear monomials are linearized… ▽ More We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists in deciding the satisfiability of ground formulas with integer polynomial constraints. Following previous work, we propose to solve SMT(QF-NIA) instances by reducing them to linear arithmetic: non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. For variables that do not have a finite domain, we can artificially introduce one by imposing a lower and an upper bound, and iteratively enlarge it until a solution is found (or the procedure times out). The key for the success of the approach is to determine, at each iteration, which domains have to be enlarged. Previously, unsatisfiable cores were used to identify the domains to be changed, but no clue was obtained as to how large the new domains should be. Here we explain two novel ways to guide this process by analyzing solutions to optimization problems: (i) to minimize the number of violated artificial domain bounds, solved via a Max-SMT solver, and (ii) to minimize the distance with respect to the artificial domains, solved via an Optimization Modulo Theories (OMT) solver. Using this SMT-based optimization technology allows smoothly extending the method to also solve Max-SMT problems over non-linear integer arithmetic. Finally we leverage the resulting Max-SMT(QF-NIA) techniques to solve $\exists \forall$ formulas in a fragment of quantified non-linear arithmetic that appears commonly in verification and synthesis applications. △ Less

Submitted 31 August, 2020; originally announced August 2020.

Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph

Authors: Elvira Albert, Jesús Correas, Pablo Gordillo, Alejandro Hernández-Cerezo Guillermo Román-Díez, Albert Rubio

Abstract: The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or CLI for .Net programs): the use of the stack for saving the jump addresses instead of having it explicit in the code of the jum** instructions. Static analyzers need the complete control flow graph (CFG) of the EVM pr… ▽ More The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or CLI for .Net programs): the use of the stack for saving the jump addresses instead of having it explicit in the code of the jum** instructions. Static analyzers need the complete control flow graph (CFG) of the EVM program in order to be able to represent all its execution paths. This report addresses the problem of obtaining a precise and complete stack-sensitive CFG by means of a static analysis, cloning the blocks that might be executed using different states of the execution stack. The soundness of the analysis presented is proved. △ Less

Submitted 5 October, 2020; v1 submitted 29 April, 2020; originally announced April 2020.

Actor-Based Model Checking for SDN Networks

Authors: Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva

Abstract: Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behavior of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provide… ▽ More Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behavior of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and distributed software---actor-based modelling. We show how SDN programs can be seamlessly modelled using \emph{actors}, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDN networks is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks. △ Less

Submitted 27 January, 2020; originally announced January 2020.

GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts

Authors: Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio

Abstract: We present the main concepts, components, and usage of GASOL, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. GASOL offers a wide variety of cost models that allow inferring the gas consumption associated to selected types of EVM instructions and/or inferring the number of times that such types of bytecode instructions are executed. Among others, we have cost models to measure o… ▽ More We present the main concepts, components, and usage of GASOL, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. GASOL offers a wide variety of cost models that allow inferring the gas consumption associated to selected types of EVM instructions and/or inferring the number of times that such types of bytecode instructions are executed. Among others, we have cost models to measure only storage opcodes, to measure a selected family of gas-consumption opcodes following the Ethereum's classification, to estimate the cost of a selected program line, etc. After choosing the desired cost model and the function of interest, GASOL returns to the user an upper bound of the cost for this function. As the gas consumption is often dominated by the instructions that access the storage, GASOL uses the gas analysis to detect under-optimized storage patterns, and includes an (optional) automatic optimization of the selected function. Our tool can be used within an Eclipse plugin for Solidity which displays the gas and instructions bounds and, when applicable, the gas-optimized Solidity function. △ Less

Submitted 26 December, 2019; originally announced December 2019.

Modelling heterogeneous distributions with an Uncountable Mixture of Asymmetric Laplacians

Authors: Axel Brando, Jose A. Rodríguez-Serrano, Jordi Vitrià, Alberto Rubio

Abstract: In regression tasks, aleatoric uncertainty is commonly addressed by considering a parametric distribution of the output variable, which is based on strong assumptions such as symmetry, unimodality or by supposing a restricted shape. These assumptions are too limited in scenarios where complex shapes, strong skews or multiple modes are present. In this paper, we propose a generic deep learning fram… ▽ More In regression tasks, aleatoric uncertainty is commonly addressed by considering a parametric distribution of the output variable, which is based on strong assumptions such as symmetry, unimodality or by supposing a restricted shape. These assumptions are too limited in scenarios where complex shapes, strong skews or multiple modes are present. In this paper, we propose a generic deep learning framework that learns an Uncountable Mixture of Asymmetric Laplacians (UMAL), which will allow us to estimate heterogeneous distributions of the output variable and shows its connections to quantile regression. Despite having a fixed number of parameters, the model can be interpreted as an infinite mixture of components, which yields a flexible approximation for heterogeneous distributions. Apart from synthetic cases, we apply this model to room price forecasting and to predict financial operations in personal bank accounts. We demonstrate that UMAL produces proper distributions, which allows us to extract richer insights and to sharpen decision-making. △ Less

Submitted 29 October, 2019; v1 submitted 27 October, 2019; originally announced October 2019.

Comments: 12 pages, 4 figures, Paper accepted as poster at the 33rd Conference on Neural Information Processing Systems (NeurIPS 2019), Vancouver, Canada

Resource Analysis driven by (Conditional) Termination Proofs

Authors: Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio

Abstract: When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that t… ▽ More When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools. Under consideration for acceptance in TPLP. △ Less

Submitted 23 July, 2019; originally announced July 2019.

Comments: Paper presented at the 35th International Conference on Logic Programming (ICLP 2019), Las Cruces, New Mexico, USA, 20-25 September 2019, 16 pages

Journal ref: Theory and Practice of Logic Programming 19 (2019) 722-739

SAFEVM: A Safety Verifier for Ethereum Smart Contracts

Authors: Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio

Abstract: Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code,… ▽ More Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax. △ Less

Submitted 12 June, 2019; originally announced June 2019.

An Adversarial Risk Analysis Framework for Cybersecurity

Authors: David Rios Insua, Aitor Couce Vieira, Jose Antonio Rubio, Wolter Pieters, Katsiaryna Labunets, Daniel Garcia Rasines

Abstract: Cyber threats affect all kinds of organisations. Risk analysis is an essential methodology for cybersecurity as it allows organisations to deal with the cyber threats potentially affecting them, prioritise the defence of their assets and decide what security controls should be implemented. Many risk analysis methods are present in cybersecurity models, compliance frameworks and international stand… ▽ More Cyber threats affect all kinds of organisations. Risk analysis is an essential methodology for cybersecurity as it allows organisations to deal with the cyber threats potentially affecting them, prioritise the defence of their assets and decide what security controls should be implemented. Many risk analysis methods are present in cybersecurity models, compliance frameworks and international standards. However, most of them employ risk matrices, which suffer shortcomings that may lead to suboptimal resource allocations. We propose a comprehensive framework for cybersecurity risk analysis, covering the presence of both adversarial and non-intentional threats and the use of insurance as part of the security portfolio. A case study illustrating the proposed framework is presented, serving as template for more complex cases. △ Less

Submitted 18 March, 2019; originally announced March 2019.

Running on Fumes--Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis

Authors: Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey

Abstract: Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised.… ▽ More Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviours. We report on the design and implementation of GASTAP, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers sound gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities. △ Less

Submitted 7 August, 2019; v1 submitted 22 November, 2018; originally announced November 2018.

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode

Authors: Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey

Abstract: Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores the bytecode), (2) the information to be gathered in the analysis is only visible at the level of bytecode (e.g., gas consumption is specified at the level of EVM instructions), (3) the analysis results may be affected by… ▽ More Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores the bytecode), (2) the information to be gathered in the analysis is only visible at the level of bytecode (e.g., gas consumption is specified at the level of EVM instructions), (3) the analysis results may be affected by optimizations performed by the compiler (thus the analysis should be done ideally after compilation). This paper presents EthIR, a framework for analyzing Ethereum bytecode, which relies on (an extension of) OYENTE, a tool that generates CFGs; EthIR produces from the CFGs, a rule-based representation (RBR) of the bytecode that enables the application of (existing) high-level analyses to infer properties of EVM code. △ Less

Submitted 10 May, 2018; originally announced May 2018.

Reinforcement Learning for Fair Dynamic Pricing

Authors: Roberto Maestre, Juan Duque, Alberto Rubio, Juan Arévalo

Abstract: Unfair pricing policies have been shown to be one of the most negative perceptions customers can have concerning pricing, and may result in long-term losses for a company. Despite the fact that dynamic pricing models help companies maximize revenue, fairness and equality should be taken into account in order to avoid unfair price differences between groups of customers. This paper shows how to sol… ▽ More Unfair pricing policies have been shown to be one of the most negative perceptions customers can have concerning pricing, and may result in long-term losses for a company. Despite the fact that dynamic pricing models help companies maximize revenue, fairness and equality should be taken into account in order to avoid unfair price differences between groups of customers. This paper shows how to solve dynamic pricing by using Reinforcement Learning (RL) techniques so that prices are maximized while kee** a balance between revenue and fairness. We demonstrate that RL provides two main features to support fairness in dynamic pricing: on the one hand, RL is able to learn from recent experience, adapting the pricing policy to complex market environments; on the other hand, it provides a trade-off between short and long-term objectives, hence integrating fairness into the model's core. Considering these two features, we propose the application of RL for revenue optimization, with the additional integration of fairness as part of the learning procedure by using Jain's index as a metric. Results in a simulated environment show a significant improvement in fairness while at the same time maintaining optimisation of revenue. △ Less

Submitted 27 March, 2018; originally announced March 2018.

Compositional Safety Verification with Max-SMT

Authors: Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio

Abstract: 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 $\varphi$, we show how to, using a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the i… ▽ More 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 $\varphi$, we show how to, using a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the invariant implies $\varphi$. From this, we build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures to prove the validity of a precondition, using the obtained intermediate results to restrict the search space for further proof attempts. As only small program parts need to be handled at a time, our method is scalable and distributable. The derived conditions can be viewed as implicit contracts between different parts of the program, and thus enable an incremental program analysis. △ Less

Submitted 3 August, 2015; v1 submitted 14 July, 2015; originally announced July 2015.

Comments: Extended technical report version of the conference paper at FMCAD'15

The computability path ordering

Authors: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Abstract: This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminati… ▽ More This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminating type checks from some recursive calls and by incorporating the treatment of bound variables as in the com-putability closure. The well-foundedness proof shows that core CPO captures the essence of computability arguments á la Tait and Girard, therefore explaining its name. We further show that no further type check can be eliminated from its recursive calls without loosing well-foundedness, but for one for which we found no counterexample yet. Two extensions of core CPO are then introduced which allow one to consider: the first, higher-order inductive types; the second, a precedence in which some function symbols are smaller than application and abstraction. △ Less

Submitted 22 October, 2015; v1 submitted 12 June, 2015; originally announced June 2015.

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 4 (October 26, 2015) lmcs:1604

The computability path ordering: the end of a quest

Authors: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Abstract: In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved o… ▽ More In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering. △ Less

Submitted 16 June, 2008; originally announced June 2008.

Comments: Dans CSL'08 (2008)

HORPO with Computability Closure : A Reconstruction

Authors: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Abstract: This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types. This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types. △ Less

Submitted 27 August, 2007; originally announced August 2007.

Journal ref: Dans 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning LNCS (2007)

Higher-Order Termination: from Kruskal to Computability

Authors: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Abstract: Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been an important issue for showing programs correct. In the early days of logic, strong normalization was usually shown by assigning ordinals to expressions in s… ▽ More Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been an important issue for showing programs correct. In the early days of logic, strong normalization was usually shown by assigning ordinals to expressions in such a way that eliminating a cut would yield an expression with a smaller ordinal. In the early days of verification, computer scientists used similar ideas, interpreting the arguments of a program call by a natural number, such as their size. Showing the size of the arguments to decrease for each recursive call gives a termination proof of the program, which is however rather weak since it can only yield quite small ordinals. In the sixties, Tait invented a new method for showing cut elimination of natural deduction, based on a predicate over the set of terms, such that the membership of an expression to the predicate implied the strong normalization property for that expression. The predicate being defined by induction on types, or even as a fixpoint, this method could yield much larger ordinals. Later generalized by Girard under the name of reducibility or computability candidates, it showed very effective in proving the strong normalization property of typed lambda-calculi... △ Less

Submitted 5 January, 2007; v1 submitted 8 September, 2006; originally announced September 2006.

Journal ref: Dans 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - LPAR 2006 4246 (2006)