Amrollahi, D, Bartocci, E, Kenison, G, Kovacs, L, Moosbrugger, M and Stankovic, M (2024) (Un)Solvable loop analysis. FORMAL METHODS IN SYSTEM DESIGN. ISSN 0925-9856

Full text not available from this repository. Please see publisher or open access link below:

Abstract

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Rodríguez-Carbonell and Kapur (in: Proceedings of the ISSAC, pp 266–273, 2004), one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

Item Type:	Article
Uncontrolled Keywords:	Algebraic recurrences; Invariant generation; Solvable loop synthesis; Solvable operators; Verification; Invariant generation; Solvable loop synthesis; Algebraic recurrences; Verification; Solvable operators; 0802 Computation Theory and Mathematics; 0803 Computer Software; 0805 Distributed Computing; Electrical & Electronic Engineering
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions:	Computer Science and Mathematics
Publisher:	Springer
SWORD Depositor:	A Symplectic
Date Deposited:	04 Nov 2024 13:09
Last Modified:	06 Nov 2024 11:57
DOI or ID number:	10.1007/s10703-024-00455-0
URI:	https://researchonline.ljmu.ac.uk/id/eprint/24655

View Item