top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
Computer Aided Verification [[electronic resource] ] : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings / / edited by Ganesh Gopalakrishnan, Shaz Qadeer
Computer Aided Verification [[electronic resource] ] : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings / / edited by Ganesh Gopalakrishnan, Shaz Qadeer
Edizione [1st ed. 2011.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011
Descrizione fisica 1 online resource (XV, 763 p. 180 illus., 46 illus. in color.)
Disciplina 005.1015113
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer science
Software engineering
Compilers (Computer programs)
Machine theory
Computer programming
Artificial intelligence
Computer Science Logic and Foundations of Programming
Software Engineering
Compilers and Interpreters
Formal Languages and Automata Theory
Programming Techniques
Artificial Intelligence
ISBN 3-642-22110-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISA-996465714203316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / / edited by Tayssir Touili, Byron Cook, Paul Jackson
Computer Aided Verification [[electronic resource] ] : 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / / edited by Tayssir Touili, Byron Cook, Paul Jackson
Edizione [1st ed. 2010.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Descrizione fisica 1 online resource (XVI, 676 p. 169 illus.)
Disciplina 005.1015113
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer science
Software engineering
Compilers (Computer programs)
Machine theory
Artificial intelligence
Computer networks
Computer Science Logic and Foundations of Programming
Software Engineering
Compilers and Interpreters
Formal Languages and Automata Theory
Artificial Intelligence
Computer Communication Networks
ISBN 1-280-38785-8
9786613565778
3-642-14295-8
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto 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-Level Microarchitectural 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.
Record Nr. UNISA-996465781203316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / / edited by Tayssir Touili, Byron Cook, Paul Jackson
Computer Aided Verification [[electronic resource] ] : 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / / edited by Tayssir Touili, Byron Cook, Paul Jackson
Edizione [1st ed. 2010.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Descrizione fisica 1 online resource (XVI, 676 p. 169 illus.)
Disciplina 005.1015113
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer science
Software engineering
Compilers (Computer programs)
Machine theory
Artificial intelligence
Computer networks
Computer Science Logic and Foundations of Programming
Software Engineering
Compilers and Interpreters
Formal Languages and Automata Theory
Artificial Intelligence
Computer Communication Networks
ISBN 1-280-38785-8
9786613565778
3-642-14295-8
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto 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-Level Microarchitectural 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.
Record Nr. UNINA-9910482958903321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
Edizione [1st ed. 2009.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009
Descrizione fisica 1 online resource (XV, 722 p.)
Disciplina 005.11
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer programming
Computer systems
Software engineering
Computer science
Machine theory
Programming Techniques
Computer System Implementation
Software Engineering
Computer Science Logic and Foundations of Programming
Formal Languages and Automata Theory
ISBN 3-642-02658-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Tutorials -- Transactional Memory: Glimmer of a Theory -- Mixed-Signal System Verification: A High-Speed Link Example -- Modelling Epigenetic Information Maintenance: A Kappa Tutorial -- Component-Based Construction of Real-Time Systems in BIP -- Invited Talks -- Models and Proofs of Protocol Security: A Progress Report -- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? -- SPEED: Symbolic Complexity Bound Analysis -- Regression Verification: Proving the Equivalence of Similar Programs -- Regular Papers -- Symbolic Counter Abstraction for Concurrent Software -- Priority Scheduling of Distributed Systems Based on Model Checking -- Explaining Counterexamples Using Causality -- Size-Change Termination, Monotonicity Constraints and Ranking Functions -- Linear Functional Fixed-points -- Better Quality in Synthesis through Quantitative Objectives -- Automatic Verification of Integer Array Programs -- Automated Analysis of Java Methods for Confidentiality -- Requirements Validation for Hybrid Systems -- Towards Performance Prediction of Compositional Models in Industrial GALS Designs -- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion -- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers -- Meta-analysis for Atomicity Violations under Nested Locking -- An Antichain Algorithm for LTL Realizability -- On Extending Bounded Proofs to Inductive Proofs -- Games through Nested Fixpoints -- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories -- Software Transactional Memory on Relaxed Memory Models -- Sliding Window Abstraction for Infinite Markov Chains -- Centaur Technology Media Unit Verification -- Incremental Instance Generation in Local Reasoning -- Quantifier Elimination via Functional Composition -- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique -- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation -- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models -- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints -- Generalizing DPLL to Richer Logics -- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability -- Intra-module Inference -- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers -- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints -- Reachability Analysis of Hybrid Systems Using Support Functions -- Reducing Test Inputs Using Information Partitions -- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure -- Cardinality Abstraction for Declarative Networking Applications -- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences -- Tool Papers -- D-Finder: A Tool for Compositional Deadlock Detection and Verification -- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment -- The Zonotope Abstract Domain Taylor1+ -- InvGen: An Efficient Invariant Generator -- INFAMY: An Infinite-State Markov Model Checker -- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep -- Homer: A Higher-Order Observational Equivalence Model checkER -- Apron: A Library of Numerical Abstract Domains for Static Analysis -- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic -- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs -- MCMAS: A Model Checker for the Verification of Multi-Agent Systems -- TASS: Timing Analyzer of Scenario-Based Specifications -- Translation Validation: From Simulink to C -- VS3: SMT Solvers for Program Verification -- PAT: Towards Flexible Verification under Fairness -- A Concurrent Portfolio Approach to SMT Solving.
Record Nr. UNISA-996465423003316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
Edizione [1st ed. 2009.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009
Descrizione fisica 1 online resource (XV, 722 p.)
Disciplina 005.11
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer programming
Computer systems
Software engineering
Computer science
Machine theory
Programming Techniques
Computer System Implementation
Software Engineering
Computer Science Logic and Foundations of Programming
Formal Languages and Automata Theory
ISBN 3-642-02658-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Tutorials -- Transactional Memory: Glimmer of a Theory -- Mixed-Signal System Verification: A High-Speed Link Example -- Modelling Epigenetic Information Maintenance: A Kappa Tutorial -- Component-Based Construction of Real-Time Systems in BIP -- Invited Talks -- Models and Proofs of Protocol Security: A Progress Report -- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? -- SPEED: Symbolic Complexity Bound Analysis -- Regression Verification: Proving the Equivalence of Similar Programs -- Regular Papers -- Symbolic Counter Abstraction for Concurrent Software -- Priority Scheduling of Distributed Systems Based on Model Checking -- Explaining Counterexamples Using Causality -- Size-Change Termination, Monotonicity Constraints and Ranking Functions -- Linear Functional Fixed-points -- Better Quality in Synthesis through Quantitative Objectives -- Automatic Verification of Integer Array Programs -- Automated Analysis of Java Methods for Confidentiality -- Requirements Validation for Hybrid Systems -- Towards Performance Prediction of Compositional Models in Industrial GALS Designs -- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion -- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers -- Meta-analysis for Atomicity Violations under Nested Locking -- An Antichain Algorithm for LTL Realizability -- On Extending Bounded Proofs to Inductive Proofs -- Games through Nested Fixpoints -- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories -- Software Transactional Memory on Relaxed Memory Models -- Sliding Window Abstraction for Infinite Markov Chains -- Centaur Technology Media Unit Verification -- Incremental Instance Generation in Local Reasoning -- Quantifier Elimination via Functional Composition -- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique -- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation -- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models -- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints -- Generalizing DPLL to Richer Logics -- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability -- Intra-module Inference -- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers -- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints -- Reachability Analysis of Hybrid Systems Using Support Functions -- Reducing Test Inputs Using Information Partitions -- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure -- Cardinality Abstraction for Declarative Networking Applications -- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences -- Tool Papers -- D-Finder: A Tool for Compositional Deadlock Detection and Verification -- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment -- The Zonotope Abstract Domain Taylor1+ -- InvGen: An Efficient Invariant Generator -- INFAMY: An Infinite-State Markov Model Checker -- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep -- Homer: A Higher-Order Observational Equivalence Model checkER -- Apron: A Library of Numerical Abstract Domains for Static Analysis -- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic -- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs -- MCMAS: A Model Checker for the Verification of Multi-Agent Systems -- TASS: Timing Analyzer of Scenario-Based Specifications -- Translation Validation: From Simulink to C -- VS3: SMT Solvers for Program Verification -- PAT: Towards Flexible Verification under Fairness -- A Concurrent Portfolio Approach to SMT Solving.
Record Nr. UNINA-9910483039603321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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. UNINA-9910483216903321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings / / edited by Werner Damm, Holger Hermanns
Computer Aided Verification [[electronic resource] ] : 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings / / edited by Werner Damm, Holger Hermanns
Edizione [1st ed. 2007.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007
Descrizione fisica 1 online resource (XV, 562 p.)
Disciplina 006.3
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer science
Software engineering
Machine theory
Artificial intelligence
Logic design
Theory of Computation
Computer Science Logic and Foundations of Programming
Software Engineering
Formal Languages and Automata Theory
Artificial Intelligence
Logic Design
ISBN 3-540-73368-X
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Automatically Proving Program Termination -- A Mathematical Approach to RTL Verification -- Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? -- Invited Tutorials -- Algorithms for Interface Synthesis -- A Tutorial on Satisfiability Modulo Theories -- A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java -- Verification of Hybrid Systems -- Session I: Compositionality -- SAT-Based Compositional Verification Using Lazy Learning -- Local Proofs for Global Safety Properties -- Session II: Verification Process -- Low-Level Library Analysis and Summarization -- Verification Across Intellectual Property Boundaries -- Session III: Timed Synthesis and Games -- On Synthesizing Controllers from Bounded-Response Properties -- An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games -- UPPAAL-Tiga: Time for Playing Games! -- The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems -- Session IV: Infinitive State Verification -- Systematic Acceleration in Regular Model Checking -- Parameterized Verification of Infinite-State Processes with Global Conditions -- Session V: Tool Environment -- CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes -- jMoped: A Test Environment for Java Programs -- Hector: Software Model Checking with Cooperating Analysis Plugins -- The Why/Krakatoa/Caduceus Platform for Deductive Program Verification -- Session VI: Shapes -- Shape Analysis for Composite Data Structures -- Array Abstractions from Proofs -- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures -- Revamping TVLA: Making Parametric Shape Analysis Competitive -- Session VII: Concurrent Program Verification -- Fast and Accurate Static Data-Race Detection for Concurrent Programs -- Parametric and Sliced Causality -- Spade: Verification of Multithreaded Dynamic and Recursive Programs -- Session VIII: Reactive Designs -- Anzu: A Tool for Property Synthesis -- RAT: A Tool for the Formal Analysis of Requirements -- Session IX: Parallelisation -- Parallelising Symbolic State-Space Generators -- I/O Efficient Accepting Cycle Detection -- Session X: Constraints and Decisions -- C32SAT: Checking C Expressions -- CVC3 -- BAT: The Bit-Level Analysis Tool -- LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals -- Session XI: Probabilistic Verification -- Three-Valued Abstraction for Continuous-Time Markov Chains -- Magnifying-Lens Abstraction for Markov Decision Processes -- Underapproximation for Model-Checking Based on Random Cryptographic Constructions -- Session XII: Abstraction -- Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra -- Structural Abstraction of Software Verification Conditions -- An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software -- Adaptive Symmetry Reduction -- Session XIII: Assume-Guarantee Reasoning -- From Liveness to Promptness -- Automated Assumption Generation for Compositional Verification -- Session XIV: Hybrid Systems -- Abstraction and Counterexample-Guided Construction of ?-Automata for Model Checking of Step-Discrete Linear Hybrid Models -- Test Coverage for Continuous and Hybrid Systems -- Hybrid Systems: From Verification to Falsification -- Session XV: Program Analysis -- Comparison Under Abstraction for Verifying Linearizability -- Leaping Loops in the Presence of Abstraction -- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis -- Session XVI: SAT and Decision Procedures -- A Decision Procedure for Bit-Vectors and Arrays -- Boolean Abstraction for Temporal Logic Satisfiability -- A Lazy and Layered SMT( ) Solver for Hard Industrial Verification Problems.
Record Nr. UNISA-996466098303316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings / / edited by Werner Damm, Holger Hermanns
Computer Aided Verification [[electronic resource] ] : 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings / / edited by Werner Damm, Holger Hermanns
Edizione [1st ed. 2007.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007
Descrizione fisica 1 online resource (XV, 562 p.)
Disciplina 006.3
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer science
Software engineering
Machine theory
Artificial intelligence
Logic design
Theory of Computation
Computer Science Logic and Foundations of Programming
Software Engineering
Formal Languages and Automata Theory
Artificial Intelligence
Logic Design
ISBN 3-540-73368-X
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Automatically Proving Program Termination -- A Mathematical Approach to RTL Verification -- Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? -- Invited Tutorials -- Algorithms for Interface Synthesis -- A Tutorial on Satisfiability Modulo Theories -- A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java -- Verification of Hybrid Systems -- Session I: Compositionality -- SAT-Based Compositional Verification Using Lazy Learning -- Local Proofs for Global Safety Properties -- Session II: Verification Process -- Low-Level Library Analysis and Summarization -- Verification Across Intellectual Property Boundaries -- Session III: Timed Synthesis and Games -- On Synthesizing Controllers from Bounded-Response Properties -- An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games -- UPPAAL-Tiga: Time for Playing Games! -- The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems -- Session IV: Infinitive State Verification -- Systematic Acceleration in Regular Model Checking -- Parameterized Verification of Infinite-State Processes with Global Conditions -- Session V: Tool Environment -- CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes -- jMoped: A Test Environment for Java Programs -- Hector: Software Model Checking with Cooperating Analysis Plugins -- The Why/Krakatoa/Caduceus Platform for Deductive Program Verification -- Session VI: Shapes -- Shape Analysis for Composite Data Structures -- Array Abstractions from Proofs -- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures -- Revamping TVLA: Making Parametric Shape Analysis Competitive -- Session VII: Concurrent Program Verification -- Fast and Accurate Static Data-Race Detection for Concurrent Programs -- Parametric and Sliced Causality -- Spade: Verification of Multithreaded Dynamic and Recursive Programs -- Session VIII: Reactive Designs -- Anzu: A Tool for Property Synthesis -- RAT: A Tool for the Formal Analysis of Requirements -- Session IX: Parallelisation -- Parallelising Symbolic State-Space Generators -- I/O Efficient Accepting Cycle Detection -- Session X: Constraints and Decisions -- C32SAT: Checking C Expressions -- CVC3 -- BAT: The Bit-Level Analysis Tool -- LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals -- Session XI: Probabilistic Verification -- Three-Valued Abstraction for Continuous-Time Markov Chains -- Magnifying-Lens Abstraction for Markov Decision Processes -- Underapproximation for Model-Checking Based on Random Cryptographic Constructions -- Session XII: Abstraction -- Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra -- Structural Abstraction of Software Verification Conditions -- An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software -- Adaptive Symmetry Reduction -- Session XIII: Assume-Guarantee Reasoning -- From Liveness to Promptness -- Automated Assumption Generation for Compositional Verification -- Session XIV: Hybrid Systems -- Abstraction and Counterexample-Guided Construction of ?-Automata for Model Checking of Step-Discrete Linear Hybrid Models -- Test Coverage for Continuous and Hybrid Systems -- Hybrid Systems: From Verification to Falsification -- Session XV: Program Analysis -- Comparison Under Abstraction for Verifying Linearizability -- Leaping Loops in the Presence of Abstraction -- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis -- Session XVI: SAT and Decision Procedures -- A Decision Procedure for Bit-Vectors and Arrays -- Boolean Abstraction for Temporal Logic Satisfiability -- A Lazy and Layered SMT( ) Solver for Hard Industrial Verification Problems.
Record Nr. UNINA-9910484352003321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings / / edited by Thomas Ball, Robert B. Jones
Computer Aided Verification [[electronic resource] ] : 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings / / edited by Thomas Ball, Robert B. Jones
Edizione [1st ed. 2006.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006
Descrizione fisica 1 online resource (XV, 564 p.)
Disciplina 004.24
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer science
Software engineering
Machine theory
Artificial intelligence
Logic design
Theory of Computation
Computer Science Logic and Foundations of Programming
Software Engineering
Formal Languages and Automata Theory
Artificial Intelligence
Logic Design
ISBN 3-540-37411-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Formal Specifications on Industrial-Strength Code—From Myth to Reality -- I Think I Voted: E-Voting vs. Democracy -- Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs -- The Ideal of Verified Software -- Session 1. Automata -- Antichains: A New Algorithm for Checking Universality of Finite Automata -- Safraless Compositional Synthesis -- Minimizing Generalized Büchi Automata -- Session 2. Tools Papers -- Ticc: A Tool for Interface Compatibility and Composition -- FAST Extended Release -- Session 3. Arithmetic -- Don’t Care Words with an Application to the Automata-Based Approach for Real Addition -- A Fast Linear-Arithmetic Solver for DPLL(T) -- Session 4. SAT and Bounded Model Checking -- Bounded Model Checking for Weak Alternating Büchi Automata -- Deriving Small Unsatisfiable Cores with Dominators -- Session 5. Abstraction/Refinement -- Lazy Abstraction with Interpolants -- Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop -- Counterexamples with Loops for Predicate Abstraction -- Session 6. Tools Papers -- cascade: C Assertion Checker and Deductive Engine -- Yasm: A Software Model-Checker for Verification and Refutation -- Session 7. Symbolic Trajectory Evaluation -- SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation -- Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation -- Session 8. Property Specification and Verification -- Some Complexity Results for SystemVerilog Assertions -- Check It Out: On the Efficient Formal Verification of Live Sequence Charts -- Session 9. Time -- Symmetry Reduction for Probabilistic Model Checking -- Communicating Timed Automata: The More Synchronous, the More Difficult to Verify -- Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis -- Session 10. Tools Papers -- DiVinE – A Tool for Distributed Verification -- EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation -- Session 11. Concurrency -- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions -- Model Checking Multithreaded Programs with Asynchronous Atomic Methods -- Causal Atomicity -- Session 12. Trees, Pushdown Systems and Boolean Programs -- Languages of Nested Trees -- Improving Pushdown System Model Checking -- Repair of Boolean Programs with an Application to C -- Session 13. Termination -- Termination of Integer Linear Programs -- Automatic Termination Proofs for Programs with Shape-Shifting Heaps -- Termination Analysis with Calling Context Graphs -- Session 14. Tools Papers -- Terminator: Beyond Safety -- CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools -- Session 15. Abstract Interpretation -- SMT Techniques for Fast Predicate Abstraction -- The Power of Hybrid Acceleration -- Lookahead Widening -- Session 16. Tools Papers -- The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover -- LEVER: A Tool for Learning Based Verification -- Session 17. Memory Consistency -- Formal Verification of a Lazy Concurrent List-Based Set Algorithm -- Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study -- Fast and Generalized Polynomial Time Memory Consistency Verification -- Session 18. Shape Analysis -- Programs with Lists Are Counter Automata -- Lazy Shape Analysis -- Abstraction for Shape Analysis with Fast and Precise Transformers.
Record Nr. UNISA-996465602503316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui