Provably correct software is one of the key challenges of our software-driven society. Program synthesis—the task of constructing a program satisfying a given specification—is one strategy for achieving this. The result of this task is then a program that is correct by design. As in the domain of program verification, handling loops is one of the main ingredients to a successful synthesis procedure. We present an algorithm for synthesizing loops satisfying a given polynomial loop invariant. The class of loops we are considering can be modeled by a system of algebraic recurrence equations with constant coefficients, thus encoding program loops with affine operations among program variables. We turn the task of loop synthesis into a polynomial constraint problem by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications toward synthesizing loops satisfying a given polynomial loop invariant—program verification—as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops, we implement and evaluate the method using the Absynth tool.

Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursion. For such programs one needs additional information, for example in the form of loop invariants, expressing properties to hold at intermediate program points. In this paper we study program loops with non-trivial arithmetic, implementing addition and multiplication among numeric program variables. We present a new approach for automatically generating all polynomial invariants of a class of such programs. Our approach turns programs into linear ordinary recurrence equations and computes closed form solutions of these equations. These closed forms express the most precise inductive property, and hence invariant. We apply Gröbner basis computation to obtain a basis of the polynomial invariant ideal, yielding thus a finite representation of all polynomial invariants. Our work significantly extends the class of so-called P-solvable loops by handling multiplication with the loop counter variable. We implemented our method in the Mathematica package Aligator and showcase the practical use of our approach.

This paper presents the Angry-HEX artificial intelligent agent that participated in the 2013 and 2014 Angry Birds Artificial Intelligence Competitions. The agent has been developed in the context of a joint project between the University of Calabria (UniCal) and the Vienna University of Technology (TU Vienna). The specific issues that arise when introducing artificial intelligence in a physics-based game are dealt with a combination of traditional imperative programming and declarative programming, used for modeling discrete knowledge about the game and the current situation. In particular, we make use of HEX programs, which are an extension of answer set programming (ASP) programs toward integration of external computation sources, such as 2-D physics simulation tools.