More Web Proxy on the site http://driver.im/

research-article

Formal verification of semi-algebraic sets and real analytic functions

Authors:

J. Tanner Slagel,

Aaron DutleAuthors Info & Claims

CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 278 - 290

https://doi.org/10.1145/3437992.3439933

Published: 20 January 2021 Publication History

Abstract

Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts appear in the study of Differential Equations, where the real analytic solution to a differential equation is known to enter or exit a semi-algebraic set in a predictable way. Motivated to enhance the capability to reason about differential equations in the Prototype Verification System (PVS), a formalization of multivariate polynomials, semi-algebraic sets, and real analytic functions is developed. The way that a real analytic function behaves in a neighborhood around a point where the function meets the boundary of a semi-algebraic set is described and verified. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, the behavior around the boundary of a semi-algebraic set can be very different.

References

[1]

Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub. 2016. Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. 76-87. htps://doi.org/10.1145/2854065.2854072

Digital Library

[2]

Jacek Bochnak, Michel Coste, and Marie-Françoise Roy. 2013. Real algebraic geometry. Vol. 36. Springer Science & Business Media. htps: //doi.org/10.1007/978-3-662-03718-8

[3]

Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer. 2017. Formally verified diferential dynamic logic. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. 208-221. htps://doi.org/10.1145/3018610.3018616

Digital Library

[4]

Cyril Cohen. 2013. Pragmatic quotient types in Coq. In International Conference on Interactive Theorem Proving. Springer, 213-228. htps: //doi.org/10.1007/978-3-642-39634-2_17

Digital Library

[5]

Brian A Davey and Hilary A Priestley. 2002. Introduction to lattices and order. Cambridge university press. htps://doi.org/10.1017/ CBO9780511809088

[6]

Maxime Dénès, Anders Mörtberg, and Vincent Siles. 2012. A refinement-based approach to computational algebra in Coq. In International Conference on Interactive Theorem Proving. Springer, 83-98. htps://doi.org/10.1007/978-3-642-32347-8_7

[7]

Boris Djalal. 2018. A constructive formalisation of Semi-algebraic sets and functions. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. 240-251. htps://doi.org/ 10.1145/3167099

Digital Library

[8]

Gerald B Folland. 1995. Introduction to partial diferential equations. Vol. 102. Princeton university press. htps://doi.org/10.1515/ 9780691213033

[9]

Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X : An axiomatic tactical theorem prover for hybrid systems. In International Conference on Automated Deduction. Springer, 527-538. htps://doi.org/10.1007/978-3-319-21401-6_36

[10]

Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geofrey J Gordon, and Peter Capell. 2014. Hybrid theorem proving of aerospace systems: Applications and challenges. Journal of Aerospace Information Systems 11, 10 ( 2014 ), 702-713. htps://doi.org/10.2514/1. I010178

[11]

Khalil Ghorbal, Andrew Sogokon, and André Platzer. 2017. A hierarchy of proof rules for checking positive invariance of algebraic and semialgebraic sets. Computer Languages, Systems & Structures 47 ( 2017 ), 19-43. htps://doi.org/10.1016/j.cl. 2015. 11.003

[12]

Florian Haftmann, Andreas Lochbihler, and Wolfgang Schreiner. 2014. Towards abstract and executable multivariate polynomials in Isabelle. In Isabelle Workshop, Vol. 201.

[13]

John Harrison. 1997. Verifying the accuracy of polynomial approximations in HOL. In International Conference on Theorem Proving in Higher Order Logics. Springer, 137-152. htps://doi.org/10.1007/BFb0028391

[14]

Hassan K Khalil and Jessy W Grizzle. 2002. Nonlinear systems. Vol. 3. Prentice hall Upper Saddle River, NJ.

[15]

Steven G Krantz and Harold R Parks. 2002. A primer of real analytic functions. Springer Science & Business Media. htps://doi.org/10.1007/ 978-0-8176-8134-0

[16]

Wenda Li. 2019. Towards justifying computer algebra algorithms in Isabelle/HOL. Ph. D. Dissertation. University of Cambridge. htps: //doi.org/10.17863/CAM.36637

[17]

