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
73
views
0
references
Top references
cited by
61
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
0
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Computer Aided Verification
CVC4
other
Author(s):
Clark Barrett
,
Christopher L. Conway
,
Morgan Deters
,
Liana Hadarean
,
Dejan Jovanović
,
Tim King
,
Andrew Reynolds
,
Cesare Tinelli
Publication date
(Print):
2011
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 Research
Author and book information
Book Chapter
Publication date (Print):
2011
Pages
: 171-177
DOI:
10.1007/978-3-642-22110-1_14
SO-VID:
bc5737b3-ac33-4520-a559-1bb066e70d0f
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection
pp. 470
HMC: Verifying Functional Programs Using Abstract Interpreters
pp. 50
Stability in Weak Memory Models
pp. 99
Getting Rid of Store-Buffers in TSO Analysis
pp. 149
Resolution Proofs and Skolem Functions in QBF Evaluation and Applications
pp. 165
The BINCOA Framework for Binary Code Analysis
pp. 171
CVC4
pp. 178
SLAyer: Memory Safety for Systems-Level Code
pp. 184
CPAchecker: A Tool for Configurable Software Verification
pp. 225
Model Checking Algorithms for CTMDPs
pp. 243
Quantitative Synthesis for Concurrent Programs
pp. 277
Smoothing a Program Soundly and Robustly
pp. 349
Time for Statistical Model Checking of Real-Time Systems
pp. 372
Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
pp. 379
SpaceEx: Scalable Verification of Hybrid Systems
pp. 396
From Cardiac Cells to Genetic Regulatory Networks
pp. 412
Threader: A Constraint-Based Verifier for Multi-threaded Programs
pp. 457
μZ– An Efficient Engine for Fixed Points with Constraints
pp. 463
BAP: A Binary Analysis Platform
pp. 504
Bug-Assist: Assisting Fault Localization in ANSI-C Programs
pp. 526
Language Equivalence for Probabilistic Automata
pp. 573
Interpolation-Based Software Verification with Wolverine
pp. 585
PRISM 4.0: Verification of Probabilistic Real-Time Systems
pp. 592
Program Analysis for Overlaid Data Structures
pp. 609
KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs
pp. 663
Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP
pp. 669
Practical, Low-Effort Equivalence Verification of Real Code
pp. 686
Relational Abstractions for Continuous and Hybrid Systems
pp. 703
Simplifying Loop Invariant Generation Using Splitter Predicates
pp. 743
Model Checking Recursive Programs with Numeric Data Types
Cited by
61
Satisfiability Modulo Theories
Authors:
Clark Barrett
,
Cesare Tinelli
Automating Separation Logic Using SMT
Authors:
Ruzica Piskac
,
Thomas Wies
,
Damien Zufferey
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
Authors:
Andrew Reynolds
,
Morgan Deters
,
Viktor Kuncak
…
See all cited by