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

research-article

A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL

Author:

Manuel EberlAuthors Info & Claims

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Pages 75 - 83

https://doi.org/10.1145/2676724.2693166

Published: 13 January 2015 Publication History

Abstract

Sturm sequences are a method for computing the number of real roots of a univariate real polynomial inside a given interval efficiently. In this paper, this fact and a number of methods to construct Sturm sequences efficiently have been formalised with the interactive theorem prover Isabelle/HOL. Building upon this, an Isabelle/HOL proof method was then implemented to prove interesting statements about the number of real roots of a univariate real polynomial and related properties such as non-negativity and monotonicity.

References

[1]

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In Proc. 36th ACM Symposium on Principles of Programming Languages, pages 340--353, 2009.

Digital Library

[2]

N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In Proc. 2009 ACM SIGPLAN International Conference on Functional Programming, pages 97--108, 2009.

Digital Library

[3]

L. Beringer, G. Stewart, R. Dockins, and A. W. Appel. Verified compilation for shared-memory C. In Proc. 2014 European Symposium on Programming (ESOP'14), volume 8410 of LNCS, pages 107--127. Springer-Verlag, Apr. 2014.

Digital Library

[4]

S. D. Brookes. Full abstraction for a shared-variable parallel language. Inf. Comput., 127(2):145--163, 1996.

[5]

E. W. Dijkstra. A constructive approach to the problem of program correctness. BIT Numerical Mathematics, 8:174--186, 1968.

[6]

R. Dockins. Operational Refinement for Compiler Correctness. PhD thesis, Princeton University, 2012.

Digital Library

[7]

D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. In Proc. 24th IEEE Symposium on Logic in Computer Science, pages 71--80, 2009.

Digital Library

[8]

D. Ghica and N. Tzevelekos. A system-level game semantics. In Proc. 28th Conf. on the Mathematical Foundations of Programming Semantics (MFPS), 2012.

Digital Library

[9]

C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In Proc. 38th ACM Symposium on Principles of Programming Languages, pages 133--146, 2011.

Digital Library

[10]

C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In Proc. 39th ACM Symposium on Principles of Programming Languages, pages 59--72, 2012.

Digital Library

[11]

X. Leroy. The CompCert verified compiler. http://compcert.inria.fr/, 2005--2013.

[12]

X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, 2009.

Digital Library

[13]

X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformation. Journal of Automated Reasoning, 2008.

Digital Library

[14]

X. Leroy and H. Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284--304, 2009.

Digital Library

[15]

C. C. Morgan. Programming from specifications, 2nd Edition. Prentice Hall International series in computer science. Prentice-Hall, 1994.

Digital Library

[16]

M. Müller-Olm. Modular Compiler Verification -- A Refinement- Algebraic Approach Advocating Stepwise Abstraction, volume 1283 of Lecture Notes in Computer Science. Springer, 1997.

[17]

A. Pitts and I. Stark. Operational reasoning for functions with local state. In HOOTS'98, pages 227--274, 1998.

Digital Library

[18]

T. Ramananandro, Z. Shao, S.-C. Weng, J. Koenig, and Y. Fu. A compositional semantics for verified separate compilation and linking. Technical Report YALEU/DCS/TR-1494, Dept. of Computer Science, Yale University, New Haven, CT, December 2014. URL: flint.cs.yale.edu/publications/vscl.html.

[19]

G. Stewart, L. Beringer, S. Cuellar, and A. W. Appel. Compositional CompCert. In Proc. 42nd ACM Symposium on Principles of Programming Languages, page (to appear), 2015.

Digital Library

[20]

The Coq development team. The Coq proof assistant. http://coq.inria.fr, 1999 - 2015.

[21]

N. Wirth. Program development by stepwise refinement. Communications of the ACM, 14(4):221--227, Apr. 1971.

Digital Library

[22]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Proc. 2011 ACM Conference on Programming Language Design and Implementation, pages 283--294, 2011.

Digital Library

Cited By

Kosaian KTan YPlatzer AKrebbers RTraytel DPientka BZdancewic S(2023)A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOLProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575672(211-224)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575672
Barbosa HReynolds AKremer GLachnitt HNiemetz ANötzli AOzdemir APreiner MViswanathan AViteri SZohar YTinelli CBarrett C(2022)Flexible Proof Production in an Industrial-Strength SMT SolverAutomated Reasoning10.1007/978-3-031-10769-6_3(15-35)Online publication date: 1-Aug-2022
https://doi.org/10.1007/978-3-031-10769-6_3
Li WPaulson LMahboubi AMyreen M(2019)Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theoremProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294092(52-64)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294092
Show More Cited By

Index Terms

A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL

Recommendations

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs

We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent ...
Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems

Sturm's theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm's theorem is known as ...
Programming and verifying a declarative first-order prover in Isabelle/HOL

We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

January 2015

192 pages

ISBN:9781450332965

DOI:10.1145/2676724

Program Chairs:
Xavier Leroy
Inria Paris-Rocquencourt, France
,
Alwen Tiu
Nanyang Technological University, Singapore

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

CPP '15 Paper Acceptance Rate 18 of 26 submissions, 69%;

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

16
Total Citations
View Citations
106
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kosaian KTan YPlatzer AKrebbers RTraytel DPientka BZdancewic S(2023)A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOLProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575672(211-224)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575672
Barbosa HReynolds AKremer GLachnitt HNiemetz ANötzli AOzdemir APreiner MViswanathan AViteri SZohar YTinelli CBarrett C(2022)Flexible Proof Production in an Industrial-Strength SMT SolverAutomated Reasoning10.1007/978-3-031-10769-6_3(15-35)Online publication date: 1-Aug-2022
https://doi.org/10.1007/978-3-031-10769-6_3
Li WPaulson LMahboubi AMyreen M(2019)Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theoremProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294092(52-64)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294092
Li WPaulson L(2019)Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-019-09521-3Online publication date: 3-Apr-2019
https://doi.org/10.1007/s10817-019-09521-3
Li WPassmore GPaulson L(2019)Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-017-9424-662:1(69-91)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1007/s10817-017-9424-6
Paulson LNipkow TWenzel M(2019)From LCF to Isabelle/HOLFormal Aspects of Computing10.1007/s00165-019-00492-1Online publication date: 2-Sep-2019
https://doi.org/10.1007/s00165-019-00492-1
Divasón JJoosten SKunčar OThiemann RYamada A(2018)Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167103(2-13)Online publication date: 2018
https://doi.org/10.1145/3176245.3167103
Djalal B(2018)A constructive formalisation of Semi-algebraic sets and functionsProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167099(240-251)Online publication date: 2018
https://doi.org/10.1145/3176245.3167099
Divasón JJoosten SKunčar OThiemann RYamada AAndronick JFelty A(2018)Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167103(2-13)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167103
Djalal BAndronick JFelty A(2018)A constructive formalisation of Semi-algebraic sets and functionsProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167099(240-251)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167099
Show More Cited By

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