Ebook: Verification, Model Checking, and Abstract Interpretation: 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings
- Tags: Logics and Meanings of Programs, Software Engineering, Programming Languages Compilers Interpreters, Algorithm Analysis and Problem Complexity, Mathematical Logic and Formal Languages, Programming Techniques
- Series: Lecture Notes in Computer Science 6538
- Year: 2011
- Publisher: Springer-Verlag Berlin Heidelberg
- Edition: 1
- Language: English
- pdf
This book constitutes the refereed proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, held in Austin, TX, USA, in January 2011, co-located with the Symposium on Principles of Programming Languages, POPL 2011.
The 24 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 71 initial submissions. The papers showcases state-of-the-art research in areas such as verification, model checking, abstract interpretation and address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Further topics covered are static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization.
This book constitutes the refereed proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, held in Austin, TX, USA, in January 2011, co-located with the Symposium on Principles of Programming Languages, POPL 2011.
The 24 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 71 initial submissions. The papers showcases state-of-the-art research in areas such as verification, model checking, abstract interpretation and address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Further topics covered are static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization.
This book constitutes the refereed proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, held in Austin, TX, USA, in January 2011, co-located with the Symposium on Principles of Programming Languages, POPL 2011.
The 24 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 71 initial submissions. The papers showcases state-of-the-art research in areas such as verification, model checking, abstract interpretation and address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Further topics covered are static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization.
Content:
Front Matter....Pages -
Are Cells Asynchronous Circuits?....Pages 1-1
Formal Analysis of Message Passing....Pages 2-18
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation....Pages 19-22
Quality Engineering: Leveraging Heterogeneous Information....Pages 23-37
More Precise Yet Widely Applicable Cost Analysis....Pages 38-53
Refinement-Based CFG Reconstruction from Unstructured Programs....Pages 54-69
SAT-Based Model Checking without Unrolling....Pages 70-87
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic....Pages 88-102
Probabilistic B?chi Automata with Non-extremal Acceptance Thresholds....Pages 103-117
Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice....Pages 118-133
Proving Stabilization of Biological Systems....Pages 134-149
Precondition Inference from Intermittent Assertions and Application to Contracts on Collections....Pages 150-168
Strengthening Induction-Based Race Checking with Lightweight Static Analysis....Pages 169-183
Access Nets: Modeling Access to Physical Spaces....Pages 184-198
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation....Pages 199-213
Verifying Deadlock-Freedom of Communication Fabrics....Pages 214-231
Static Analysis of Finite Precision Computations....Pages 232-247
An Evaluation of Automata Algorithms for String Analysis....Pages 248-262
Automata Learning with Automated Alphabet Abstraction Refinement....Pages 263-277
Towards Complete Reasoning about Axiomatic Specifications....Pages 278-293
String Analysis as an Abstract Interpretation....Pages 294-308
ExplainHoudini: Making Houdini Inference Transparent....Pages 309-323
Abstract Probabilistic Automata....Pages 324-339
Distributed and Predictable Software Model Checking....Pages 340-355
Access Analysis-Based Tight Localization of Abstract Memories....Pages 356-370
Decision Procedures for Automating Termination Proofs....Pages 371-386
Collective Assertions....Pages 387-402
Sets with Cardinality Constraints in Satisfiability Modulo Theories....Pages 403-418
Back Matter....Pages -
This book constitutes the refereed proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, held in Austin, TX, USA, in January 2011, co-located with the Symposium on Principles of Programming Languages, POPL 2011.
The 24 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 71 initial submissions. The papers showcases state-of-the-art research in areas such as verification, model checking, abstract interpretation and address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Further topics covered are static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization.
Content:
Front Matter....Pages -
Are Cells Asynchronous Circuits?....Pages 1-1
Formal Analysis of Message Passing....Pages 2-18
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation....Pages 19-22
Quality Engineering: Leveraging Heterogeneous Information....Pages 23-37
More Precise Yet Widely Applicable Cost Analysis....Pages 38-53
Refinement-Based CFG Reconstruction from Unstructured Programs....Pages 54-69
SAT-Based Model Checking without Unrolling....Pages 70-87
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic....Pages 88-102
Probabilistic B?chi Automata with Non-extremal Acceptance Thresholds....Pages 103-117
Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice....Pages 118-133
Proving Stabilization of Biological Systems....Pages 134-149
Precondition Inference from Intermittent Assertions and Application to Contracts on Collections....Pages 150-168
Strengthening Induction-Based Race Checking with Lightweight Static Analysis....Pages 169-183
Access Nets: Modeling Access to Physical Spaces....Pages 184-198
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation....Pages 199-213
Verifying Deadlock-Freedom of Communication Fabrics....Pages 214-231
Static Analysis of Finite Precision Computations....Pages 232-247
An Evaluation of Automata Algorithms for String Analysis....Pages 248-262
Automata Learning with Automated Alphabet Abstraction Refinement....Pages 263-277
Towards Complete Reasoning about Axiomatic Specifications....Pages 278-293
String Analysis as an Abstract Interpretation....Pages 294-308
ExplainHoudini: Making Houdini Inference Transparent....Pages 309-323
Abstract Probabilistic Automata....Pages 324-339
Distributed and Predictable Software Model Checking....Pages 340-355
Access Analysis-Based Tight Localization of Abstract Memories....Pages 356-370
Decision Procedures for Automating Termination Proofs....Pages 371-386
Collective Assertions....Pages 387-402
Sets with Cardinality Constraints in Satisfiability Modulo Theories....Pages 403-418
Back Matter....Pages -
....