Hardware and Software: Verification and Testing
10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings
Herausgegeben:Yahav, Eran
Hardware and Software: Verification and Testing
10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings
Herausgegeben:Yahav, Eran
- Broschiertes Buch
- Merkliste
- Auf die Merkliste
- Bewerten Bewerten
- Teilen
- Produkt teilen
- Produkterinnerung
- Produkterinnerung
This book constitutes the refereed proceedings of the 10th International Haifa Verification Conference, HVC 2014, held in Haifa, Israel, in November 2014.The 17 revised full papers and 4 short papers presented were carefully reviewed and selected from 43 submissions. The papers cover a wide range of topics in the sub-fields of testing and verification applicable to software, hardware, and complex hybrid systems.
Andere Kunden interessierten sich auch für
- Hardware and Software: Verification and Testing37,99 €
- NASA Formal Methods37,99 €
- Automated Technology for Verification and Analysis37,99 €
- Software Engineering and Formal Methods37,99 €
- Verified Software: Theories, Tools and Experiments36,99 €
- Software Engineering and Formal Methods37,99 €
- Formal Methods for Industrial Critical Systems36,99 €
-
-
-
This book constitutes the refereed proceedings of the 10th International Haifa Verification Conference, HVC 2014, held in Haifa, Israel, in November 2014.The 17 revised full papers and 4 short papers presented were carefully reviewed and selected from 43 submissions. The papers cover a wide range of topics in the sub-fields of testing and verification applicable to software, hardware, and complex hybrid systems.
Produktdetails
- Produktdetails
- Lecture Notes in Computer Science 8855
- Verlag: Springer / Springer International Publishing / Springer, Berlin
- Artikelnr. des Verlages: 978-3-319-13337-9
- 2014
- Seitenzahl: 320
- Erscheinungstermin: 6. November 2014
- Englisch
- Abmessung: 235mm x 155mm x 18mm
- Gewicht: 488g
- ISBN-13: 9783319133379
- ISBN-10: 3319133373
- Artikelnr.: 41615472
- Lecture Notes in Computer Science 8855
- Verlag: Springer / Springer International Publishing / Springer, Berlin
- Artikelnr. des Verlages: 978-3-319-13337-9
- 2014
- Seitenzahl: 320
- Erscheinungstermin: 6. November 2014
- Englisch
- Abmessung: 235mm x 155mm x 18mm
- Gewicht: 488g
- ISBN-13: 9783319133379
- ISBN-10: 3319133373
- Artikelnr.: 41615472
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.- Enhancing Scenario Quality Using Quasi-Events.- Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems.- DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification.- Generating Modulo-2 Linear Invariants for Hardware Model Checking.- Suraq - A Controller Synthesis Tool Using Uninterpreted Functions.- Synthesizing Finite-State Protocols from Scenarios and Requirements.- Automatic Error Localization for Software Using Deductive Verification.- Generating JML Specifications from Alloy Expressions.- Assume-Guarantee Abstraction Refinement Meets Hybrid Systems.- Handling TSO in Mechanized Linearizability Proofs.- Partial Quantifier Elimination.- Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study.- A Framework to Synergize Partial Order Reduction with State Interpolation.- Reduction of Resolution Refutations and Interpolants via Subsumption.- Read, Write and Copy Dependencies for Symbolic Model Checking.- Efficient Combinatorial Test Generation Based on Multivalued Decision Diagrams.- Formal Verification of Secure User Mode Device Execution with DMA.- Supervisory Control of Discrete-Event Systems via IC3.- Partial-Order Reduction for Multi-core LTL Model Checking.- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution.
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.- Enhancing Scenario Quality Using Quasi-Events.- Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems.- DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification.- Generating Modulo-2 Linear Invariants for Hardware Model Checking.- Suraq — A Controller Synthesis Tool Using Uninterpreted Functions.- Synthesizing Finite-State Protocols from Scenarios and Requirements.- Automatic Error Localization for Software Using Deductive Verification.- Generating JML Specifications from Alloy Expressions.- Assume-Guarantee Abstraction Refinement Meets Hybrid Systems.- Handling TSO in Mechanized Linearizability Proofs.- Partial Quantifier Elimination.- Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study.- A Framework to Synergize Partial Order Reduction with State Interpolation.- Reduction of Resolution Refutations and Interpolants via Subsumption.- Read, Write and Copy Dependencies for Symbolic Model Checking.- Efficient Combinatorial Test Generation Based on Multivalued Decision Diagrams.- Formal Verification of Secure User Mode Device Execution with DMA.- Supervisory Control of Discrete-Event Systems via IC3.- Partial-Order Reduction for Multi-core LTL Model Checking.- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution.
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.- Enhancing Scenario Quality Using Quasi-Events.- Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems.- DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification.- Generating Modulo-2 Linear Invariants for Hardware Model Checking.- Suraq - A Controller Synthesis Tool Using Uninterpreted Functions.- Synthesizing Finite-State Protocols from Scenarios and Requirements.- Automatic Error Localization for Software Using Deductive Verification.- Generating JML Specifications from Alloy Expressions.- Assume-Guarantee Abstraction Refinement Meets Hybrid Systems.- Handling TSO in Mechanized Linearizability Proofs.- Partial Quantifier Elimination.- Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study.- A Framework to Synergize Partial Order Reduction with State Interpolation.- Reduction of Resolution Refutations and Interpolants via Subsumption.- Read, Write and Copy Dependencies for Symbolic Model Checking.- Efficient Combinatorial Test Generation Based on Multivalued Decision Diagrams.- Formal Verification of Secure User Mode Device Execution with DMA.- Supervisory Control of Discrete-Event Systems via IC3.- Partial-Order Reduction for Multi-core LTL Model Checking.- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution.
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.- Enhancing Scenario Quality Using Quasi-Events.- Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems.- DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification.- Generating Modulo-2 Linear Invariants for Hardware Model Checking.- Suraq — A Controller Synthesis Tool Using Uninterpreted Functions.- Synthesizing Finite-State Protocols from Scenarios and Requirements.- Automatic Error Localization for Software Using Deductive Verification.- Generating JML Specifications from Alloy Expressions.- Assume-Guarantee Abstraction Refinement Meets Hybrid Systems.- Handling TSO in Mechanized Linearizability Proofs.- Partial Quantifier Elimination.- Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study.- A Framework to Synergize Partial Order Reduction with State Interpolation.- Reduction of Resolution Refutations and Interpolants via Subsumption.- Read, Write and Copy Dependencies for Symbolic Model Checking.- Efficient Combinatorial Test Generation Based on Multivalued Decision Diagrams.- Formal Verification of Secure User Mode Device Execution with DMA.- Supervisory Control of Discrete-Event Systems via IC3.- Partial-Order Reduction for Multi-core LTL Model Checking.- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution.