Cantitate/Preț
Produs
Total produse
Vezi coșul
Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings de Tayssir Touili

Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings: Lecture Notes in Computer Science, cartea 6174

Editat de Tayssir Touili, Byron Cook, Paul Jackson
en Limba Engleză Paperback – 30 iun 2010

Descoperim în acest volum resurse fundamentale pentru analiza formală asistată de calculator, începând cu prezentarea unor instrumente esențiale precum ABC — un instrument de verificare de calibru industrial — și platforma de cercetare Static Driver Verifier. Computer Aided Verification nu se rezumă la teorie pură, ci pune la dispoziția cercetătorilor 17 lucrări dedicate instrumentelor software, care detaliază implementarea algoritmilor de verificare în scenarii reale. Structura volumului urmărește o progresie logică de la fundamentele teoretice ale logicii temporale de ordinul întâi până la aplicații critice în securitatea codului moștenit și managementul memoriei în algoritmi concurenți.

Observăm o organizare riguroasă pe secțiuni tematice care acoperă spectrul verificării sistemelor hardware și software. Găsim aici secțiuni dedicate verificării programelor care manipulează liste cu date nelimitate, sintezei invarianților și testării concurenței prin analiză simbolică. Un punct distinctiv al acestui volum, publicat în seria Lecture Notes in Computer Science, este accentul pus pe „verificarea la nivel de bază”, oferind tutoriale despre analiza și verificarea codului mașină. De asemenea, parcurgem soluții pentru proceduri de decizie și raționament compozițional, elemente vitale pentru scalabilitatea metodelor de verificare în sisteme complexe. Editorii Tayssir Touili, Byron Cook și Paul Jackson au selectat contribuții care fac puntea între fluxurile de lucru academice și cerințele de fiabilitate din industrie, abordând inclusiv fluxul informațional cantitativ și sistemele hibride.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 63925 lei

Preț vechi: 79907 lei
-20%

Puncte Express: 959

Carte disponibilă

Livrare economică 27 mai-10 iunie

 Adaugă în coș

Wish list
Gift list
Am citit!
Adaugă în listă

Specificații

ISBN-13: 9783642142949
ISBN-10: 364214294X
Pagini: 676
Ilustrații: XVI, 676 p. 169 illus.
Dimensiuni: 11 x 93 x 28 mm
Greutate: 0.95 kg
Ediția:2010
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Theoretical Computer Science and General Issues

Locul publicării:Berlin, Heidelberg, Germany

Public țintă

Research

De ce să citești această carte

Pentru cercetătorii și inginerii din domeniul metodelor formale, această carte oferă acces la tehnici avansate de model checking și verificare software. Cititorul câștigă o înțelegere profundă a modului în care pot fi aplicate riguros instrumentele automate pentru a garanta corectitudinea sistemelor hardware și a codului de nivel scăzut, beneficiind de tutoriale practice și studii de caz pe sisteme de securitate.

Cuprins

Invited Talks.- Policy Monitoring in First-Order Temporal Logic.- Retrofitting Legacy Code for Security.- Quantitative Information Flow: From Theory to Practice?.- Memory Management in Concurrent Algorithms.- Invited Tutorials.- ABC: An Academic Industrial-Strength Verification Tool.- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code.- Constraint Solving for Program Verification: Theory and Practice by Example.- Session 1. Software Model Checking.- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data.- Termination Analysis with Compositional Transition Invariants.- Lazy Annotation for Program Testing and Verification.- The Static Driver Verifier Research Platform.- Dsolve: Safety Verification via Liquid Types.- Contessa: Concurrency Testing Augmented with Symbolic Analysis.- Session 2. Model Checking and Automata.- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing.- Efficient Emptiness Check for Timed Büchi Automata.- Session 3. Tools.- Merit: An Interpolating Model-Checker.- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems.- Jtlv: A Framework for Developing Verification Algorithms.- Petruchio: From Dynamic Networks to Nets.- Session 4. Counter and Hybrid Systems Verification.- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems.- Safety Verification for Probabilistic Hybrid Systems.- A Logical Product Approach to Zonotope Intersection.- Fast Acceleration of Ultimately Periodic Relations.- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.- Session 5. Memory Consistency.- Fences in Weak Memory Models.- Generating Litmus Tests for Contrasting Memory Consistency Models.- Session 6. Verification of Hardware and Low Level Code.- Directed Proof Generation for Machine Code.- Verifying Low-Level Implementations of High-Level Datatypes.- Automatic Generation of Inductive Invariants from High-LevelMicroarchitectural Models of Communication Fabrics.- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification.- Session 7. Tools.- LTSmin: Distributed and Symbolic Reachability.- libalf: The Automata Learning Framework.- Session 8. Synthesis.- Symbolic Bounded Synthesis.- Measuring and Synthesizing Systems in Probabilistic Environments.- Achieving Distributed Control through Model Checking.- Robustness in the Presence of Liveness.- RATSY – A New Requirements Analysis Tool with Synthesis.- Comfusy: A Tool for Complete Functional Synthesis.- Session 9. Concurrent Program Verification I.- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs.- Automatically Proving Linearizability.- Model Checking of Linearizability of Concurrent List Implementations.- Local Verification of Global Invariants in Concurrent Programs.- Abstract Analysis of Symbolic Executions.- Session 10. Compositional Reasoning.- Automated Assume-Guarantee Reasoning through Implicit Learning.- Learning Component Interfaces with May and Must Abstractions.- A Dash of Fairness for Compositional Reasoning.- SPLIT: A Compositional LTL Verifier.- Session 11. Tools.- A Model Checker for AADL.- PESSOA: A Tool for Embedded Controller Synthesis.- Session 12. Decision Procedures.- On Array Theory of Bounded Elements.- Quantifier Elimination by Lazy Model Enumeration.- Session 13. Concurrent Program Verification II.- Bounded Underapproximations.- Global Reachability in Bounded Phase Multi-stack Pushdown Systems.- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces.- Dynamic Cutoff Detection in Parameterized Concurrent Programs.- Session 14. Tools.- PARAM: A Model Checker for Parametric Markov Models.- Gist: A Solver for Probabilistic Games.- A NuSMV Extension for Graded-CTL Model Checking.

Caracteristici

State-of-the-art research Fast-track conference proceedings Unique visibility

Descriere

This book constitutes the refereed proceedings of the 22nd International Conference on Computer Aided Verification, CAV 2010, held in Edinburgh, UK, in July 2010 as part of the Federated Logic Conference, FLoC 2010. The 34 revised full papers presented together with 17 tool papers, 4 invited talks and 3 invited tutorials were carefully reviewed and selected from 101 regular paper and 44 tool paper submissions. The papers are dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for hardware and software systems. They are organized in topical sections on software model checking; model checking and automata; tools; counter and hybrid systems verification; memory consistency; verification of hardware and low level code; synthesis; concurrent program verification; compositional reasoning; and decision procedures.