LEADER 06481nam 22007935 450 001 996465668603316 005 20240313002207.0 010 $a3-642-34281-7 024 7 $a10.1007/978-3-642-34281-3 035 $a(CKB)3280000000002210 035 $a(SSID)ssj0000788959 035 $a(PQKBManifestationID)11449502 035 $a(PQKBTitleCode)TC0000788959 035 $a(PQKBWorkID)10722038 035 $a(PQKB)10793306 035 $a(DE-He213)978-3-642-34281-3 035 $a(MiAaPQ)EBC3068792 035 $a(PPN)168326582 035 $a(EXLCZ)993280000000002210 100 $a20121029d2012 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFormal Methods and Software Engineering$b[electronic resource] $e14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012, Proceedings /$fedited by Toshiaki Aoki, Kenji Taguchi 205 $a1st ed. 2012. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2012. 215 $a1 online resource (XIV, 512 p. 131 illus.) 225 1 $aProgramming and Software Engineering ;$v7635 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-34280-9 320 $aIncludes bibliographical references and index. 327 $aToward Practical Application of Formal Methods in Software Lifecycle Processes -- Formal Methods in the Aerospace Industry: Follow the Money -- Applying Term Rewriting to Speech Recognition of Numbers -- Variable Permissions for Concurrency Verification -- A Concurrent Temporal Programming Model with Atomic Blocks -- A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs -- Towards a Formal Verification Methodology for Collective Robotic Systems -- Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS -- Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic -- Quantitative Program Dependence Graphs -- Quantitative Analysis of Information Flow Using Theorem Proving -- Modeling and Verification of Probabilistic Actor Systems Using pRebeca -- Modular Verification of OO Programs with Interfaces -- Separation Predicates: A Taste of Separation Logic in First-Order Logic -- The Confinement Problem in the Presence of Faults -- Verification of ATL Transformations Using Transformation Models and Model Finders -- Automatic Generation of Provably Correct Embedded Systems -- Complementary Methodologies for Developing Hybrid Systems with Event-B -- A Temporal Logic with Mean-Payoff Constraints -- Time Constraints with Temporal Logic Programming -- Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System -- Equational Abstraction Refinement for Certified Tree Regular Model Checking -- SMT-Based False Positive Elimination in Static Program Analysis -- Predicate Analysis with Block-Abstraction Memoization -- Heuristic-Guided Abstraction Refinement for Concurrent Systems -- More Anti-chain Based Refinement Checking -- An Analytical and Experimental Comparison of CSP Extensions and Tools -- Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization -- Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers -- State Space c-Reductions of Concurrent Systems in Rewriting Logic -- A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification -- ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications -- Demonic Testing of Concurrent Programs -- Towards Certified Runtime Verification. 330 $aThis book constitutes the refereed proceedings of the 14th International Conference on Formal Engineering Methods, ICFEM 2012, held in Kyoto, Japan, November 2012. The 31 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 85 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on concurrency, applications of formal methods to new areas, quantity and probability, formal verification, modeling and development methodology, temporal logics, abstraction and refinement, tools, as well as testing and runtime verification. 410 0$aProgramming and Software Engineering ;$v7635 606 $aSoftware engineering 606 $aComputer programming 606 $aProgramming languages (Electronic computers) 606 $aAlgorithms 606 $aMathematical logic 606 $aComputer communication systems 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aAlgorithm Analysis and Problem Complexity$3https://scigraph.springernature.com/ontologies/product-market-codes/I16021 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022 608 $aConference proceedings.$2fast 615 0$aSoftware engineering. 615 0$aComputer programming. 615 0$aProgramming languages (Electronic computers). 615 0$aAlgorithms. 615 0$aMathematical logic. 615 0$aComputer communication systems. 615 14$aSoftware Engineering. 615 24$aProgramming Techniques. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aAlgorithm Analysis and Problem Complexity. 615 24$aMathematical Logic and Formal Languages. 615 24$aComputer Communication Networks. 676 $a005.1 702 $aAoki$b Toshiaki$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aTaguchi$b Kenji$f1956-$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Formal Engineering Methods 906 $aBOOK 912 $a996465668603316 996 $aFormal Methods and Software Engineering$9771999 997 $aUNISA