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
19
views
11
references
Top references
cited by
8
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
1,670
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Computer Aided Verification
Generalizing DPLL to Richer Logics
other
Author(s):
Kenneth L. McMillan
,
Andreas Kuehlmann
,
Mooly Sagiv
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
11
Record
: found
Abstract
: not found
Article
: not found
A machine program for theorem-proving
Martin Davis
,
George Logemann
,
Donald Loveland
(1962)
0
comments
Cited
305
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
A Computing Procedure for Quantification Theory
Martin Davis
,
Hilary Putnam
(1960)
0
comments
Cited
222
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
DPLL(T): Fast Decision Procedures
Harald Ganzinger
,
George Hagen
,
Robert Nieuwenhuis
…
(2004)
0
comments
Cited
33
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2009
Pages
: 462-476
DOI:
10.1007/978-3-642-02658-4_35
SO-VID:
4cab21bd-f579-4b70-a546-e56f7a43a6fa
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
1,670
Cross-Training A Richer Staff for Leaner Budgets
Authors:
ROSEMARY F. LYONS
,
F. Lyons
Automated crack segmentation on 3D asphalt surfaces with richer attention and hybrid pyramid structures
Authors:
Shuo Ding
,
Hong Lang
,
Jiang Chen
…
Some of America's wealthiest hospital systems ended up even richer, thanks to federal bailouts
Authors:
J. Rau
,
C. SPOLAR
See all similar
Cited by
8
Satisfiability Modulo Theories
Authors:
Clark Barrett
,
Cesare Tinelli
A Method for Symbolic Computation of Abstract Operations
Authors:
Aditya Thakur
,
Thomas Reps
Semantically-Guided Goal-Sensitive Reasoning: Model Representation
Authors:
Maria Paola Bonacina
,
David Plaisted
See all cited by