Jiang Liu, Naijun Zhan, and Hengjun Zhao. 2011. Computing semialgebraic invariants for polynomial dynamical systems. In Proceedings of the ninth ACM international conference on Embedded software. 97-106. htps://doi.org/10.1145/2038642.2038659

Digital Library

[18]

Jiang Liu, Naijun Zhan, and Hengjun Zhao. 2011. Computing semialgebraic invariants for polynomial dynamical systems. In Proceedings of the ninth ACM international conference on Embedded software. 97-106. htps://doi.org/10.1145/2038642.2038659

Digital Library

[19]

Assia Mahboubi. 2006. Programming and certifying a CAD algorithm in the Coq system. In Dagstuhl Seminar Proceedings. Schloss DagstuhlLeibniz-Zentrum für Informatik.

[20]

Assia Mahboubi. 2007. Implementing the cylindrical algebraic decomposition within the Coq system. Mathematical Structures in Computer Science 17, 1 ( 2007 ), 99.

[21]

César Muñoz and Anthony Narkawicz. 2013. Formalization of Bernstein polynomials and applications to global optimization. Journal of Automated Reasoning 51, 2 ( 2013 ), 151-196. htps://doi.org/10.1007/ s10817-012-9256-3

Digital Library

[22]

Anthony Narkawicz, César Muñoz, and Aaron Dutle. 2015. Formallyverified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems. Journal of Automated Reasoning 54, 4 ( 2015 ), 285-326. htps://doi.org/10.1007/s10817-015-9320-x

Digital Library

[23]

Sam Owre, John M Rushby, and Natarajan Shankar. 1992. PVS: A prototype verification system. In International Conference on Automated Deduction. Springer, 748-752. htps://doi.org/10.1007/3-540-55602-8_217

[24]

Sam Owre and Natarajan Shankar. 2008. A brief overview of PVS. In International Conference on Theorem Proving in Higher Order Logics. Springer, 22-27. htps://doi.org/10.1007/978-3-540-71067-7_5

Digital Library

[25]

André Platzer. 2008. Diferential dynamic logic for hybrid systems. Journal of Automated Reasoning 41, 2 ( 2008 ), 143-189. htps://doi.org/ 10.1007/s10817-008-9103-8

Digital Library

[26]

André Platzer. 2018. Logical foundations of cyber-physical systems. Vol. 662. Springer. htps://doi.org/10.1007/978-3-319-63588-0

Digital Library

[27]

André Platzer and Jan-David Quesel. 2008. KeYmaera: A hybrid theorem prover for hybrid systems (system description). In International Joint Conference on Automated Reasoning. Springer, 171-178. htps://doi.org/10.1007/978-3-540-71070-7_15

Digital Library

[28]

André Platzer and Yong Kiam Tan. 2018. Diferential equation axiomatization: The impressive power of diferential ghosts. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. 819-828. htps://doi.org/10.1145/3209108.3209147

Digital Library

[29]

Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer. 2016. How to model and prove hybrid systems with KeYmaera: a tutorial on safety. International Journal on Software Tools for Technology Transfer 18, 1 ( 2016 ), 67-91. htps://doi.org/10.1007/ s10009-015-0367-0

Digital Library

[30]

Andrew Sogokon, Khalil Ghorbal, Paul B Jackson, and André Platzer. 2016. A method for invariant generation for polynomial continuous systems. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 268-288. htps://doi.org/10.1007/ 978-3-662-49122-5_13

Digital Library

[31]

Andrew Sogokon and Paul B Jackson. 2015. Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In International Symposium on Formal Methods. Springer, 514-531. htps://doi.org/10.1007/978-3-319-19249-9_32

[32]

Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, and André Platzer. 2019. Pegasus: A framework for sound continuous invariant generation. In International Symposium on Formal Methods. Springer, 138-157. htps://doi.org/10.1007/978-3-030-30942-8_10

[33]

Brian L Stevens, Frank L Lewis, and Eric N Johnson. 2015. Aircraft control and simulation: dynamics, controls design, and autonomous systems. John Wiley & Sons. htps://doi.org/10.1002/9781119174882

[34]

