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
8
views
12
references
Top references
cited by
2
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
2,267
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
Secure Programming via Visibly Pushdown Safety Games
other
Author(s):
William R. Harris
,
Somesh Jha
,
Thomas Reps
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
Smart Contracts Programming Languages
Most cited references
12
Record
: found
Abstract
: not found
Article
: not found
Certification of programs for secure information flow
Peter J. Denning
,
Dorothy Denning
(1977)
0
comments
Cited
68
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Conference Proceedings
: not found
Visibly pushdown languages
Rajeev Alur
,
P. Madhusudan
(2004)
0
comments
Cited
64
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Conference Proceedings
: not found
Control-flow integrity
Mihai Budiu
,
Martín Abadi
,
Jay Ligatti
…
(2005)
0
comments
Cited
59
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2012
Pages
: 581-598
DOI:
10.1007/978-3-642-31424-7_41
SO-VID:
89412183-d761-4e08-a096-089cb9d7513e
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
2,267
Sound and precise malware analysis for android via pushdown reachability and entry-point saturation
Authors:
Shuying Liang
,
Andrew W. Keep
,
Matthew Might
…
Reachability Analysis of Communicating Pushdown Systems
Authors:
Alexander Heußner
,
Jérôme Leroux
,
Anca Muscholl
…
A Note on Limited Pushdown Alphabets in Stateless Deterministic Pushdown Automata
Authors:
Tomáš Masopust
See all similar
Cited by
2
Secure Programming via Visibly Pushdown Safety Games
Authors:
William R. Harris
,
Somesh Jha
,
Thomas Reps
Hankel Matrices for Weighted Visibly Pushdown Automata
Authors:
Nadia Labai
,
Johann Makowsky
See all cited by