Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
40
views
12
references
Top references
cited by
9
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
6,300
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
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems
other
Author(s):
Sylvain Conchon
,
Amit Goel
,
Sava Krstić
,
Alain Mebsout
,
Fatiha Zaïdi
Publication date
(Print):
2012
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Further versions
open (via free pdf)
Powered by
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
Model Reduction of Parametrized Systems 2015
Most cited references
12
Record
: found
Abstract
: not found
Book Chapter
: not found
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions
Randal E. Bryant
,
Shuvendu K. Lahiri
,
Sanjit Seshia
(2002)
0
comments
Cited
17
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
MCMT: A Model Checker Modulo Theories
Silvio Ghilardi
,
Silvio Ranise
(2010)
0
comments
Cited
14
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Towards SMT Model Checking of Array-Based Systems
Silvio Ghilardi
,
Enrica Nicolini
,
Silvio Ranise
…
(2008)
0
comments
Cited
11
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2012
Pages
: 718-724
DOI:
10.1007/978-3-642-31424-7_55
SO-VID:
c923b02c-5bcb-46de-adb2-0dfab7e1a7c9
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
6,300
Preference of loose housed dairy cows for two different cubicle floor coverings
Authors:
P. JENSEN
,
B. Recén
,
I. Ekesbo
…
A note on management practices and cubicle refusal in dairy cows
Authors:
JM O’Connell
,
PS Giller
,
WJ Meaney
The significance of cubicles for the behaviour of dairy cows
Authors:
H Hopster
,
H.K. Wierenga
See all similar
Cited by
9
Decidability of Parameterized Verification
Authors:
Igor Konnov
,
Sasha Rubin
,
Roderick Bloem
…
A Non-linear Arithmetic Procedure for Control-Command Software Verification
Authors:
Pierre Roux
,
Mohamed Iguernlala
,
Sylvain Conchon
Formal Specification and Verification of Dynamic Parametrized Architectures
Authors:
Alessandro Cimatti
,
Ivan Stojic
,
Stefano Tonetta
See all cited by