LEADER 05148nam 22006015 450 001 9910484926703321 005 20251226203446.0 010 $a1-280-38817-X 010 $a9786613566096 010 $a3-642-14808-5 024 7 $a10.1007/978-3-642-14808-8 035 $a(CKB)2670000000036356 035 $a(SSID)ssj0000446827 035 $a(PQKBManifestationID)11318386 035 $a(PQKBTitleCode)TC0000446827 035 $a(PQKBWorkID)10504736 035 $a(PQKB)11377995 035 $a(DE-He213)978-3-642-14808-8 035 $a(MiAaPQ)EBC3065694 035 $a(PPN)149018436 035 $a(BIP)31787119 035 $a(EXLCZ)992670000000036356 100 $a20100821d2010 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTheoretical Aspects of Computing $e7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010, Proceedings /$fedited by Ana Cavalcanti, David Deharbe, Marie-Claude Gaudel, Jim Woodcock 205 $a1st ed. 2010. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010. 215 $a1 online resource (XIII, 397 p. 60 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6255 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-642-14807-7 320 $aIncludes bibliographical references and index. 327 $aInvited Papers and Abstract -- Invariants and Well-Foundedness in Program Algebra -- A Theory of Software Product Line Refinement -- The TLA?+? Proof System: Building a Heterogeneous Verification Platform -- Grammars -- Subtyping Algorithm of Regular Tree Grammars with Disjoint Production Rules -- Minimal Tree Language Extensions: A Keystone of XML Type Compatibility and Evolution -- Tracking Down the Origins of Ambiguity in Context-Free Grammars -- Semantics -- Prioritized slotted-Circus -- A Denotational Semantical Model for Orc Language -- An Extended cCSP with Stable Failures Semantics -- Preference and Non-deterministic Choice -- Modelling -- Material Flow Abstraction of Manufacturing Systems -- Specification and Verification of a MPI Implementation for a MP-SoC -- Special Track: Formal Aspects of Software Testing and Grand Challenge in Verified Software -- Testing of Abstract Components -- Scalable Distributed Concolic Testing: A Case Study on a Flash Storage Platform -- Analyzing a Formal Specification of Mondex Using Model Checking -- Formal Modelling of Separation Kernel Components -- Mechanized Verification with Sharing -- Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking -- Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements -- Logics -- Complete Calculi for Structured Specifications in Fork Algebra -- Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting -- Characterizing Locality (Encapsulation) with Bisimulation -- Justification Logic and History Based Computation -- Algorithms and Types -- A Class of Greedy Algorithms and Its Relation to Greedoids -- On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types -- A Modality for Safe Resource Sharing andCode Reentrancy. 330 $aThe now well-established series of International Colloquia on Theoretical - pects of Computing (ICTAC) brings together practitionersand researchersfrom academia, industry and government to present research results, and exchange experience and ideas. Beyond these scholarly goals, another main purpose is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries. ThisvolumecontainsthepaperspresentedatICTAC2010.Itwasheldduring September 1-3 in the city of Natal, Rio Grande do Norte, Brazil. Therewere68submissionsbyauthorsfrom24countriesallaroundthe world. Each submission was reviewed by at least three, and on average four, Program Committee members and external reviewers. After extensive discussions, they decided to accept the 23 (regular) papers presented here. Authors of a selection of these papers were invited to submit an extended version of their work to a special issue of the Theoretical Computer Science journal. Seven of the papers were part of a special track including one paper on "F- mal Aspects of Software Testing", and six on the "Grand Challenge in Veri'ed Software."ThespecialtrackwasjointlyorganizedbyMarie-ClaudeGaudel,from the Universit´ e de Paris-Sud, and Jim Woodcock, from the University of York. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6255 606 $aComputer science 606 $aTheory of Computation 615 0$aComputer science. 615 14$aTheory of Computation. 676 $a003./54 701 $aCavalcanti$b Ana$01736503 712 12$aICTAC 2010 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484926703321 996 $aTheoretical Aspects of Computing$94521272 997 $aUNINA