Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions

Jun Liu; Maxwell Fitzsimmons

REVIEW 3 major objections 5 minor 37 references

Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A simple parity condition on sign-definite polynomials lets automated synthesis of global Lyapunov functions succeed on problems where sampling-based and SMT baselines fail.

desk verdict A practical symbolic pre-processing step that makes SMT/LP Lyapunov synthesis work on several benchmarks; worth a serious referee, but the LaSalle loop's unspecified r values and parameters need fixing before the empirical claims are fully auditable. read the letter →

arxiv 2506.18171 v1 pith:UOUWCES5 submitted 2025-06-22 eess.SY cs.SYmath.DSmath.OC

Jun Liu , Maxwell Fitzsimmons This is my paper · ORCID

classification eess.SYcs.SYmath.DSmath.OC MSC 93D3093D2034D20

keywords polynomialLyapunovfunctionsglobalasymptoticstabilitysymbolicreductionsign-definitepolynomialssatisfiabilitymodulotheoriesLaSalleinvarianceprincipleSMTsynthesiscounterexample-guided

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper makes the automated search for polynomial Lyapunov functions, which certify that a dynamical system converges to the origin from everywhere, more reliable by applying symbolic algebra before numerical or logical search. It proves that any polynomial staying nonpositive on all of $\mathbb{R}^n$ must have even lowest and highest total degrees, nonpositive extremal homogeneous parts, and even exponent factors on certain leading monomials. These necessary conditions are turned into symbolic reduction rules that prune impossible terms from a Lyapunov template before an optimizer or an SMT solver runs. The paper also gives a LaSalle-type sufficient condition using higher Lie derivatives so that weak Lyapunov functions can still certify global asymptotic stability, and an SMT-encoded instability test that quickly disproves global stability for many random systems.

What carries the argument

The machinery is the pair of results built around sign-definite polynomials and the Lie-derivative chain. The first is the parity/degree identity of Proposition 1: a globally nonpositive polynomial cannot have an odd lowest or highest total degree, and its extremal homogeneous parts must themselves be nonpositive. Its computational use is symbolic reduction: compute the Lie derivative of the template $V$, impose the necessary coefficient constraints on the offending monomials, and solve those linear constraints to remove impossible terms before calling an SMT solver or an optimizer. The second is the LaSalle condition of Proposition 2, defined through the sets $C_k=\{x: L^1_fV(x)=\cdots=L^k_fV(x)=0\}$: if $C_1\cap\cdots\cap C_r=\{0\}$ for some finite $r$, then a weak Lyapunov function suffices to prove global asymptotic stability, and this condition is encoded as an SMT formula with higher Lie derivatives.

What would settle it

Try to construct, using quantifier elimination on real closed fields, a polynomial $p$ with $p(x)\le 0$ for all $x$ whose highest-degree homogeneous part has odd total degree; any such polynomial would falsify Proposition 1(1). For the LaSalle procedure, take a known globally asymptotically stable system with a weak Lyapunov function whose Lie derivative vanishes on a continuum containing nonzero points, and decide exactly whether $C_1\cap\cdots\cap C_r=\{0\}$ for some finite $r$; if no finite $r$ collapses the chain, the finite-$r$ SMT check would incorrectly report that no such weak Lyapunov function exists.

Watch

Extended reading notes

Core claim

The central discovery is Proposition 1: a polynomial $p(x)=\sum_{l\le|\alpha|\le k} c_\alpha x^\alpha$ that satisfies $p(x)\le 0$ for all $x$ must have even lowest degree $l$ and even highest degree $k$; its lowest- and highest-degree homogeneous parts $p_l$ and $p_k$ must be negative semidefinite; and any monomial whose exponent in some variable is maximal among all monomials in $p$ must have that exponent even. The same conclusions hold with signs reversed for globally nonnegative polynomials. Section 5.1 turns these necessities into reduction rules: since $\dot V=\nabla V\cdot f$ must be nonpositive for a valid global Lyapunov candidate, any terms in $\dot V$ that violate the parity and degree conditions must be forced to vanish, yielding linear equations on the template coefficients. The experiments show that this converts cases where sampling-based synthesis times out or returns invalid certificates into fast successful synthesis, including four- and six-dimensional systems and weak-Lyapunov examples solved through LaSalle's principle.

