Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings

Front Cover
Ganesh Gopalakrishnan, Shaz Qadeer
Springer Science & Business Media, Jul 5, 2011 - Computers - 763 pages

This book constitutes the refereed proceedings of the 23rd International Conference on Computer Aided Verification, CAV 2011, held in Snowbird, UT, USA, in July 2011.

The 35 revised full papers presented together with 20 tool papers were carefully reviewed and selected from 161 submissions. The papers are organized in topical sections on the following workshops: 4th International Workshop on Numerical Software Verification (NSV 2011), 10th International Workshop on Parallel and Distributed Methods in Verifications (PDMC 2011), 4th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 2011), Frontiers in Analog Circuit Synthesis and Verification (FAC 2011), International Workshop on Satisfiability Modulo Theories, including SMTCOMP (SMT 2011), 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), Formal Methods for Robotics and Automation (FM-R 2011), and Practical Synthesis for Concurrent Systems (PSY 2011).

 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

A String Solver for Testing Analysis and Vulnerability Detection
1
Using Types for Software Verification
20
SMTBased Modular Analysis of Sequential Systems Code
21
Logic and Compositional Verification of Hybrid Systems
28
Using Coverage to Deploy Formal Verification in a Simulation World
44
Stability in Weak Memory Models
50
Verification of Certifying Computations
67
Parameter Identification for Markov Models of Biochemical Reactions
83
A ConstraintBased Verifier for Multithreaded Programs
412
Interactive Synthesis of Code Snippets
418
Forest Automata for Verification of Heap Manipulation
424
Synthesizing CyberPhysical Architectural Models with RealTime Constraints
441
μZ An Efficient Engine for Fixed Points with Constraints
457
A Binary Analysis Platform
463
Verifying Functional Programs Using Abstract Interpreters
470
A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations
486

Getting Rid of StoreBuffers in TSO Analysis
99
Malware Analysis with Tree Automata Inference
116
StateEventBased LTL Model Checking under Parametric Generalized Fairness
132
Resolution Proofs and Skolem Functions in QBF Evaluation and Applications
149
The BINCOA Framework for Binary Code Analysis
165
CVC4
171
Memory Safety for SystemsLevel Code
178
A Tool for Configurable Software Verification
184
Existential Quantification as Incremental SAT
191
E∆cient Analysis of Probabilistic Programs with an Unbounded Counter
208
Model Checking Algorithms for CTMDPs
225
Quantitative Synthesis for Concurrent Programs
243
Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Buchi Objectives
260
Smoothing a Program Soundly and Robustly
277
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification
293
KRATOS A Software Model Checker for SystemC
310
Efficient Scenario Verification for Hybrid Automata
317
Temporal Property Verification as a Program Analysis Task
333
Time for Statistical Model Checking of RealTime Systems
349
SymmetryAware Predicate Abstraction for SharedVariable Concurrent Programs
356
A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
372
Scalable Verification of Hybrid Systems
379
From Cardiac Cells to Genetic Regulatory Networks
396
Assisting Fault Localization in ANSIC Programs
504
Synthesis of Distributed Control through Knowledge Accumulation
510
Language Equivalence for Probabilistic Automata
526
Formalization and Automated Verification of RESTful Behavior
541
Linear Completeness Thresholds for Bounded Model Checking
557
InterpolationBased Software Verification with Wolverine
573
Synthesizing Biological Theories
579
Verification of Probabilistic RealTime Systems
585
Program Analysis for Overlaid Data Structures
592
A Symbolic Execution and Automatic Test Generation Tool for C++ Programs
609
Fully Symbolic Model Checking for Timed Automata
616
Complete Formal Hardware Verification of Interfaces for a FlexRayLike Bus
633
Verification and Synthesis for Timed Automata
649
A Fixpoint Calculator for Quantified Bag Constraints
656
Analyzing Unsynthesizable Specifications for HighLevel Robot Behavior Using LTLMoP
663
Practical LowEffort Equivalence Verification of Real Code
669
Relational Abstractions for Continuous and Hybrid Systems
686
Simplifying Loop Invariant Generation Using Splitter Predicates
703
Monitorability of Stochastic Dynamical Systems
720
EqualityBased Translation Validator for LLVM
737
Model Checking Recursive Programs with Numeric Data Types
743
Author Index
760
Copyright

Common terms and phrases