Theoretical Aspects of Computing -- ICTAC 2011
8th International Colloquium, Johannesburg, South Africa, August 31 -- September 2, 2011, Proceedings
Published on 12. August 2011
X, 267 pages
978-3-642-23283-1 (ISBN)
Description
This book constitutes the refereed proceedings of the 8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011 held in Johannesburg, South Africa, in August/September 2011.
The 14 revised full papers presented together with the abstracts of three keynote talks were carefully reviewed and selected from 44 submissions. The papers address various 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.
The 14 revised full papers presented together with the abstracts of three keynote talks were carefully reviewed and selected from 44 submissions. The papers address various 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.
More details
Other editions
Additional editions
Antonio Cerone | Pekka Pihlajasaari
Theoretical Aspects of Computing -- ICTAC 2011
8th International Colloquium, Johannesburg, South Africa, August 31 -- September 2, 2011, Proceedings
Book
08/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Virtual Time and Timeout in Client-Server Networks
- Introduction
- Background
- Causal Model of Virtual Time
- Simulation Model of Virtual Time
- Contributions of This Work
- References
- The Use of Mathematics in Software Development
- References
- Infinitely Often Testing
- Axiomatizing Weak Ready Simulation Semantics over BCCSP
- Introduction
- Preliminaries
- Weak Simulation
- Ground-Completeness for Weak Simulation
- -Completeness for Weak Simulation
- Weak Ready Simulation
- Axiomatizing RS When A Is Infinite
- Axiomatizing RS When A Is Finite
- Conclusion
- References
- Symbolic Worst Case Execution Times
- Introduction
- Related Work
- Numeric Path Analysis
- Parametric Path Analysis
- Longest Paths in Singleton-Loop-Graphs
- Preliminaries
- The Algorithm
- While-Loop-Graphs
- Conclusion
- References
- Selecting Good a Priori Sequences for Vehicle Routing Problem with Stochastic Demand
- Introduction
- The a Priori Strategy for VRPSD
- Previous Results
- Our Model
- Our Results
- Non-split VRPSD on Trees
- Non-split VRPSD on Cycles
- VRPSD on Cactus Graphs
- Non-split VRPSD on General Graphs
- Discussion
- Conclusion
- References
- On Characterization, Definabilityand $\omega$ -Saturated Models
- Introduction
- Basic Definitions
- Characterization
- Definability
- Conclusions and Further Work
- References
- On the Complexity of Szilard Languages of Regulated Grammars
- Introduction
- SZLs of RCGs - Prerequisites
- On the Complexity of SZLs of RCGs
- Remarks on SZLs of RCGs with PS Rules
- On the Complexity of SZLs of Other Regulated Rewriting Grammars
- References
- Energy Games in Multiweighted Automata
- Introduction
- Multiweighted Automata and Games
- Relationship to Petri Nets
- Reductions among Energy Games
- Summary of Complexity Results
- Parameterized Existential Problems
- Extension to Timed Automata
- Conclusion and Future Work
- References
- Intersection Types for the Resource Control Lambda Calculi
- Untyped Resource Control Calculi
- Resource Control Lambda Calculus $\rcl$
- Resource Control Sequent Lambda Calculus $\llG$
- Intersection Type Assignment Systems for Resource Control
- Intersection Types for $\rcl$
- Intersection Types for $\llG$
- Typability $\Rightarrow$ SN in Both Systems
- Typeability $\Rightarrow$ SN in $\rcl \cap$
- Typeability $\Rightarrow$ SN in $\llG \cap$
- SN $\Rightarrow$ Typability in Both Systems
- SN $\Rightarrow$ Typability in $\rcl \cap$
- SN $\Rightarrow$ Typability in $\llG \cap$
- Conclusions
- References
- Modal Interface Theories for Communication-Safe Component Assemblies
- Introduction
- Interface Languages
- Interface Assemblies
- Modal I/O-Automata for Interface and Assembly Specifications
- Modal I/O-Transition Systems: Basic Definitions
- Modelling Component Systems with MIOs: Example
- Interfaces and Assemblies
- Communication-Safe Assemblies
- Refinement of Interfaces and Assemblies
- Case Study
- Conclusion
- References
- WP Semantics and Behavioral Subtyping
- Introduction
- The Programming Language: Java
- A WP Semantics for Java
- The Assertion Language: OOSL
- The WP Semantics
- Properties
- Soundness and Completeness
- Behavioral Subtyping
- Method Specification and Refinement
- Object Invariant
- Behavioral Subtyping
- Related Work and Conclusion
- References
- Computing Preconditions and Postconditions of While Loops
- Introduction: Preconditions and Postconditions of Loops
- Mathematical Background
- Elements of Relations
- Refinement Ordering
- Lattice Properties
- Invariant Relations
- Loop Semantics
- Invariant Relations
- Weakest Preconditions
- A Relational Formula
- Invariant Relations and Weakest Preconditions
- Illustration: A Larger Example
- Strongest Postconditions
- Relational Definition
- Invariant Relations and Strongest Postconditions
- Illustration: A Larger Example
- Computing Invariant Relations
- Mathematical Foundations
- Scaling Up
- Conclusion: Summary, Comparison and Prospects
- Summary
- Related Work
- Prospects
- References
- A Framework for Instantiating Pedagogic mLearning Objects Applications
- Introduction
- Related Work
- Mobile Learning (MLearning)
- MLearning Objects
- Traditional Learning Theories and MLearning
- The Global eLearning Framework
- MLearning Objects Frameworks
- Methodology
- Results and Discussions
- Raising Awareness of the Problem and Making Suggestions for MoLODUF Dimensions
- Developing the MoLODUF
- Evaluating the MoLODUF
- Instantiating MLearning Objects Deployment and Utilization Applications
- Conclusion and Future Work
- References
- Emulating Primality with Multiset Representations of Natural Numbers
- Introduction
- Encoding Finite Multisets with Primes
- Ranking/Unranking of Sets and Finite Sequences
- Encoding Multisets
- A Bijection between Finite Multisets and Natural Numbers
- Exploring the Analogy between Multiset Decompositions and Factoring
- A Multiset Analog to Multiplication
- Multiset Analogues for div, gcd and lcd
- Multiset Primes
- An Analog to the ``rad'' Function
- Emulating the Möbius and Mertens Functions
- Deriving Automorphisms of N
- Related Work
- Conclusion and Future Work
- References
- Formal Verification of a Lock-Free Stack with Hazard Pointers
- Introduction
- The Hazard Pointers Method
- A Lock-Free Stack with Hazard Pointers
- The Lock-Free Stack
- The Extended Stack
- The Verification Framework
- Interval Temporal Logic
- Symbolic Execution and Induction
- The System Model and the Decomposition Theory
- Verifying the Stack with Hazard Pointers
- Central Properties of Hazard Pointers
- Verification Conditions for the Stack
- The Main Proofs
- Related Work and Comparison
- Summary and Discussion
- References
- Ambiguity of Unary Symmetric Difference NFAs
- Introduction
- Background
- Definition of -NFAs
- Analysis of -NFA Behaviour
- Ambiguity
- Ambiguity of Unary -NFAs
- Other Ambiguity Results
- Conclusion and Future Work
- References
- Author Index
