LEADER 01171nam a22002891i 4500 001 991004183479707536 005 20030131112238.0 008 020822s1969 it a||||||||||||||||ita 020 $a8839702407 035 $ab11932855-39ule_inst 035 $aARCHE-002267$9ExL 040 $aDip.to Filologia Ling. e Lett.$bita$cA.t.i. Arché s.c.r.l. Pandora Sicilia s.r.l. 082 04$a808.3 100 1 $aBianchini, Angela$0198246 245 13$aIl romanzo d'appendice /$cA. Bianchini 260 $aTorino :$bERI,$c[1969] 300 $a190 p. :$bill. ;$c21 cm 490 0 $aNuovi quaderni ;$v2 650 4$aRomanzo d'appendice 907 $a.b11932855$b28-04-17$c01-04-03 912 $a991004183479707536 945 $aLE008 FL.M. II C 65$g1$iLE008IFM-2921$lle008$o-$pE0.00$q-$rl$s- $t0$u0$v0$w0$x0$y.i12205710$z01-04-03 945 $aLE008 Cr E V 45$g2$i2008000208882$lle008$o-$pE0.00$q-$rl$s- $t0$u0$v0$w0$x0$y.i12205722$z01-04-03 945 $aLE008 FL.M. VI L 101$g3$iLE008A-03131$lle008$o-$pE0.00$q-$rl$s- $t0$u0$v0$w0$x0$y.i12205734$z01-04-03 996 $aRomanzo d'appendice$9167248 997 $aUNISALENTO 998 $ale008$b01-04-03$cm$da $e-$fita$git $h3$i3 LEADER 07141nam 22008295 450 001 9910483872003321 005 20251226202641.0 010 $a3-642-05089-1 024 7 $a10.1007/978-3-642-05089-3 035 $a(CKB)1000000000804425 035 $a(SSID)ssj0000355501 035 $a(PQKBManifestationID)11294242 035 $a(PQKBTitleCode)TC0000355501 035 $a(PQKBWorkID)10320431 035 $a(PQKB)11346413 035 $a(DE-He213)978-3-642-05089-3 035 $a(MiAaPQ)EBC3064748 035 $a(PPN)139962360 035 $a(EXLCZ)991000000000804425 100 $a20100301d2009 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFM 2009: Formal Methods $eSecond World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings /$fedited by Ana Cavalcanti, Dennis Dams 205 $a1st ed. 2009. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009. 215 $a1 online resource (XVII, 820 p.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v5850 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-642-05088-3 320 $aIncludes bibliographical references and index. 327 $aInvited Papers -- Formal Methods for Privacy -- What Can Formal Methods Bring to Systems Biology? -- Guess and Verify ? Back to the Future -- Verification, Testing and Statistics -- Security, Probability and Nearly Fair Coins in the Cryptographers? Café -- Model Checking I -- Recursive Abstractions for Parameterized Systems -- Abstract Model Checking without Computing the Abstraction -- Three-Valued Spotlight Abstractions -- Fair Model Checking with Process Counter Abstraction -- Compositionality -- Systematic Development of Trustworthy Component Systems -- Partial Order Reductions Using Compositional Confluence Detection -- A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition -- Verification -- Abstract Specification of the UBIFS File System for Flash Memory -- Inferring Mealy Machines -- Formal Management of CAD/CAM Processes -- Concurrency -- Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way -- Symbolic Predictive Analysis for Concurrent Programs -- On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study -- Refinement -- Sums and Lovers: Case Studies in Security, Compositionality and Refinement -- Iterative Refinement of Reverse-Engineered Models by Model-Based Testing -- Model Checking Linearizability via Refinement -- Static Analysis -- It?s Doomed; We Can Prove It -- ?Carbon Credits? for Resource-Bounded Computations Using Amortised Analysis -- Field-Sensitive Value Analysis by Field-Insensitive Analysis -- Theorem Proving -- Making Temporal Logic Calculational: A Tool for Unification and Discovery -- A Tableau for CTL* -- Certifiable Specification and Verification of C Programs -- Formal Reasoning about Expectation Properties for Continuous Random Variables -- Semantics.-The Denotational Semantics of slotted-Circus -- Unifying Probability with Nondeterminism -- Towards an Operational Semantics for Alloy -- A Robust Semantics Hides Fewer Errors -- Special Track: Industrial Applications I -- Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks -- Formal Verification of Avionics Software Products -- Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study -- Object-Orientation -- Connecting UML and VDM++ with Open Tool Support -- Language and Tool Support for Class and State Machine Refinement in UML-B -- Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects -- Abstract Object Creation in Dynamic Logic -- Pointers -- Reasoning about Memory Layouts -- A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis -- Real-Time -- On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery -- Verifying Real-Time Systems against Scenario-Based Requirements -- Special Track: Tools and Industrial Applications II -- Formal Specification of a Cardiac Pacing System -- Automated Property Verification for Large Scale B Models -- Reduced Execution Semantics of MPI: From Theory to Practice -- Model Checking II -- A Metric Encoding for Bounded Model Checking -- An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method -- Verifying Information Flow Control over Unbounded Processes -- Specification and Verification of Web Applications in Rewriting Logic -- Industry-Day Abstracts -- Verifying the Microsoft Hyper-V Hypervisor with VCC -- Industrial Practice in Formal Methods: A Review -- Model-Based GUI Testing Using Uppaal  at Novo Nordisk. 330 $aThis book presents the refereed proceedings of FM 2009, the 16th International Symposium on Formal Methods, held as the Second World Congress on Formal Methods in Eindhoven, The Netherlands, in November 2009 in the course of the first International Formal Methods Week, FMWeek 2009. The 45 revised full papers presented together with 5 invited papers and 3 additional papers from the Industry Day were carefully reviewed and selected from 139 submissions. The papers are organized in topical sections on model checking, compositionality, verification, concurrency, refinement, static analysis, theorem proving, semantics, industrial applications, object-orientation, pointers, real-time, tools and industrial applications, and industry-day abstracts. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v5850 606 $aSoftware engineering 606 $aUser interfaces (Computer systems) 606 $aHuman-computer interaction 606 $aComputer science 606 $aCompilers (Computer programs) 606 $aComputer programming 606 $aSoftware Engineering 606 $aUser Interfaces and Human Computer Interaction 606 $aComputer Science Logic and Foundations of Programming 606 $aCompilers and Interpreters 606 $aProgramming Techniques 615 0$aSoftware engineering. 615 0$aUser interfaces (Computer systems). 615 0$aHuman-computer interaction. 615 0$aComputer science. 615 0$aCompilers (Computer programs). 615 0$aComputer programming. 615 14$aSoftware Engineering. 615 24$aUser Interfaces and Human Computer Interaction. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aCompilers and Interpreters. 615 24$aProgramming Techniques. 676 $a005.1 686 $aDAT 310f$2stub 686 $aDAT 510f$2stub 686 $aSS 4800$2rvk 701 $aCavalcanti$b Ana$01736503 701 $aDams$b Dennis$01751455 712 12$aInternational Symposium of Formal Methods Europe. 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483872003321 996 $aFM 2009$94190523 997 $aUNINA