Article

Multiple Counters Automata, Safety Analysis and Presburger Arithmetic

Authors:

Hubert Comon,

Yan JurskiAuthors Info & Claims

CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification

Pages 268 - 279

Published: 28 June 1998 Publication History

Abstract

No abstract available.

Cited By

View all

Kincaid ZBreck JCyphert JReps T(2019)Closed forms for numerical loopsProceedings of the ACM on Programming Languages10.1145/32903683:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290368
Boutonnet RHalbwachs N(2018)Improving the results of program analysis by abstract interpretation beyond the decreasing sequenceFormal Methods in System Design10.1007/s10703-017-0310-y53:3(384-406)Online publication date: 1-Dec-2018
https://dl.acm.org/doi/10.1007/s10703-017-0310-y
Konečný F(2016)PTIME Computation of Transitive Closures of Octagonal RelationsProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_42(645-661)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_42
Show More Cited By

Multiple Counters Automata, Safety Analysis and Presburger Arithmetic
1. Security and privacy
  1. Software and application security

Recommendations

Bounds on the automata size for Presburger arithmetic

Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by the automata-based approach for Presburger arithmetic. In this article, we give an ...
Visibly Pushdown Automata and Transducers with Counters
Non-Classical Models of Automata and Applications VI

We generalize the models of visibly pushdown automata (VPDAs) and visibly pushdown transducers (VPDTs) by equipping them with reversal-bounded counters. We show that some of the results for VPDAs and VPDTs (e.g., closure under intersection and ...
On the use of non-deterministic automata for presburger arithmetic
CONCUR'10: Proceedings of the 21st international conference on Concurrency theory

A well-known decision procedure for Presburger arithmetic uses deterministic finite-state automata. While the complexity of the decision procedure for Presburger arithmetic based on quantifier elimination is known (roughly, there is a double-exponential ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification

June 1998

550 pages

ISBN:3540646086

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 June 1998

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kincaid ZBreck JCyphert JReps T(2019)Closed forms for numerical loopsProceedings of the ACM on Programming Languages10.1145/32903683:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290368
Boutonnet RHalbwachs N(2018)Improving the results of program analysis by abstract interpretation beyond the decreasing sequenceFormal Methods in System Design10.1007/s10703-017-0310-y53:3(384-406)Online publication date: 1-Dec-2018
https://dl.acm.org/doi/10.1007/s10703-017-0310-y
Konečný F(2016)PTIME Computation of Transitive Closures of Octagonal RelationsProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_42(645-661)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_42
Alberti FGhilardi SSharygina N(2015)A New Acceleration-Based Combination Framework for Array PropertiesProceedings of the 10th International Symposium on Frontiers of Combining Systems - Volume 932210.1007/978-3-319-24246-0_11(169-185)Online publication date: 21-Sep-2015
https://dl.acm.org/doi/10.1007/978-3-319-24246-0_11
Bozga MIosif RKoneăźNý F(2014)Safety Problems Are NP-complete for Flat Integer Programs with Octagonal LoopsProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_14(242-261)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_14
Vasanta Lakshmi KAcharya AKomondoor R(2014)Checking Liveness Properties of Presburger Counter Systems Using Reachability AnalysisProceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 844210.1007/978-3-319-06410-9_24(335-350)Online publication date: 12-May-2014
https://dl.acm.org/doi/10.1007/978-3-319-06410-9_24
Demri S(2013)On selective unboundedness of VASSJournal of Computer and System Sciences10.1016/j.jcss.2013.01.01479:5(689-713)Online publication date: 1-Aug-2013
https://dl.acm.org/doi/10.1016/j.jcss.2013.01.014
Halbwachs NHenry J(2012)When the decreasing sequence failsProceedings of the 19th international conference on Static Analysis10.1007/978-3-642-33125-1_15(198-213)Online publication date: 11-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33125-1_15
Demri SDhar ASangnier A(2012)Taming past LTL and flat counter systemsProceedings of the 6th international joint conference on Automated Reasoning10.1007/978-3-642-31365-3_16(179-193)Online publication date: 26-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31365-3_16
Göller SHaase COuaknine JWorrell J(2012)Branching-Time model checking of parametric one-counter automataProceedings of the 15th international conference on Foundations of Software Science and Computational Structures10.1007/978-3-642-28729-9_27(406-420)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28729-9_27
Show More Cited By

View Options

View options

Login options

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

Abstract

Cited By

Recommendations

Bounds on the automata size for Presburger arithmetic

Visibly Pushdown Automata and Transducers with Counters

On the use of non-deterministic automata for presburger arithmetic

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations