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
44
views
18
references
Top references
cited by
11
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,434
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
TRACER: A Symbolic Execution Tool for Verification
other
Author(s):
Joxan Jaffar
,
Vijayaraghavan Murali
,
Jorge A. Navas
,
Andrew E. Santosa
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
Primate Tool Use
Most cited references
18
Record
: found
Abstract
: not found
Article
: not found
Symbolic execution and program testing
James C King
(1976)
0
comments
Cited
164
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs
George C. Necula
,
Scott McPeak
,
Shree P. Rahul
…
(2002)
0
comments
Cited
55
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Article
: not found
An interpolating theorem prover
K.L. McMillan
(2005)
0
comments
Cited
43
times
– based on
0
reviews
Review now
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2012
Pages
: 758-766
DOI:
10.1007/978-3-642-31424-7_61
SO-VID:
d3bdd163-3a37-49cf-bbfe-4ea29be2eecd
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
1,434
Eunomia: Enabling User-specified Fine-Grained Search in Symbolically Executing WebAssembly Binaries
Authors:
Ningyu He
,
Zhehao Zhao
,
Jikai Wang
…
Decomposition of a symbolic element over a countable amenable group into blocks approximating ergodic measures
Authors:
Tomasz Downarowicz
,
Mateusz Więcek
Probabilistic Verification of Structural Stability Design Procedures
Authors:
Zdeněk Kala
See all similar
Cited by
11
The SeaHorn Verification Framework
Authors:
Arie Gurfinkel
,
Temesghen Kahsai
,
Anvesh Komuravelli
…
On Solving Universally Quantified Horn Clauses
Authors:
Nikolaj Bjørner
,
Ken McMillan
,
Andrey Rybalchenko
A Survey of Symbolic Execution Techniques
Authors:
Roberto Baldoni
,
Emilio Coppa
,
Daniele D’elia
…
See all cited by