Load-bearing premise

The load-bearing premise is that a polynomial which is nonpositive on all of $\mathbb{R}^n$ really must obey the parity and degree constraints of Proposition 1; for the LaSalle-based results, it is the additional assumption that every valid weak Lyapunov function has some finite number $r$ of higher Lie derivatives that collapses the zero-set chain to the origin, and the implementation gives no proof or explicit bound for the $r$ it searches.

Editorial extensions

If this is right

For any polynomial Lyapunov candidate of a polynomial vector field, the Lie derivative's lowest- and highest-degree homogeneous parts must be even and negative semidefinite, so templates violating this can be rejected before any solver runs.
Because the reduction rules are necessary conditions, they never discard a valid Lyapunov candidate, so complete SMT synthesis over the reduced template remains sound.
Weak, non-strict Lyapunov functions can certify global asymptotic stability by checking a finite chain of higher Lie derivatives, which the paper demonstrates on examples where strict Lyapunov search fails.
Sampling-based synthesis can fail in a strong sense without reduction: on the motivating example, every finite sample set admits invalid coefficients that satisfy the sampled inequalities, so no number of samples repairs the template.
Instability can be certified with the same reduction machinery, and the paper reports sub-second disproofs of global asymptotic stability for randomly generated systems up to ten dimensions.
The reduction rules shrink the parameter space before solving, which the experiments show is often the difference between timeout and a valid certificate.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A direct test of how much of the difficulty is algebraic rather than computational would be to run the reduced-template SMT synthesis against a brute-force coefficient search on the same examples; the gap measures the value of the symbolic step.
The LaSalle procedure's finite $r$ is a heuristic in the implementation: the paper cites an algebraic descending-chain argument for finite termination but gives no explicit bound, so an adaptive loop that keeps increasing $r$ until condition (13) holds would be a natural and testable extension.
The same parity and degree reduction should apply to local Lyapunov certificates outside a compact neighborhood of the origin, since the necessary conditions are purely algebraic and do not rely on global geometry; testing this on a compact-domain SMT formulation would check that extension.
For high-dimensional instability tests, the reduction appears to be the main enabler, suggesting that symbolic preprocessing could similarly accelerate neural or other template-based Lyapunov searches.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper is a genuinely useful engineering contribution: it packages some elementary necessary conditions on sign-definite polynomials into symbolic reduction rules that prune Lyapunov templates before SMT or LP solving. It does not change the complexity landscape or answer any open decidability question, and Proposition 1 is not deep mathematics, but the pre-processing is clearly effective on the examples—LP-CEGIS and Z3-CEGIS with reduction solve cases that the same methods without reduction cannot. The formal justification in Claim 5.4, showing that sample-based CEGIS can be permanently misled on a simple quadratic template, is a nice touch. The LaSalle-type condition in Proposition 2 is correctly stated and the authors properly credit [10,17] for the underlying idea. The archived code and verifiable certificates in the appendix are real evidence: the synthesized functions can be checked by substitution, so the concrete results are not in doubt.

The soft spots are about auditability, not correctness. First, the symbolic reduction algorithm is only described informally via examples and a remark; there is no pseudocode or precise statement of which reduction rules are applied in which order. That is minor, since the idea is simple, but a formal specification would make the results reproducible. Second, the LaSalle synthesis loop in Section 5.2 is the main worry. The paper says (18) and (19) are checked in an iterative loop up to some degree-r Lie derivative, but it never reports the maximum r tried, the actual r used for E8–E10, or whether the loop terminates by finding a certificate or by hitting a bound. If the implementation stops at a fixed bound and returns unsatisfiable, that is not a valid "complete" verdict, because Proposition 2 only applies when the r actually satisfies (13), and for a fixed template no such r is guaranteed to exist a priori. The reported Lyapunov functions for E8–E10 are still valid certificates, so this is an under-auditable claim about completeness, not a broken result. Finally, Table 3 is confusing: the stable columns show 0.000 times while timeouts also appear as 0.0, and it is unclear what the Z3-complete-SR calls actually proved in the stable cases. The paper also leaves mu and other LP parameters unspecified.

