LEADER 06043nam 22007935 450 001 996465588703316 005 20200703031408.0 010 $a1-280-38754-8 010 $a9786613565464 010 $a3-642-13977-9 024 7 $a10.1007/978-3-642-13977-2 035 $a(CKB)2670000000028979 035 $a(SSID)ssj0000446824 035 $a(PQKBManifestationID)11314932 035 $a(PQKBTitleCode)TC0000446824 035 $a(PQKBWorkID)10504352 035 $a(PQKB)10525198 035 $a(DE-He213)978-3-642-13977-2 035 $a(MiAaPQ)EBC3065452 035 $a(PPN)149064217 035 $a(EXLCZ)992670000000028979 100 $a20100629d2010 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTests and Proofs$b[electronic resource] $e4th International Conference, TAP 2010, Málaga, Spain, July 1-2, 2010, Proceedings /$fedited by Gordon Fraser, Angelo Gargantini 205 $a1st ed. 2010. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010. 215 $a1 online resource (174 p. 60 illus.) 225 1 $aProgramming and Software Engineering ;$v6143 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-13976-0 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- How Tests and Proofs Impede One Another: The Need for Always-On Static and Dynamic Feedback -- Myths in Software Engineering: From the Other Side -- Specifications from Testing -- QuickSpec: Guessing Formal Specifications Using Testing -- Testing Proofs -- Testing First-Order Logic Axioms in Program Verification -- Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases -- Proof Process Evaluation with Mutation Analysis -- Test Generation Using Proof Techniques -- Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay -- DyGen: Automatic Generation of High-Coverage Tests via Mining Gigabytes of Dynamic Traces -- Combining Static Analysis and Test Generation for C Program Debugging -- Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding -- Theorem Proving and Testing -- Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions -- Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications -- Abstraction -- Syntactic Abstraction of B Models to Generate Tests -- Building a Test-Ready Abstraction of a Behavioral Model Using CLP. 330 $aThis volume contains the proceedings of TAP 2010, the 4th International C- ference on Tests and Proofs held during July 1?2 in M´ alaga, Spain as part of TOOLS Federated Conferences. TAP 2010wasthe fourth event of an ongoingseriesof conferencesdevoted to the convergence of proofs and tests. In the past, proving and testing were seen as very di?erent and even competing techniques. Proving people would say: If correctness is proved, what do we need tests for? Testers, on the other hand, would claim that proving is too limited in applicability and testing is the only truepathtocorrectness. Ofcourse,bothhaveapoint,buttoquoteEdBrinksma from his 2009 keynote at the Dutch Testing Day and Testcom/FATES: ?Who would want to ?y in an airplane with software proved correct, but not tested?? Indeed, the true power lies in the combination of both approaches. Today, m- ern test systems rely on techniques deeply rooted in formal proof techniques, and testing techniques make it possible to apply proof techniques where there was no possibility previously. At a time when even mainstream software engineering conferences start f- turing papers with both ?testing? and ?proving?in their titles, we are clearly on the verge of a new age where testing and proving are not competing but ?nally accepted as complementary techniques. Albeit, we are not quite there yet, and so the TAP conferences aim to provide a forum for researchers working on the converging topics and to raise general awareness of this convergence. 410 0$aProgramming and Software Engineering ;$v6143 606 $aComputer programming 606 $aSoftware engineering 606 $aProgramming languages (Electronic computers) 606 $aComputer logic 606 $aMathematical logic 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 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 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 607 $aMa?laga <2010>$2swd 615 0$aComputer programming. 615 0$aSoftware engineering. 615 0$aProgramming languages (Electronic computers). 615 0$aComputer logic. 615 0$aMathematical logic. 615 14$aProgramming Techniques. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aMathematical Logic and Formal Languages. 676 $a005.14 702 $aFraser$b Gordon$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aGargantini$b Angelo$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTAP 2010 906 $aBOOK 912 $a996465588703316 996 $aTests and Proofs$92841686 997 $aUNISA