Synthesis for Polynomial Lasso Programs

DOI10.1007/978-3-642-54013-4_24MaRDI QIDQ2938082zbMATH OpenOpenAlexFDO

Authors Jan Leike, Ashish Tiwari

Publication date 13 January 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1311.4046

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We present a method for the synthesis of polynomial lasso programs. These programs consist of a program stem, a set of transitions, and an exit condition, all in the form of algebraic assertions (conjunctions of polynomial equalities). Central to this approach is the discovery of non-linear (algebraic) loop invariants. We extend Sankaranarayanan, Sipma, and Manna's template-based approach and prove a completeness criterion. We perform program synthesis by generating a constraint whose solution is a synthesized program together with a loop invariant that proves the program's correctness. This constraint is non-linear and is passed to an SMT solver. Moreover, we can enforce the termination of the synthesized program with the support of test cases.

Recommendations

• Lasserre hierarchy for large scale polynomial optimization in real and complex variables
• Solving polynomial least squares problems via semidefinite programming relaxations
• scientific article; zbMATH DE number 4062814
• Towards a Genuinely Polynomial Algorithm for Linear Programming
• Sparse Polynomial Optimization
• Polynomial affine algorithms for linear programming
• scientific article; zbMATH DE number 7740918
• LP formulations for polynomial optimization problems
• Polynomial approximations for continuous linear programs
• Exploiting sparsity in complex polynomial optimization

Cited in

(6)

• Termination of single-path polynomial loop programs
• Finding polynomial loop invariants for probabilistic programs
• Linear ranking for linear lasso programs
• Algebra-Based Reasoning for Loop Synthesis
• Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
• A search-based procedure for nonlinear real arithmetic

This page was built for publication: Synthesis for Polynomial Lasso Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938082)