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
25
views
13
references
Top references
cited by
4
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,036
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Relational Reasoning via SMT Solving
other
Author(s):
Aboubakr Achraf El Ghazi
,
Mana Taghdiri
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
Most cited references
13
Record
: found
Abstract
: not found
Book Chapter
: not found
PVS: A prototype verification system
S. Owre
,
J. M. Rushby
,
N Shankar
(1992)
0
comments
Cited
87
times
– based on
0
reviews
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
Record
: found
Abstract
: not found
Book Chapter
: not found
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures
T. Lev-Ami
,
N. Immerman
,
T. Reps
…
(2005)
0
comments
Cited
10
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2011
Pages
: 133-148
DOI:
10.1007/978-3-642-21437-0_12
SO-VID:
fcb5c420-bc24-4042-952c-c2027d175d8a
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
Model Integration and Cyber Physical Systems: A Semantics Perspective
pp. 2
Some Thoughts on Behavioral Programming
pp. 3
The Only Way Is Up
pp. 12
Does It Pay to Extend the Perimeter of a World Model?
pp. 27
System Verification through Program Verification
pp. 57
TraceContract: A Scala DSL for Trace Analysis
pp. 73
Using Debuggers to Understand Failed Verification Attempts
pp. 88
Sampling-Based Runtime Verification
pp. 103
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
pp. 118
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems
pp. 133
Relational Reasoning via SMT Solving
pp. 169
Validated Compilation through Logic
pp. 184
Certification of Safe Polynomial Memory Bounds
pp. 215
Specifying Confidentiality in Circus
pp. 246
The Safety-Critical Java Memory Model: A Formal Account
pp. 262
Failure-Divergence Refinement of Compensating Communicating Processes
pp. 278
Termination without $\checkmark$ in CSP
pp. 293
Timed Migration and Interaction with Access Permissions
pp. 308
From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community
pp. 338
Refinement-Based Verification of Local Synchronization Algorithms
pp. 353
Simulating Concurrent Behaviors with Worst-Case Cost Bounds
pp. 369
Automatically Refining Partial Specifications for Program Verification
pp. 386
Structured Specifications for Better Verification of Heap-Manipulating Programs
pp. 402
Verification of Unloadable Modules
pp. 417
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking
pp. 432
On Combining State Space Reductions with Global Fairness Assumptions
Similar content
3,036
Improving SMT for Baltic languages with factored models
Authors:
R. Skadins
,
K Goba
,
V Šics
Predicting Scooping and Skipping in Solder Paste Printing for Reflow Soldering of SMT Devices
Authors:
S.H. Mannan
,
N.N. Ekere
,
E.K. Lo
…
The MathSAT 4 SMT Solver
Authors:
R. BRUTTOMESSO
,
A. Cimatti
,
A. Franzen
…
See all similar
Cited by
4
Translating Alloy Specifications to UML Class Diagrams Annotated with OCL
Authors:
Ana Garis
,
Alcino Cunha
,
Daniel Riesco
A Proof Assistant for Alloy Specifications
Authors:
Mattias Ulbrich
,
Ulrich Geilmann
,
Aboubakr Achraf El Ghazi
…
First-Order Transitive Closure Axiomatization via Iterative Invariant Injections
Authors:
Aboubakr Achraf El Ghazi
,
Mana Taghdiri
,
Mihai Herda
See all cited by