Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, ProceedingsThis 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
| 1 | |
| 20 | |
| 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 |
| 760 | |
Common terms and phrases
abstract interpretation algorithm analysis approach approximation assertion automata automaton behavior benchmarks Boolean bound Büchi automaton checker clause clock components compute concurrent programs consider constraints data structures defined denote disjunctive dynamic encoding equivalent error evaluation example execution finite formal formal verification formula function given graph Hampi Heidelberg hybrid systems hypergraphs implementation initial input integer invariants Isabelle/HOL iteration language Lemma linear LLVM LNCS logic loop malware Markov Markov chain MDPs memory method model checking node operations optimal output parameters path performance pointer predicate abstraction probabilistic problem procedure proof properties quantified reachability refinement relation satisfies scheduler semantics sequence simulation Skolem functions specification Springer SQL injection Streett automaton symbolic steps synchronization SystemC techniques Theorem thread tool transition transition relation tree uc-klee variables vector verification
Bibliographic information
| Title | Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings Volume 6806 of Theoretical Computer Science and General Issues |
| Editors | Ganesh Gopalakrishnan, Shaz Qadeer |
| Edition | illustrated |
| Publisher | Springer, 2011 |
| ISBN | 3642221106, 9783642221101 |
| Length | 763 pages |
| Subjects | › › Computers / Artificial Intelligence / General Computers / Information Technology Computers / Languages / General Computers / Programming / General Computers / Software Development & Engineering / General Mathematics / Discrete Mathematics Mathematics / Logic |
| Export Citation | BiBTeX EndNote RefMan |