My overall take: the core symbolic reduction idea is sound and worth knowing, and the paper deserves to go to peer review. It needs minor revision—specify the reduction procedure, report the LaSalle loop parameters, and clean up Table 3—but the contribution is solid and the negative result about CEGIS is a useful warning for the community. I would cite this if I were working on automated Lyapunov synthesis.

Referee Report

3 major / 5 minor

Summary. This paper proposes symbolic reduction rules for the formal synthesis of global polynomial Lyapunov functions. Proposition 1 gives necessary algebraic conditions on sign-definite polynomials, including parity constraints on lowest and highest homogeneous parts and on monomials that attain maximal exponent in a variable; these conditions are used to eliminate impossible terms from a Lyapunov template before SMT/LP synthesis. Proposition 2 reformulates LaSalle's invariance principle as a finite higher-order Lie derivative condition that can be checked by SMT. The authors present SMT-based complete synthesis for strict and weak Lyapunov functions, a LaSalle loop, instability tests, and CEGIS baselines with and without the reduction. Experiments on ten examples (E1–E10) and random instability tests up to dimension 10 show that the reduction improves success rates and runtimes, with code and data archived at a public DOI.

Significance. The core technical results are correct and practically useful. Proposition 1 is a clean, parameter-free necessary-condition result, and the symbolic reduction built on it addresses a real bottleneck: sample-based CEGIS can be misled by near-cancellations that are algebraically impossible for a sign-definite polynomial. Proposition 2's Lie-derivative condition is a practical sufficient condition for LaSalle, and the paper's use of exact SMT arithmetic to verify the synthesized certificates is a strength. The archived code (DOI 10.5281/zenodo.15272621) supports reproducibility. If the procedures are fully specified, the approach could make global Lyapunov synthesis substantially more robust than the SOS/SDP baseline in the tested regime. The paper does not overclaim the exhaustiveness of the reduction (Remark 2), and the proof of Claim 5.4 is self-contained.

major comments (3)

[Section 5.1] The reduction procedure is only illustrated, not formally specified. The text says to “introduce symbolic equality and inequality constraints” from Proposition 1, but it does not define the algorithm for selecting which monomials to test, how to handle iterated reductions after coefficients are zeroed (e.g., when the lowest or highest degree changes), or when the procedure terminates. Since the paper's central claim is that symbolic reduction is a systematic preprocessing method, this under-specification makes the method unauditable from the manuscript alone; the archived code alleviates, but does not replace, a formal description of the algorithm.
[Section 5.2, Eqs. (18)–(19)] The iterative LaSalle loop is not specified: no maximum r, no increment rule, and no r values are reported for E8–E10. Proposition 2 requires existence of a finite r satisfying (13), but for a fixed template such an r is not guaranteed a priori. If the loop stops at an implementation-chosen bound and returns “unsatisfiable”, the procedure would incorrectly report that no weak Lyapunov function of the given form exists even though a larger r would work. The concrete certificates in Table 2 can be checked, so the reported Lyapunov functions are valid, but the “complete synthesis” label for the LaSalle module is not justified. The paper cites [10] for finite termination via the descending chain condition, but it does not prove that its own loop reaches such an r or provide a bound.
[Section 5.2, Eq. (16)] The strict-Lyapunov SMT query (16) does not encode radial unboundedness. Positive definiteness of a polynomial does not imply radial unboundedness (e.g., V(x1,x2)=x1^2+x2^2(1−x1)^2 is positive definite but bounded along the line x1=1). The text inserts “provided that V is also radially unbounded” after invoking Theorem 1, but the synthesis query and the subsequent verification step are not described as checking this condition. As written, a satisfying model of (16) may not satisfy the hypotheses of Theorem 1, so the procedure is not complete for global Lyapunov certificates unless radial unboundedness is added as a constraint or verified separately. The same omission affects the weak-Lyapunov query (17).

minor comments (5)

