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
36
views
15
references
Top references
cited by
3
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
4,161
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings
SAFARI: SMT-Based Abstraction for Arrays with Interpolants
other
Author(s):
Francesco Alberti
,
Roberto Bruttomesso
,
Silvio Ghilardi
,
Silvio Ranise
,
Natasha Sharygina
Publication date
(Print):
2012
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
Value-based Healthcare
Most cited references
15
Record
: found
Abstract
: not found
Book Chapter
: not found
Counterexample-Guided Abstraction Refinement
Edmund Clarke
,
Orna Grumberg
,
Somesh Jha
…
(2000)
0
comments
Cited
157
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Lazy Abstraction with Interpolants
Kenneth McMillan
(2006)
0
comments
Cited
79
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Article
: not found
The software model checker Blast
Dirk Beyer
,
Thomas Henzinger
,
Ranjit Jhala
…
(2007)
0
comments
Cited
58
times
– based on
0
reviews
Review now
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2012
Pages
: 679-685
DOI:
10.1007/978-3-642-31424-7_49
SO-VID:
dc170ccf-3028-44bf-aab0-c087b62d936b
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
Synthesis and Some of Its Challenges
pp. 2
Model Checking Cell Biology
pp. 3
Synthesizing Programs with Constraint Solvers
pp. 4
IC3 and beyond: Incremental, Inductive Verification
pp. 5
Formal Verification of Genetic Circuits
pp. 6
From C to Infinity and Back: Unbounded Auto-active Verification with VCC
pp. 7
Deterministic Automata for the (F,G)-Fragment of LTL
pp. 23
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
pp. 39
ACTL ∩ LTL Synthesis
pp. 55
Learning Boolean Functions Incrementally
pp. 71
Interpolants as Classifiers
pp. 88
Termination Analysis with Algorithmic Learning
pp. 105
Automated Termination Proofs for Java Programs with Cyclic Data
pp. 123
Proving Termination of Probabilistic Programs Using Patterns
pp. 139
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
pp. 155
Diagnosing Abstraction Failure for Separation Logic–Based Analyses
pp. 174
A Method for Symbolic Computation of Abstract Operations
pp. 193
Leveraging Interpolant Strength in Model Checking
pp. 210
Detecting Fair Non-termination in Multithreaded Programs
pp. 227
Lock Removal for Concurrent Trace Programs
pp. 243
How to Prove Algorithms Linearisable
pp. 260
Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
pp. 277
Software Model Checking via IC3
pp. 294
Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
pp. 310
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
pp. 327
Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
pp. 343
Timed Relational Abstractions for Sampled Data Control Systems
pp. 362
Approximately Bisimilar Symbolic Models for Digital Control Systems
pp. 378
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
pp. 394
Minimum Satisfying Assignments for SMT
pp. 410
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
pp. 427
A Solver for Reachability Modulo Theories
pp. 444
On Decidability of Prebisimulation for Timed Automata
pp. 462
Exercises in Nonstandard Static Analysis of Hybrid Systems
pp. 479
A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
pp. 495
An Axiomatic Memory Model for POWER Multiprocessors
pp. 513
nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
pp. 532
Incremental, Inductive CTL Model Checking
pp. 548
Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
pp. 564
Automatic Quantification of Cache Side-Channels
pp. 581
Secure Programming via Visibly Pushdown Safety Games
pp. 599
Alternate and Learn: Finding Witnesses without Looking All over
pp. 616
A Complete Method for Symmetry Reduction in Safety Verification
pp. 634
Synthesizing Number Transformations from Input-Output Examples
pp. 652
Acacia+, a Tool for LTL Synthesis
pp. 658
MGSyn: Automatic Synthesis for Industrial Automation
pp. 665
OpenNWA: A Nested-Word Automaton Library
pp. 672
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
pp. 679
SAFARI: SMT-Based Abstraction for Arrays with Interpolants
pp. 686
Bma: Visual Tool for Modeling and Analyzing Biological Networks
pp. 693
APEX: An Analyzer for Open Probabilistic Programs
pp. 699
Recent Developments in FDR
pp. 705
A Model Checker for Hierarchical Probabilistic Real-Time Systems
pp. 712
SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
pp. 718
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems
pp. 725
HybridSAL Relational Abstracter
pp. 732
Euler: A System for Numerical Optimization of Programs
pp. 738
SPT: Storyboard Programming Tool
pp. 744
CSolve: Verifying C with Liquid Types
pp. 751
passert: A Tool for Debugging Parallel Programs
pp. 758
TRACER: A Symbolic Execution Tool for Verification
pp. 767
Joogie: Infeasible Code Detection for Java
pp. 774
Hector: An Equivalence Checker for a Higher-Order Fragment of ML
pp. 781
Resource Aware ML
Similar content
4,161
Automated Process Planning Based on a Semantic Capability Model and SMT
Authors:
Aljosha Köcher
,
Luis Miguel Vieira da Silva
,
Alexander Fay
A report of Bilharziella polonica cercariae in Knowsley Safari, Prescot, United Kingdom, with notes on other trematodes implicated in human cercarial dermatitis.
Authors:
A Juhász
,
S E J Barlow
,
H Williams
…
Language Modeling, Lexical Translation, Reordering: The Training Process of NMT through the Lens of Classical SMT
Authors:
Elena Voita
,
Rico Sennrich
,
Ivan Titov
See all similar
Cited by
3
From Invariant Checking to Invariant Inference Using Randomized Search
Authors:
Rahul Sharma
,
Alex Aiken
Dependent Array Type Inference from Tests
Authors:
He Zhu
,
Aditya V. Nori
,
Suresh Jagannathan
Verification of Imperative Programs by Constraint Logic Program Transformation
Authors:
Emanuele De Angelis
,
Fabio Fioravanti
,
Alberto Pettorossi
…
See all cited by