LEADER 06601nam 22006975 450 001 996465300703316 005 20200630230431.0 010 $a3-642-34188-8 024 7 $a10.1007/978-3-642-34188-5 035 $a(CKB)3280000000002205 035 $a(SSID)ssj0000788962 035 $a(PQKBManifestationID)11492113 035 $a(PQKBTitleCode)TC0000788962 035 $a(PQKBWorkID)10722589 035 $a(PQKB)10281422 035 $a(DE-He213)978-3-642-34188-5 035 $a(MiAaPQ)EBC3070275 035 $a(PPN)168326353 035 $a(EXLCZ)993280000000002205 100 $a20121026d2012 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aHardware and Software: Verification and Testing$b[electronic resource] $e7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers /$fedited by Kerstin Eder, Joćo Louren?o, Onn Shehory 205 $a1st ed. 2012. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2012. 215 $a1 online resource (XII, 263 p. 95 illus.) 225 1 $aProgramming and Software Engineering ;$v7261 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-34187-X 327 $aPreprocessing and Inprocessing Techniques in SAT -- Pioneering the Future of Verification: A Spiral of Technological and Business Innovation -- Automated Detection and Repair of Concurrency Bugs -- Verification Challenges of Workload Optimized Hardware Systems -- Synthesis with Clairvoyance -- Generalized Reactivity(1) Synthesis without a Monolithic Strategy -- IIS-Guided DFS for Efficient Bounded Reachability Analysis of Linear Hybrid Automata -- Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.Implicative Simultaneous Satisfiability and Applications -- Liveness vs Safety ? A Practical Viewpoint -- Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search -- SAM: Self-adaptive Dynamic Analysis for Multithreaded Programs -- Concurrent Small Progress Measures -- Specification and Quantitative Analysis of Probabilistic Cloud Deployment Patterns -- Interpolation-Based Function Summaries in Bounded Model Checking -- Can File Level Characteristics Help Identify System Level Fault-Proneness -- Reverse Coverage Analysis -- Symbolic Testing of OpenCL Code -- Dynamic Test Data Generation for Data Intensive Applications -- Injecting Floating-Point Testing Knowledge into Test Generators -- Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE -- HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware -- On-Line Detection and Prediction of Temporal Patterns -- Function Summaries in Software Upgrade Checking -- The Rabin Index of Parity Games -- Using Computational Biology Methods to Improve Post-silicon Microprocessor Testing. -- ioneering the Future of Verification: A Spiral of Technological and Business Innovation -- Automated Detection and Repair of Concurrency Bugs -- Verification Challenges of Workload Optimized Hardware Systems -- Synthesis with Clairvoyance -- Generalized Reactivity(1) Synthesis without a Monolithic Strategy -- IIS-Guided DFS for Efficient Bounded Reachability Analysis of Linear Hybrid Automata -- Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.Implicative Simultaneous Satisfiability and Applications -- Liveness vs Safety ? A Practical Viewpoint -- Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search -- SAM: Self-adaptive Dynamic Analysis for Multithreaded Programs -- Concurrent Small Progress Measures -- Specification and Quantitative Analysis of Probabilistic Cloud Deployment Patterns -- Interpolation-Based Function Summaries in Bounded Model Checking -- Can File Level Characteristics Help Identify System Level Fault-Proneness -- Reverse Coverage Analysis -- Symbolic Testing of OpenCL Code -- Dynamic Test Data Generation for Data Intensive Applications -- Injecting Floating-Point Testing Knowledge into Test Generators -- Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE -- HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware -- On-Line Detection and Prediction of Temporal Patterns -- Function Summaries in Software Upgrade Checking -- The Rabin Index of Parity Games -- Using Computational Biology Methods to Improve Post-silicon Microprocessor Testing. 330 $aThis book constitutes the thoroughly refereed post-conference proceedings of the 7th International Haifa Verification Conference, HVC 2011, held in Haifa, Israel in December 2011. The 15 revised full papers presented together with 3 tool papers and 4 posters were carefully reviewed and selected from 43 submissions. The papers are organized in topical sections on synthesis, formal verification, software quality, testing and coverage, experience and tools, and posters- student event. 410 0$aProgramming and Software Engineering ;$v7261 606 $aSoftware engineering 606 $aProgramming languages (Electronic computers) 606 $aComputer logic 606 $aArtificial intelligence 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 608 $aConference proceedings.$2fast 615 0$aSoftware engineering. 615 0$aProgramming languages (Electronic computers). 615 0$aComputer logic. 615 0$aArtificial intelligence. 615 14$aSoftware Engineering. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aLogics and Meanings of Programs. 615 24$aArtificial Intelligence. 676 $a005.14 702 $aEder$b Kerstin$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aLouren?o$b Joćo$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aShehory$b Onn$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Haifa Verification Conference 906 $aBOOK 912 $a996465300703316 996 $aHardware and Software, Verification and Testing$9772242 997 $aUNISA