[Section 5.4] The claim in Section 5.4 is unnumbered, but Sections 1 and 5.4 refer to “Claim 5.4”; either number the claim or fix the cross-references.
[Section 3.2, proof of Proposition 1, part (3)] The sentence “Since pk(x) and pk(x) must be negative semi-definite” should read “Since p_l(x) and p_k(x) must be negative semi-definite”.
[Section 4] In the discussion after Example 2, “L1_f(x)” should be “L1_f V(x)” (or “\dot V(x)”) for consistency with the notation in (11).
[Section 5.1, Example 3] The derivation “Setting 2c0−2c1=0, −c2=0, and c2=0 yields c0=c1 and c2=0” would be clearer if it stated explicitly that this follows from requiring the degree-7 homogeneous part of \dot V to vanish identically (since 7 is odd), rather than from term-by-term coefficient matching.
[Section 6, Table 3] The average times of 0.000 seconds for stable cases in high dimensions should be explained (e.g., timing resolution) to avoid suspicion about the measurements.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the symbolic reduction rules are derived from a self-contained necessary-condition lemma, not fitted to the examples.

full rationale

The paper's central derivation is Proposition 1, which proves necessary algebraic conditions for a polynomial to be non-positive. The proof is self-contained and does not assume the Lyapunov synthesis results. The symbolic reduction procedure in Section 5.1 applies Proposition 1 in the correct logical direction: since a valid global Lyapunov candidate requires the Lie derivative to be non-positive, any monomial whose presence would violate the necessary conditions must be eliminated. This is ordinary modus tollens, not a definition of the Lyapunov conditions in terms of the reduction rules. The examples, including Example 3 and the tables, are demonstrations of the reduction, not fitting targets: no parameter is chosen to make a prediction come true, and the reported Lyapunov functions are independently checkable certificates. Claim 5.4 is proved explicitly for the motivating example and shows why sample-based methods without reduction can fail; the proof does not rely on the paper's own conclusions. Proposition 2, the LaSalle-type sufficient condition, is proved from continuity and the definition of the sets C_k, independent of the experimental examples. The citation of [10] is only for finite termination of an analogous condition and is not load-bearing; [17] is related work, and [18] is the paper itself but is not used as evidence for the main theorem. The statement that complete synthesis is complete 'in the sense that if the formulated SMT conditions ... are satisfiable, then a Lyapunov function can be found' is a tautology about the SMT encoding, and the paper says exactly this; it is not a derived prediction. The unspecified maximum r in the LaSalle loop is a termination and auditability concern, not a circularity: an omitted bound does not make the claimed reduction equivalent to its inputs. Overall, the derivation chain is self-contained and no circular step was found.

Assumptions & free parameters 2 free parameters · 6 assumptions · 0 invented entities

The theoretical results in Propositions 1 and 2 are mathematically self-contained given standard real analysis and the classical Lyapunov theorems cited from [15,16]. The synthesis pipeline depends on two unstated tuning parameters, mu and r, which affect experimental outcomes but not the validity of the theorems. No new physical entities or ad hoc modeling assumptions are introduced.

free parameters (2)

mu (LP margin constant) = not reported
In the LP reformulation (21), the margin constant mu scales the lower bounds on V and its derivative at sample points. Its value is not specified in the paper; it is a tunable hyperparameter affecting which candidates the LP returns.
r (LaSalle Lie derivative order) = not reported
In Section 5.2, the LaSalle condition is checked for derivatives up to order r, and the synthesis iterates over r. The r values used for E8-E10 and the random tests are not reported, so the strength of the LaSalle results cannot be fully assessed.

assumptions (6)

standard math Lyapunov's global asymptotic stability theorem (Theorem 1)
Quoted from [15] and used as the correctness target for strict Lyapunov functions.
standard math LaSalle's invariance principle (Theorem 2)
Quoted from [15] and used in Proposition 2 and the synthesis procedure in Section 5.2.
standard math Instability theorem (Theorem 3)
Quoted from [16], used for SMT-based instability certificates.
domain assumption Polynomial vector field with f(0)=0 (system (1))
The entire treatment is restricted to polynomial vector fields, stated in Section 2.
standard math Sufficient smoothness and continuity of flows for deriving higher Lie derivatives
Used in the proof of Proposition 2 to argue trajectories leave the zero set when a higher Lie derivative is nonzero.
domain assumption Existence of a finite r satisfying (13) for the LaSalle procedure
The procedure searches over r up to an unspecified bound; correctness of the algorithm's termination relies on the descending chain condition argument from [10], which is cited but not proved in this paper.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions." pith.science (2026). https://pith.science/paper/UOUWCES5

@misc{pith2026250618171,
  author       = {Pith},
  title        = {Pith review of: Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UOUWCES5}},
  note         = {Machine review of arXiv:2506.18171}
}

read the original abstract

We investigate the formal synthesis of global polynomial Lyapunov functions for polynomial vector fields. We establish that a sign-definite polynomial must satisfy specific algebraic constraints, which we leverage to develop a set of straightforward symbolic reduction rules. These rules can be recursively applied to symbolically simplify the Lyapunov candidate, enabling more efficient and robust discovery of Lyapunov functions via optimization or satisfiability modulo theories (SMT) solving. In many cases, without such simplification, finding a valid Lyapunov function is often infeasible. When strict Lyapunov functions are unavailable, we design synthesis procedures for finding weak Lyapunov functions to verify global asymptotic stability using LaSalle's invariance principle. Finally, we encode instability conditions for Lyapunov functions and develop SMT procedures to disprove global asymptotic stability. Through a series of examples, we demonstrate that the proposed symbolic reduction, LaSalle-type conditions, and instability tests allow us to efficiently solve many cases that would otherwise be challenging.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 35 canonical work pages

[10]

In: 2020 7th International Conference on Control, Decision and Information Technologies (CoDIT)

Gerbet, D., Röbenack, K.: Proving asymptotic stability with LaSalle’s invariance principle: On the automatic computation of invariant sets using quantifier elimina- tion. In: 2020 7th International Conference on Control, Decision and Information Technologies (CoDIT). vol. 1, pp. 306–311. IEEE (2020)

work page 2020
[1]

In: Proc

Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Automated formal synthesis of digital controllers for state-space physical plants. In: Proc. of CAV. pp. 462–482. Springer (2017)

work page 2017
[2]

Stability of Polynomial Differential Equations: Complexity and Converse Lyapunov Questions

Ahmadi, A.A., Parrilo, P.A.: Stability of polynomial differential equations: Com- plexity and converse Lyapunov questions. arXiv preprint arXiv:1308.6833 (2013)

work page Pith review arXiv 2013
[3]

In: Proc

Ahmed, D., Peruffo, A., Abate, A.: Automated and sound synthesis of Lyapunov functions with SMT solvers. In: Proc. of TACAS. pp. 97–114 (2020)

work page 2020
[4]

In: Proc

Arnold, V.: Problems of present day mathematics, xvii (dynamical systems and differential equations). In: Proc. Symp. Pure Math. vol. 28 (1976)

work page 1976
[5]

Handbook of model checking pp

Barrett, C., Tinelli, C.: Satisfiability modulo theories. Handbook of model checking pp. 305–343 (2018)

work page 2018
[6]

Advances in neural information processing systems32 (2019)

Chang, Y.C., Roohi, N., Gao, S.: Neural Lyapunov control. Advances in neural information processing systems32 (2019)

work page 2019
[7]

Springer, 4 edn

Cox,D.A.,Little,J.,O’Shea,D.:Ideals,Varieties,andAlgorithms:AnIntroduction to Computational Algebraic Geometry and Commutative Algebra. Springer, 4 edn. (2015)

work page 2015

Show all 37 references

[8]

In: International conference on Tools and Algorithms for the Construction and Analysis of Systems

De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–
[9]

In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control

Edwards, A., Peruffo, A., Abate, A.: Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models. In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control. pp. 1–10 (2024)

2024
[11]

Springer (2007)

Giesl, P.: Construction of Global Lyapunov Functions Using Radial Basis Func- tions. Springer (2007)

2007
[12]

Discrete and Continuous Dynamical Systems-B20(8), 2291–2331 (2015)

Giesl, P., Hafstein, S.: Review on computational methods for lyapunov functions. Discrete and Continuous Dynamical Systems-B20(8), 2291–2331 (2015)

2015
[13]

Huangfu, Q., Galabova, I., Feldmeier, M., Hall, J.A.J.: HiGHS - High Performance Software for Linear Optimization.https://highs.dev/ (2023)

2023
[14]

