Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
75
views
15
references
Top references
cited by
12
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
3,063
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Computer Aided Verification
Automatic Verification of Integer Array Programs
other
Author(s):
Marius Bozga
,
Peter Habermehl
,
Radu Iosif
,
Filip Konečný
,
Tomáš Vojnar
Publication date
(Print):
2009
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
ScienceOpen Preprints
Most cited references
15
Record
: found
Abstract
: not found
Book
: not found
The Temporal Logic of Reactive and Concurrent Systems
Zohar Manna
,
Amir Pnueli
(1992)
0
comments
Cited
158
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Multiple counters automata, safety analysis and presburger arithmetic
Hubert Comon
,
Yan Jurski
(1998)
0
comments
Cited
30
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
What’s Decidable About Arrays?
Aaron R. Bradley
,
Zohar Manna
,
Henny B. Sipma
(2005)
0
comments
Cited
29
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2009
Pages
: 157-172
DOI:
10.1007/978-3-642-02658-4_15
SO-VID:
510059c3-1da7-419d-9421-ca3645e6ac7b
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 188
Requirements Validation for Hybrid Systems
pp. 383
Quantifier Elimination via Functional Composition
pp. 35
Models and Proofs of Protocol Security: A Progress Report
pp. 51
SPEED: Symbolic Complexity Bound Analysis
pp. 696
Translation Validation: From Simulink to C
pp. 157
Automatic Verification of Integer Array Programs
pp. 204
Towards Performance Prediction of Compositional Models in Industrial GALS Designs
pp. 233
Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
pp. 263
An Antichain Algorithm for LTL Realizability
pp. 306
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
pp. 337
Sliding Window Abstraction for Infinite Markov Chains
pp. 398
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
pp. 430
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
pp. 462
Generalizing DPLL to Richer Logics
pp. 477
Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
pp. 509
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
pp. 540
Reachability Analysis of Hybrid Systems Using Support Functions
pp. 614
D-Finder: A Tool for Compositional Deadlock Detection and Verification
pp. 627
The Zonotope Abstract Domain Taylor1+
pp. 634
InvGen: An Efficient Invariant Generator
pp. 641
INFAMY: An Infinite-State Markov Model Checker
pp. 661
Apron: A Library of Numerical Abstract Domains for Static Analysis
pp. 682
MCMAS: A Model Checker for the Verification of Multi-Agent Systems
pp. 709
PAT: Towards Flexible Verification under Fairness
Similar content
3,063
Mixed integer programming formulations for single machine scheduling problems
Authors:
Ahmet Keha
,
Ketan Khowala
,
John W. Fowler
…
The Prouhet-Tarry-Escott problem for Gaussian integers
Authors:
Timothy Caley
Integer quantum Hall transition in a fraction of a Landau level
Authors:
R. Bhatt
,
Scott D. Geraedts
,
Matteo Ippoliti
See all similar
Cited by
12
A Verification Toolkit for Numerical Transition Systems
Authors:
Hossein Hojjat
,
Filip Konecny
,
Florent Garnier
…
Automatic Verification of Integer Array Programs
Authors:
Marius Bozga
,
Peter Habermehl
,
Radu Iosif
…
Accelerating Interpolants
Authors:
Hossein Hojjat
,
Radu Iosif
,
Filip Konecny
…
See all cited by