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
88
views
15
references
Top references
cited by
42
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,415
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Computer Aided Verification
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
other
Author(s):
Yeting Ge
,
Leonardo de Moura
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 Research
Most cited references
15
Record
: found
Abstract
: not found
Book Chapter
: not found
Boogie: A Modular Reusable Verifier for Object-Oriented Programs
Mike Barnett
,
Bor-Yuh Chang
,
Robert DeLine
…
(2006)
0
comments
Cited
73
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Simplify: a theorem prover for program checking
David Detlefs
,
Greg Nelson
,
James Saxe
(2005)
0
comments
Cited
52
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Yeting Ge
,
Leonardo de Moura
(2009)
0
comments
Cited
42
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2009
Pages
: 306-320
DOI:
10.1007/978-3-642-02658-4_25
SO-VID:
0f5fe2d4-334e-4b7c-b90a-fab623f40d50
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,415
A theorem of Brown–Halmos type on the Bergman space modulo finite rank operators
Authors:
Xuanhao Ding
,
Yueshi Qin
,
Dechao Zheng
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
Authors:
Makoto Hamana
On Larcher's theorem concerning good lattice points and multiplicative subgroups modulo p
Authors:
Dmitrii M. Ushanov
,
Nikolay Moshchevitin
See all similar
Cited by
42
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Authors:
Yeting Ge
,
Leonardo de Moura
Satisfiability Modulo Theories
Authors:
Clark Barrett
,
Cesare Tinelli
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
Authors:
Andrew Reynolds
,
Morgan Deters
,
Viktor Kuncak
…
See all cited by