This book constitutes the refereed proceedings of the 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010 held in Natal, Brazil, in September 2010. The 23 revised full papers presented with 2 invited papers and the abstract of 1 invited talk were carefully reviewed and selected from 68 submissions. The papers address all theoretical aspects and methodological issues of computing and are organized in topical sections on grammars, semantics, modelling, the special track on formal aspects of software testing and grand challenge in verified software, on logics, as well as algorithms and types.
Author(s): Ian J. Hayes (auth.), Ana Cavalcanti, David Deharbe, Marie-Claude Gaudel, Jim Woodcock (eds.)
Series: Lecture Notes in Computer Science 6255 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 397
Tags: Computation by Abstract Devices
Front Matter....Pages -
Invariants and Well-Foundedness in Program Algebra....Pages 1-14
A Theory of Software Product Line Refinement....Pages 15-43
The TLA + Proof System: Building a Heterogeneous Verification Platform....Pages 44-44
Subtyping Algorithm of Regular Tree Grammars with Disjoint Production Rules....Pages 45-59
Minimal Tree Language Extensions: A Keystone of XML Type Compatibility and Evolution....Pages 60-75
Tracking Down the Origins of Ambiguity in Context-Free Grammars....Pages 76-90
Prioritized slotted-Circus ....Pages 91-105
A Denotational Semantical Model for Orc Language....Pages 106-120
An Extended cCSP with Stable Failures Semantics....Pages 121-136
Preference and Non-deterministic Choice....Pages 137-152
Material Flow Abstraction of Manufacturing Systems....Pages 153-167
Specification and Verification of a MPI Implementation for a MP-SoC....Pages 168-183
Testing of Abstract Components....Pages 184-198
Scalable Distributed Concolic Testing: A Case Study on a Flash Storage Platform....Pages 199-213
Analyzing a Formal Specification of Mondex Using Model Checking....Pages 214-229
Formal Modelling of Separation Kernel Components....Pages 230-244
Mechanized Verification with Sharing....Pages 245-259
Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking....Pages 260-274
Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements....Pages 275-289
Complete Calculi for Structured Specifications in Fork Algebra....Pages 290-305
Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting....Pages 306-321
Characterizing Locality (Encapsulation) with Bisimulation....Pages 322-336
Justification Logic and History Based Computation....Pages 337-351
A Class of Greedy Algorithms and Its Relation to Greedoids....Pages 352-366
On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types....Pages 367-381
A Modality for Safe Resource Sharing and Code Reentrancy....Pages 382-396
Back Matter....Pages -
