Verification, model checking, and abstract interpretation : 10th international conference, VMCAI 2009, Savannah, GA, USA, January 18 - 20, 2009 ; proceedings / / Neil D. Jones, Markus Muller-Olm (eds.)

• Pubblicazione: New York, NY ; ; Berlin ; ; Heidelberg, : Springer, c2009
• Edizione: 1st ed. 2009.
• Descrizione fisica: 1 online resource (XI, 381 p.)
• Disciplina: 005.11
• Soggetto topico: Mathematical optimization; Programming (Mathematics)
• Altri autori: JonesNeil D Muller-OlmMarkus
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di contenuto: Invited Talks -- Model Checking: Progress and Problems -- Model Checking Concurrent Programs -- Thread-Modular Shape Analysis -- Invited Tutorials -- Advances in Program Termination and Liveness -- Verification of Security Protocols -- Submitted Papers -- Towards Automatic Stability Analysis for Rely-Guarantee Proofs -- Mostly-Functional Behavior in Java Programs -- The Higher-Order Aggregate Update Problem -- An Abort-Aware Model of Transactional Programming -- Model-Checking the Linux Virtual File System -- LTL Generalized Model Checking Revisited -- Monitoring the Full Range of ?-Regular Properties of Stochastic Systems -- Constraint-Based Invariant Inference over Predicate Abstraction -- Reducing Behavioural to Structural Properties of Programs with Procedures -- Query-Driven Program Testing -- Average-Price-per-Reward Games on Hybrid Automata with Strong Resets -- Abstraction Refinement for Probabilistic Software -- Finding Concurrency-Related Bugs Using Random Isolation -- An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries -- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities -- Deciding Extensions of the Theories of Vectors and Bags -- A Posteriori Soundness for Non-deterministic Abstract Interpretations -- An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking -- A Scalable Memory Model for Low-Level Code -- Synthesizing Switching Logic Using Constraint Solving -- Extending Symmetry Reduction by Exploiting System Architecture -- Shape-Value Abstraction for Verifying Linearizability -- Mixed Transition Systems Revisited -- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking.
• Sommario/riassunto: The book constitutes the refereed proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2009, held in Savannah, GA, USA, in January 2009 - co-located with POPL 2009, the 36th Annual Symposium on Principles of Programming Languages. The 24 revised full papers presented together with 3 invited talks and 2 invited tutorials were carefully reviewed and selected from 72 submissions. The papers address all current issues from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine the three areas.
• Titolo autorizzato: Verification, model checking, and abstract interpretation
• ISBN: 3-540-93900-8
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910484590103321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science ; ; 5403.