LEADER 04117oam 2200697 450 001 9910483947603321 005 20210602143438.0 010 $a3-540-77966-3 024 7 $a10.1007/978-3-540-77966-7 035 $a(CKB)1000000000490627 035 $a(SSID)ssj0000318069 035 $a(PQKBManifestationID)11267551 035 $a(PQKBTitleCode)TC0000318069 035 $a(PQKBWorkID)10308268 035 $a(PQKB)10006271 035 $a(DE-He213)978-3-540-77966-7 035 $a(MiAaPQ)EBC3062200 035 $a(MiAaPQ)EBC336938 035 $a(MiAaPQ)EBC6426088 035 $a(Au-PeEL)EBL336938 035 $a(CaONFJC)MIL134299 035 $a(OCoLC)233973884 035 $a(PPN)123743591 035 $a(EXLCZ)991000000000490627 100 $a20210602d2008 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aHardware and software, verification and testing $ethird International Haifa Verification Conference, HVC 2007, Haifa, Israel, October 23-25, 2007 : proceedings /$fKaren Yorav (editor) 205 $a1st ed. 2008. 210 1$aBerlin, Germany :$cSpringer,$d[2008] 210 4$d©2008 215 $a1 online resource (XII, 267 p.) 225 1 $aProgramming and Software Engineering ;$v4899 300 $aIncludes index. 311 $a3-540-77964-7 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Simulation vs. Formal: Absorb What Is Useful; Reject What Is Useless -- Scaling Commercial Verification to Larger Systems -- From Hardware Verification to Software Verification: Re-use and Re-learn -- Where Do Bugs Come from? -- HVC Award -- Symbolic Execution and Model Checking for Testing -- Hardware Verification -- On the Characterization of Until as a Fixed Point Under Clocked Semantics -- Reactivity in SystemC Transaction-Level Models -- Model Checking -- Verifying Parametrised Hardware Designs Via Counter Automata -- How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison -- Dynamic Hardware Verification -- Constraint Patterns and Search Procedures for CP-Based Random Test Generation -- Using Virtual Coverage to Hit Hard-To-Reach Events -- Merging Formal and Testing -- Test Case Generation for Ultimately Periodic Paths -- Dynamic Testing Via Automata Learning -- Formal Verification for Software -- On the Architecture of System Verification Environments -- Exploiting Shared Structure in Software Verification Conditions -- Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code -- A Complete Bounded Model Checking Algorithm for Pushdown Systems -- Software Testing -- Locating Regression Bugs -- The Advantages of Post-Link Code Coverage -- GenUTest: A Unit Test and Mock Aspect Generation Tool. 330 $aThis book constitutes the thoroughly refereed post-workshop proceedings of the Third International Haifa Verification Conference, HVC 2007, held in Haifa, Israel, in October 2007. The 15 revised full papers presented together with 4 invited lectures were carefully reviewed and selected from 32 submissions. The papers are organized in topical tracks on hardware verification, model checking, dynamic hardware verification, merging formal and testing, formal verification for software and software testing. 410 0$aProgramming and Software Engineering ;$v4899 606 $aComputer input-output equipment$vCongresses 606 $aSoftware architecture$vCongresses 606 $aComputer programs$xVerification$vCongresses 610 1 $aVerification 610 1 $aHardware 610 1 $aSoftware 615 0$aComputer input-output equipment 615 0$aSoftware architecture 615 0$aComputer programs$xVerification 676 $a004.24 702 $aYorav$b Karen 712 12$aInternational Haifa Verification Conference 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bUtOrBLW 906 $aBOOK 912 $a9910483947603321 996 $aHardware and Software, Verification and Testing$9772242 997 $aUNINA