In: Proceedings of the 17th international conference on Hybrid systems: computation and control

Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation- guided Lyapunov analysis for hybrid dynamical systems. In: Proceedings of the 17th international conference on Hybrid systems: computation and control. pp. 133–142 (2014)

2014
[15]

Prentice-Hall (2002)

Khalil, H.K.: Nonlinear Systems. Prentice-Hall (2002)

2002
[16]

Academic Press (1961) Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions 19

LaSalle,J.,Lefschetz,S.:StabilitybyLiapunov’sDirectMethodwithApplications. Academic Press (1961) Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions 19

1961
[17]

Mathematics in Computer Science6(4), 395– 408 (2012)

Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems. Mathematics in Computer Science6(4), 395– 408 (2012)

2012
[18]

arXiv preprint (2025)

Liu, J., Fitzsimmons, M.: Symbolic reduction for formal synthesis of global lya- punov functions. arXiv preprint (2025)

2025
[19]

In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control

Liu, J., Meng, Y., Fitzsimmons, M., Zhou, R.: LyZNet: A lightweight python tool for learning and verifying neural lyapunov functions and regions of attraction. In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control. pp. 1–8 (2024)

2024
[20]

Automatica 175, 112193 (2025)

Liu, J., Meng, Y., Fitzsimmons, M., Zhou, R.: Physics-informed neural network Lyapunov functions: PDE characterization, learning, and verification. Automatica 175, 112193 (2025)

2025
[21]

International journal of control55(3), 531–534 (1992)

Lyapunov, A.M.: The general problem of the stability of motion. International journal of control55(3), 531–534 (1992)

1992
[22]

Papachristodoulou, A., Anderson, J., Valmorbida, G., Prajna, S., Seiler, P., Par- rilo, P., Peet, M., Jagt, D.: SOSTOOLS: Sum of squares optimization toolbox for MATLAB (2013)

2013
[23]

In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002

Papachristodoulou, A., Prajna, S.: On the construction of Lyapunov functions us- ing the sum of squares decomposition. In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002. vol. 3, pp. 3482–3487. IEEE (2002)

2002
[24]

In: 2015 54th IEEE conference on decision and control (CDC)

Ravanbakhsh, H., Sankaranarayanan, S.: Counter-example guided synthesis of con- trol Lyapunov functions for switched systems. In: 2015 54th IEEE conference on decision and control (CDC). pp. 4232–4239. IEEE (2015)

2015
[25]

Autonomous Robots 43, 275–307 (2019)

Ravanbakhsh, H., Sankaranarayanan, S.: Learning control Lyapunov functions from counterexamples and demonstrations. Autonomous Robots 43, 275–307 (2019)

2019
[26]

IFAC Proceedings Volumes46(23), 576–581 (2013)

Sankaranarayanan, S., Chen, X., et al.: Lyapunov function synthesis using Han- delman representations. IFAC Proceedings Volumes46(23), 576–581 (2013)

2013
[27]

Journal of Symbolic Computation 58, 41–63 (2013)

She, Z., Li, H., Xue, B., Zheng, Z., Xia, B.: Discovering polynomial Lyapunov functions for continuous dynamical systems. Journal of Symbolic Computation 58, 41–63 (2013)

2013
[28]

Nonlinear Analysis: Hybrid Systems3(4), 588–596 (2009)

She, Z., Xia, B., Xiao, R., Zheng, Z.: A semi-algebraic approach for asymptotic stability analysis. Nonlinear Analysis: Hybrid Systems3(4), 588–596 (2009)

2009
[29]

Optimization Methods and Software11(1-4), 625–653 (1999)

Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over sym- metric cones. Optimization Methods and Software11(1-4), 625–653 (1999)

1999
[30]

Automatica44(10), 2669–2675 (2008)

Topcu, U., Packard, A., Seiler, P.: Local stability analysis using simulations and sum-of-squares programming. Automatica44(10), 2669–2675 (2008)

2008
[31]

Nature methods17(3), 261–272 (2020)

Virtanen, P., Gommers, R., Oliphant, T.E., Haberland, M., Reddy, T., Courna- peau, D., Burovski, E., Peterson, P., Weckesser, W., Bright, J., et al.: SciPy 1.0: fundamental algorithms for scientific computing in Python. Nature methods17(3), 261–272 (2020)

