(Un)solvable loop analysis

DOI10.1007/S10703-024-00455-0MaRDI QIDQ6987107zbMATH OpenFDO

Authors Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovič

Publication date 7 May 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

verificationinvariant generationsolvable operatorsalgebraic recurrencessolvable loop synthesis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• scientific article; zbMATH DE number 5578049 (Why is no real title available?)
• scientific article; zbMATH DE number 3479037 (Why is no real title available?)
• scientific article; zbMATH DE number 1973372 (Why is no real title available?)
• Algebraic tools for computing polynomial loop invariants
• Aligator.jl -- a Julia package for loop invariant generation
• An axiomatic basis for computer programming
• Analysis of Bayesian networks via prob-solvable loops
• Automated generation of non-linear loop invariants utilizing hypergeometric sequences
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Automatic Generation of Polynomial Loop Invariants
• Computing polynomial program invariants
• Computing the algebraic relations of \(C\)-finite sequences and multisequences
• Deductive proofs of almost sure persistence and recurrence properties
• Generating all polynomial invariants in simple loops
• Invariant generation for multi-path loops with polynomial assignments
• Logical analysis of programs
• Parallelotope Bundles for Polynomial Reachability
• Polynomial automorphisms and invariants.
• Polynomial invariants by linear algebra
• Quasi-translations and counterexamples to the Homogeneous Dependence Problem
• Reasoning Algebraically About P-Solvable Loops
• Search for homogeneous polynomial invariants and a cubic-homogeneous mapping without quadratic invariants
• Simple mathematical models with very complicated dynamics
• Solving invariant generation for unsolvable loops
• TRACE MAPS, INVARIANTS, AND SOME OF THEIR APPLICATIONS
• Termination of polynomial loops
• The Jacobian conjecture: Reduction of degree and formal expansion of the inverse
• The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
• Trace maps as 3D reversible dynamical systems with an invariant
• Weakest precondition reasoning for expected run-times of probabilistic programs

This page was built for publication: (Un)solvable loop analysis

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