000 05481nam a22006255i 4500
001 978-3-642-34281-3
003 DE-He213
005 20240730193727.0
007 cr nn 008mamaa
008 121029s2012 gw | s |||| 0|eng d
020 _a9783642342813
_9978-3-642-34281-3
024 7 _a10.1007/978-3-642-34281-3
_2doi
050 4 _aQA76.758
072 7 _aUMZ
_2bicssc
072 7 _aCOM051230
_2bisacsh
072 7 _aUMZ
_2thema
082 0 4 _a005.1
_223
245 1 0 _aFormal Methods and Software Engineering
_h[electronic resource] :
_b14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012, Proceedings /
_cedited by Toshiaki Aoki, Kenji Taguchi.
250 _a1st ed. 2012.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2012.
300 _aXIV, 512 p. 131 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aProgramming and Software Engineering,
_x2945-9168 ;
_v7635
505 0 _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.
520 _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.
650 0 _aSoftware engineering.
_94138
650 0 _aComputer programming.
_94169
650 0 _aCompilers (Computer programs).
_93350
650 0 _aAlgorithms.
_93390
650 0 _aMachine theory.
_9154315
650 0 _aComputer networks .
_931572
650 1 4 _aSoftware Engineering.
_94138
650 2 4 _aProgramming Techniques.
_9154316
650 2 4 _aCompilers and Interpreters.
_931853
650 2 4 _aAlgorithms.
_93390
650 2 4 _aFormal Languages and Automata Theory.
_9154317
650 2 4 _aComputer Communication Networks.
_9154318
700 1 _aAoki, Toshiaki.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9154319
700 1 _aTaguchi, Kenji.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9154320
710 2 _aSpringerLink (Online service)
_9154321
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783642342806
776 0 8 _iPrinted edition:
_z9783642342820
830 0 _aProgramming and Software Engineering,
_x2945-9168 ;
_v7635
_9154322
856 4 0 _uhttps://doi.org/10.1007/978-3-642-34281-3
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c94837
_d94837