Yong Kiam Tan and André Platzer. 2020. An Axiomatic Approach to Existence and Liveness for Diferential Equations. arXiv preprint arXiv: 2004. 14561 ( 2020 ).

[35]

Morris Tenenbaum and Harry Pollard. 1963. Ordinary diferential equations: an elementary textbook for students of mathematics, engineering, and the sciences. Dover Publications.

[36]

Richard Zippel. 1993. Efective Polynomial Computation. Springer US. htps://doi.org/10.1007/978-1-4615-3188-3

Cited By

Slagel JMoscato MWhite LMuñoz CBalachandran SDutle A(2024)Embedding Differential Dynamic Logic in PVSElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.402.7402(43-62)Online publication date: 23-Apr-2024
https://doi.org/10.4204/EPTCS.402.7
White LTitolo LSlagel JMuñoz CTimany ATraytel DPientka BBlazy S(2024)A Temporal Differential Dynamic Logic Formal EmbeddingProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636943(162-176)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636943
Slagel JMuñoz CBalachandran SMoscato MDutle AMasci PWhite LGonnord LTitolo L(2022)Towards an implementation of differential dynamic logic in PVSProceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3520313.3534661(44-50)Online publication date: 14-Jun-2022
https://dl.acm.org/doi/10.1145/3520313.3534661
Show More Cited By

Index Terms

Formal verification of semi-algebraic sets and real analytic functions
1. Mathematics of computing
  1. Continuous mathematics
    1. Continuous functions
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Computing the Volume of Compact Semi-Algebraic Sets
ISSAC '19: Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation

Let S\subset \bR^n be a compact basic semi-algebraic set defined as the real solution set of multivariate polynomial inequalities with rational coefficients. We design an algorithm which takes as input a polynomial system defining S and an integer p\geq ...
Real Root Finding for Equivariant Semi-algebraic Systems
ISSAC '18: Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation

Let R be a real closed field. We consider basic semi-algebraic sets defined by n -variate equations/inequalities of s symmetric polynomials and an equivariant family of polynomials, all of them of degree bounded by 2d < n. Such a semi-algebraic set is ...
A constructive formalisation of Semi-algebraic sets and functions
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

Semi-algebraic sets and semi-algebraic functions are essential to specify and certify cylindrical algebraic decomposition algorithms. We formally define in Coq the base operations on semi-algebraic sets and functions using embedded first-order formulae ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2021

342 pages

ISBN:9781450382991

DOI:10.1145/3437992

Program Chairs:
Cătălin Hriţcu,
Andrei Popescu

Copyright © 2021 ACM.

© 2021 Association for Computing Machinery. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the United States Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 January 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CPP '21

Sponsor:

SIGPLAN

CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 17 - 19, 2021

Virtual, Denmark

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
74
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)2

Reflects downloads up to 11 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Slagel JMoscato MWhite LMuñoz CBalachandran SDutle A(2024)Embedding Differential Dynamic Logic in PVSElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.402.7402(43-62)Online publication date: 23-Apr-2024
https://doi.org/10.4204/EPTCS.402.7
White LTitolo LSlagel JMuñoz CTimany ATraytel DPientka BBlazy S(2024)A Temporal Differential Dynamic Logic Formal EmbeddingProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636943(162-176)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636943
Slagel JMuñoz CBalachandran SMoscato MDutle AMasci PWhite LGonnord LTitolo L(2022)Towards an implementation of differential dynamic logic in PVSProceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3520313.3534661(44-50)Online publication date: 14-Jun-2022
https://dl.acm.org/doi/10.1145/3520313.3534661
Huerta y Munive JStruth G(2021)Predicate Transformer Semantics for Hybrid SystemsJournal of Automated Reasoning10.1007/s10817-021-09607-xOnline publication date: 31-Oct-2021
https://doi.org/10.1007/s10817-021-09607-x
Foster SHuerta y Munive JGleirscher MStruth G(2021)Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster ProofsFormal Methods10.1007/978-3-030-90870-6_20(367-386)Online publication date: 10-Nov-2021
https://doi.org/10.1007/978-3-030-90870-6_20

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents