000 06332nam a22006015i 4500
001 978-3-642-16901-4
003 DE-He213
005 20240730193118.0
007 cr nn 008mamaa
008 101108s2010 gw | s |||| 0|eng d
020 _a9783642169014
_9978-3-642-16901-4
024 7 _a10.1007/978-3-642-16901-4
_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] :
_b12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings /
_cedited by Jin Song Dong, Huibiao Zhu.
250 _a1st ed. 2010.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2010.
300 _aXIV, 712 p. 202 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 ;
_v6447
505 0 _aInvited Talks -- Fostering Proof Scores in CafeOBJ -- Exploiting Partial Success in Applying Automated Formal Methods -- Multicore Embedded Systems: The Timing Problem and Possible Solutions -- Theorem Proving and Decision Procedures -- Applying PVS Background Theories and Proof Strategies in Invariant Based Programming -- Proof Obligation Generation and Discharging for Recursive Definitions in VDM -- Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq -- Decision Procedures for the Temporal Verification of Concurrent Lists -- An Improved Decision Procedure for Propositional Projection Temporal Logic -- Web Services and Workflow -- A Semantic Model for Service Composition with Coordination Time Delays -- Compensable WorkFlow Nets -- Automatically Testing Web Services Choreography with Assertions -- Applying Ordinary Differential Equations to the Performance Analysis of Service Composition -- Verification I -- Verifying Heap-Manipulating Programs with Unknown Procedure Calls -- API Conformance Verification for Java Programs -- Assume-Guarantee Reasoning with Local Specifications -- Automating Coinduction with Case Analysis -- Applications of Formal Methods -- Enhanced Semantic Access to Formal Software Models -- Making Pattern- and Model-Based Software Development More Rigorous -- Practical Parameterised Session Types -- A Formal Verification Study on the Rotterdam Storm Surge Barrier -- Verification II -- Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems -- Automated Multiparameterised Verification by Cut-Offs -- Automating Cut-off for Multi-parameterized Systems -- Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors -- Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP -- Probability and Concurrency -- Model Checking Hierarchical Probabilistic Systems -- Trace-Driven Verification of Multithreaded Programs -- Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network -- Reasoning about Safety and Progress Using Contracts -- Program Analysis -- Abstract Program Slicing: From Theory towards an Implementation -- Loop Invariant Synthesis in a Combined Domain -- Software Metrics in Static Program Analysis -- A Combination of Forward and Backward Reachability Analysis Methods -- Model Checking -- Model Checking a Model Checker: A Code Contract Combined Approach -- On Symmetries and Spotlights - Verifying Parameterised Systems -- A Methodology for Automatic Diagnosability Analysis -- Making the Right Cut in Model Checking Data-Intensive Timed Systems -- Comparison of Model Checking Tools for Information Systems -- Object Orientation and Model Driven Engineering -- A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model -- Model-Driven Protocol Design Based on Component Oriented Modeling -- Laws of Pattern Composition -- Dynamic Resource Reallocation between Deployment Components -- Specification and Verification -- A Pattern System to Support Refining Informal Ideas into Formal Expressions -- Specification Translation of State Machines from Equational Theories into Rewrite Theories -- Alternating Interval Based Temporal Logics.
520 _aThis book constitutes the refereed proceedings of the 12th International Conference on Formal Engineering Methods, ICFEM 2010, held in Shanghai, China, November 2010. The 42 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 114 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on theorem proving and decision procedures, web services and workflow, verification, applications of formal methods, probability and concurrency, program analysis, model checking, object orientation and mod el driven engineering, as well as specification and verification.
650 0 _aSoftware engineering.
_94138
650 0 _aComputer networks .
_931572
650 0 _aCompilers (Computer programs).
_93350
650 0 _aComputer programming.
_94169
650 0 _aAlgorithms.
_93390
650 1 4 _aSoftware Engineering.
_94138
650 2 4 _aComputer Communication Networks.
_9152488
650 2 4 _aCompilers and Interpreters.
_931853
650 2 4 _aProgramming Techniques.
_9152489
650 2 4 _aAlgorithms.
_93390
700 1 _aDong, Jin Song.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9152490
700 1 _aZhu, Huibiao.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9152491
710 2 _aSpringerLink (Online service)
_9152492
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783642169007
776 0 8 _iPrinted edition:
_z9783642169021
830 0 _aProgramming and Software Engineering,
_x2945-9168 ;
_v6447
_9152493
856 4 0 _uhttps://doi.org/10.1007/978-3-642-16901-4
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c94599
_d94599