Article

Free access

Automatic discovery of linear restraints among variables of a program

Authors:

Patrick Cousot,

Nicolas HalbwachsAuthors Info & Claims

POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 84 - 96

https://doi.org/10.1145/512760.512770

Published: 01 January 1978 Publication History

PDF eReader

References

[1]

M. L. BALINSKI, An algorithm for finding all vertices of convex polyhedral sets, J. Soc. Indust. Appl. Mathem., 9, {March 1961}

Google Scholar

[2]

A. CHARNES, W. W. COOPER and A. HENDERSON, An Introduction to Linear Programming, J.Wiley, New-York, {1953}

Google Scholar

[3]

P. COUSOT and R. COUSOT, Static determination of dynamic properties of programs, 2nd Int. Symposium on Programming, B. Robinet(Ed.), Dunod, Paris, {1976}

Google Scholar

[4]

P. COUSOT and R. COUSOT, Abstracts interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conf. Record of the 4th ACM Symposium on Principles of Programming Languages, {Jan.1977}

Digital Library

Google Scholar

[5]

N. E. DYER and L. G. PROLL, An algorithm for determining all extreme points of a convex polytope, Mathematical Programming, 12, {1977}

Google Scholar

[6]

M. KARR, Affine relationships among variables of a program, Acta Informatica, 6, {1976}

Google Scholar

[7]

V. KLEE, Some characterizations of convex polyhedra, Acta Mathematica, 102, {1959}

Google Scholar

[8]

V. KLEE, On the number of vertices of a convex polytope, Canadian J. of Mathematics, 16,{1964}

Google Scholar

[9]

D. E. KNUTH, The art of computer programming, vol.3, Sorting and Searching, Addison-Wensley Pub.Co., Reading, Mass, {1973}

Digital Library

Google Scholar

[10]

H. W. KUHN, Solvability and consistency for linear equations and inequalities, Amer. Math. Monthly, 63, {1956}

Google Scholar

[11]

E. LANERY, Recherche d'un système générateur minimal d'un polyhedre convexe, Thèse de 3ème cycle, Caen, France, {1966}

Google Scholar

[12]

M. MANAS and J. NEDOMA, Finding all vertices of a convex polyhedron, Numerische Mathematik, 12, {1968}

Google Scholar

[13]

T. H. MATTHEIS, An algorithm for determining irrelevant constraints and all vertices in systems of linear inequalities, Operations Research, 21, {1973}

Google Scholar

[14]

T. L. SAATY, The number of vertices of a polyhedron, Amer. Math. Monthly, 62, {1955}

Google Scholar

[15]

M. SIMONNARD, Programmation Linéaire, Dunod, Paris, {1973}

Google Scholar

[16]

N. SUZUKI and K. ISHIHATA, Implementation of an array bound checker, Conf. Record of the 4th ACM Symposium on Principles of programming languages, {Jan.1977}

Digital Library

Google Scholar

[17]

B. WEGBREIT, Property extraction in well founded property sets, IEEE Trans. on Soft. Eng., vol. SE-1, no3, {Sept.1975}

Google Scholar

[18]

H. WEYL, The elementary theory of convex polyhedra, Annals of Math. Study, 24, {1950}

Google Scholar

Cited By

View all

Pirzada MReger GBhayat ACordeiro LFilkov VRay BZhou M(2024)LLM-Generated Invariants for Bounded Model Checking Without Loop UnrollingProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695512(1395-1407)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695512
Wu GCao WYao YWei HChen TMa XFilkov VRay BZhou M(2024)LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695014(406-417)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695014
Negrini LPresotto SFerrara PZaffanella ECortesi AArceri VPasqua M(2024)Stability: An Abstract Domain for the Trend of Variation of Numerical VariablesProceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains10.1145/3689609.3689995(10-17)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689609.3689995
Show More Cited By

Recommendations

Talk amongst yourselves: inviting users to participate in online conversations
IUI '07: Proceedings of the 12th international conference on Intelligent user interfaces

Many small online communities would benefit from increased diversity or activity in their membership. Some communities run the risk of dying out due to lack of participation. Others struggle to achieve the critical mass necessary for diverse and ...
“Use-once” variables and linear objects: storage management, reflection and multi-threading

Programming languages should have 'use-once' variables in addition to the usual 'multiple-use' variables. 'Use-once' variables are bound to linear (unshared, unaliased, or singly-referenced) objects. Linear objects are cheap to access and manage, ...
Automatic discrimination among languages based on prosody alone

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

January 1978

264 pages

ISBN:9781450373487

DOI:10.1145/512760

Conference Chairs:
Alfred V. Aho
Bell Laboratories, Murray Hill, New Jersey
,
Stephen N. Zilles
IBM, San Jose, California
,
Program Chair:
Thomas G. Szymanski
Princeton University, Princeton, New Jersey

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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1978

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '78 Paper Acceptance Rate 27 of 135 submissions, 20%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

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

1,186
Total Citations
View Citations
2,251
Total Downloads

Downloads (Last 12 months)274
Downloads (Last 6 weeks)35

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pirzada MReger GBhayat ACordeiro LFilkov VRay BZhou M(2024)LLM-Generated Invariants for Bounded Model Checking Without Loop UnrollingProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695512(1395-1407)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695512
Wu GCao WYao YWei HChen TMa XFilkov VRay BZhou M(2024)LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695014(406-417)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695014
Negrini LPresotto SFerrara PZaffanella ECortesi AArceri VPasqua M(2024)Stability: An Abstract Domain for the Trend of Variation of Numerical VariablesProceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains10.1145/3689609.3689995(10-17)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689609.3689995
Greiner SBühlmann NOhrndorf MTsigkanos CNierstrasz OKehrer TChiba SThüm T(2024)Automated Generation of Code Contracts: Generative AI to the Rescue?Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690738(1-14)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690738
Ascari FBruni RGori R(2024)Limits and Difficulties in the Design of Under-Approximation Abstract DomainsACM Transactions on Programming Languages and Systems10.1145/366601446:3(1-31)Online publication date: 10-Oct-2024
https://dl.acm.org/doi/10.1145/3666014
Rivera JFranchetti FPüschel M(2024)Floating-Point TVPI Abstract DomainProceedings of the ACM on Programming Languages10.1145/36563958:PLDI(442-466)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656395
Banerjee DXu CSingh G(2024)Input-Relational Verification of Deep Neural NetworksProceedings of the ACM on Programming Languages10.1145/36563778:PLDI(1-27)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656377
Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Liu JXing YShi XSong FXu ZMing Z(2024)Abstraction and Refinement: Towards Scalable and Exact Verification of Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/364438733:5(1-35)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3644387
Cousot P(2024)Calculational Design of [In]Correctness Transformational Program Logics by Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36328498:POPL(175-208)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632849
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

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

Cited By

Recommendations

Talk amongst yourselves: inviting users to participate in online conversations

“Use-once” variables and linear objects: storage management, reflection and multi-threading

Automatic discrimination among languages based on prosody alone