2020
[32]

Advances in Neural Information Pro- cessing Systems 35, 29113–29125 (2022)

Zhou, R., Quartz, T., De Sterck, H., Liu, J.: Neural Lyapunov control of unknown nonlinear systems with stability guarantees. Advances in Neural Information Pro- cessing Systems 35, 29113–29125 (2022)

2022
[33]

Zubov, V.I.: Methods of AM Lyapunov and Their Application, vol. 4439. US Atomic Energy Commission (1961) 20 Liu and Fitzsimmons A Description of Examples in Case Studies In this section, we provide details of the examples (E1)–(E10) included in the case studies in Section 6. W...

1961
[34]

(E4) Consider the model [26] ˙x = −x3 1 +x2 −x1−x2

Neither can be verified as a global Lya- punov function (even after removing the negligible term from the one returned by SOSTOOLS). (E4) Consider the model [26] ˙x = −x3 1 +x2 −x1−x2 . The results are as follows: – Z3-Complete-SR: V (x) = x2 1 +x2 2. – LP-CEGIS: V (x) = x2 1/...
[35]

For the first system, Z3-Complete-SR-LaSalle foundV (x) = x4 1 + 2x2 2, LP- CEGIS-SR-LaSalle returned V (x) = x4 1/100 + x2 2/50, and Z3-CEGIS-SR- LaSalle computedV (x) = x4 1 + 2x2 2
[36]

For the second system, Z3-Complete-SR-LaSalle obtainedV (x) = x6 1 + 3x2 2, LP-CEGIS-SR-LaSalle producedV (x) = x6 1/100 + 3x2 2/100, and Z3-CEGIS- SR-LaSalle foundV (x) = x6 1 + 3x2 2
[37]

For the third system, Z3-Complete-SR-LaSalle discoveredV (x) = x2 1 +x2 2, LP-CEGIS-SR-LaSalle returnedV (x) = x2 1/100 + x2 2/100, and Z3-CEGIS- SR-LaSalle also foundV (x) = x2 1 +x2 2. SOSTOOLS returnsV (x) = 0.7248x2 1− 8.155e−11x1x2 + 0.7248x2 2, which is close to an exact...

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [10]

In: 2020 7th International Conference on Control, Decision and Information Technologies (CoDIT)

Gerbet, D., Röbenack, K.: Proving asymptotic stability with LaSalle’s invariance principle: On the automatic computation of invariant sets using quantifier elimina- tion. In: 2020 7th International Conference on Control, Decision and Information Technologies (CoDIT). vol. 1, pp. 306–311. IEEE (2020)

work page 2020

[2] [1]

In: Proc

Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Automated formal synthesis of digital controllers for state-space physical plants. In: Proc. of CAV. pp. 462–482. Springer (2017)

work page 2017

[3] [2]

Stability of Polynomial Differential Equations: Complexity and Converse Lyapunov Questions

Ahmadi, A.A., Parrilo, P.A.: Stability of polynomial differential equations: Com- plexity and converse Lyapunov questions. arXiv preprint arXiv:1308.6833 (2013)

work page Pith review arXiv 2013

[4] [3]

In: Proc

Ahmed, D., Peruffo, A., Abate, A.: Automated and sound synthesis of Lyapunov functions with SMT solvers. In: Proc. of TACAS. pp. 97–114 (2020)

work page 2020

[5] [4]

In: Proc

Arnold, V.: Problems of present day mathematics, xvii (dynamical systems and differential equations). In: Proc. Symp. Pure Math. vol. 28 (1976)

work page 1976

[6] [5]

Handbook of model checking pp

Barrett, C., Tinelli, C.: Satisfiability modulo theories. Handbook of model checking pp. 305–343 (2018)

work page 2018

[7] [6]

Advances in neural information processing systems32 (2019)

Chang, Y.C., Roohi, N., Gao, S.: Neural Lyapunov control. Advances in neural information processing systems32 (2019)

work page 2019

[8] [7]

Springer, 4 edn

Cox,D.A.,Little,J.,O’Shea,D.:Ideals,Varieties,andAlgorithms:AnIntroduction to Computational Algebraic Geometry and Commutative Algebra. Springer, 4 edn. (2015)

work page 2015