Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Computer Aided Verification [[electronic resource] ] : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / / edited by Aarti Gupta, Sharad Malik
| Computer Aided Verification [[electronic resource] ] : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / / edited by Aarti Gupta, Sharad Malik |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (XVII, 558 p.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer systems Computer science Software engineering Machine theory Artificial intelligence Programming Techniques Computer System Implementation Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence |
| ISBN | 3-540-70545-7 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Singularity: Designing Better Software (Invited Talk) -- Coping with Outside-the-Box Attacks -- Invited Tutorials -- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) -- Theorem Proving for Verification (Invited Tutorial) -- Tutorial on Separation Logic (Invited Tutorial) -- Abstract Interpretation with Applications to Timing Validation -- Session 1: Concurrency -- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis -- Monitoring Atomicity in Concurrent Programs -- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings -- A Hybrid Type System for Lock-Freedom of Mobile Processes -- Session 2: Memory Consistency -- Implied Set Closure and Its Application to Memory Consistency Verification -- Effective Program Verification for Relaxed Memory Models -- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses -- Session 3: Abstraction/Refinement -- Automated Assume-Guarantee Reasoning by Abstraction Refinement -- Local Proofs for Linear-Time Properties of Concurrent Programs -- Probabilistic CEGAR -- Session 4: Hybrid Systems -- Computing Differential Invariants of Hybrid Systems as Fixedpoints -- Constraint-Based Approach for Analysis of Hybrid Systems -- Session 5: Tools – Dynamic Verification -- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems -- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement -- Session 6: Modeling and Specification Formalisms -- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems -- Conflict-Tolerant Features -- Ranking Automata and Games for Prioritized Requirements -- Session 7: Decision Procedures -- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations -- Linear Arithmetic with Stars -- Inferring Congruence Equations Using SAT -- Session 8: Tools – Decision Procedures -- The Barcelogic SMT Solver -- The MathSAT 4 SMT Solver -- CSIsat: Interpolation for LA+EUF -- Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B -- Session 9: Program Verification -- Heap Assumptions on Demand -- Proving Conditional Termination -- Monotonic Abstraction for Programs with Dynamic Memory Heaps -- Enhancing Program Verification with Lemmas -- Session 10: Program and Shape Analysis -- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis -- Scalable Shape Analysis for Systems Code -- Thread Quantification for Concurrent Shape Analysis -- Session 11: Tools – Security and Program Analysis -- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols -- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis -- Jakstab: A Static Analysis Platform for Binaries -- THOR: A Tool for Reasoning about Shape and Arithmetic -- Session 12: Hardware Verification I -- Functional Verification of Power Gated Designs by Compositional Reasoning -- A Practical Approach to Word Level Model Checking of Industrial Netlists -- Session 13: Hardware Verification II -- Validating High-Level Synthesis -- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths -- Application of Formal Word-Level Analysis to Constrained Random Simulation -- Session 14: Model Checking -- Producing Short Counterexamples Using “Crucial Events” -- Discriminative Model Checking -- Session 15: Space Efficient Algorithms -- Correcting a Space-Efficient Simulation Algorithm -- Semi-external LTL Model Checking -- Session 16: Tools – Model Checking -- QMC: A Model Checker for Quantum Systems -- T(O)RMC: A Tool for (?)-Regular Model Checking -- Faster Than Uppaal?. |
| Record Nr. | UNISA-996466098703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer aided verification : 20th international conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008 : proceedings / / Aarti Gupta, Sharad Malik (eds.)
| Computer aided verification : 20th international conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008 : proceedings / / Aarti Gupta, Sharad Malik (eds.) |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2008 |
| Descrizione fisica | 1 online resource (XVII, 558 p.) |
| Disciplina | 005.11 |
| Altri autori (Persone) |
GuptaAarti
MalikSharad |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico |
Computer software - Verification
Integrated circuits - Verification |
| ISBN | 3-540-70545-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Singularity: Designing Better Software (Invited Talk) -- Coping with Outside-the-Box Attacks -- Invited Tutorials -- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) -- Theorem Proving for Verification (Invited Tutorial) -- Tutorial on Separation Logic (Invited Tutorial) -- Abstract Interpretation with Applications to Timing Validation -- Session 1: Concurrency -- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis -- Monitoring Atomicity in Concurrent Programs -- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings -- A Hybrid Type System for Lock-Freedom of Mobile Processes -- Session 2: Memory Consistency -- Implied Set Closure and Its Application to Memory Consistency Verification -- Effective Program Verification for Relaxed Memory Models -- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses -- Session 3: Abstraction/Refinement -- Automated Assume-Guarantee Reasoning by Abstraction Refinement -- Local Proofs for Linear-Time Properties of Concurrent Programs -- Probabilistic CEGAR -- Session 4: Hybrid Systems -- Computing Differential Invariants of Hybrid Systems as Fixedpoints -- Constraint-Based Approach for Analysis of Hybrid Systems -- Session 5: Tools – Dynamic Verification -- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems -- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement -- Session 6: Modeling and Specification Formalisms -- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems -- Conflict-Tolerant Features -- Ranking Automata and Games for Prioritized Requirements -- Session 7: Decision Procedures -- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations -- Linear Arithmetic with Stars -- Inferring Congruence Equations Using SAT -- Session 8: Tools – Decision Procedures -- The Barcelogic SMT Solver -- The MathSAT 4 SMT Solver -- CSIsat: Interpolation for LA+EUF -- Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B -- Session 9: Program Verification -- Heap Assumptions on Demand -- Proving Conditional Termination -- Monotonic Abstraction for Programs with Dynamic Memory Heaps -- Enhancing Program Verification with Lemmas -- Session 10: Program and Shape Analysis -- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis -- Scalable Shape Analysis for Systems Code -- Thread Quantification for Concurrent Shape Analysis -- Session 11: Tools – Security and Program Analysis -- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols -- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis -- Jakstab: A Static Analysis Platform for Binaries -- THOR: A Tool for Reasoning about Shape and Arithmetic -- Session 12: Hardware Verification I -- Functional Verification of Power Gated Designs by Compositional Reasoning -- A Practical Approach to Word Level Model Checking of Industrial Netlists -- Session 13: Hardware Verification II -- Validating High-Level Synthesis -- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths -- Application of Formal Word-Level Analysis to Constrained Random Simulation -- Session 14: Model Checking -- Producing Short Counterexamples Using “Crucial Events” -- Discriminative Model Checking -- Session 15: Space Efficient Algorithms -- Correcting a Space-Efficient Simulation Algorithm -- Semi-external LTL Model Checking -- Session 16: Tools – Model Checking -- QMC: A Model Checker for Quantum Systems -- T(O)RMC: A Tool for (?)-Regular Model Checking -- Faster Than Uppaal?. |
| Altri titoli varianti | CAV 2008 |
| Record Nr. | UNINA-9910483216903321 |
| Berlin, : Springer, 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||