Perspectives of Systems Informatics

Name: Perspectives of Systems Informatics | 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27 - July 1, 2011, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27 - July 1, 2011, Revised Selected Papers

Edmund Clarke Andrei Voronkov(Herausgeber*in)

Springer (Verlag)

Erschienen am 13. Mai 2012

XIV, 411 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-29709-0 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Preface
Organization
Table of Contents
Petri Net Distributability
Introduction, and Historical Remarks
Coloured Petri Nets and Transition Systems
Definitions, Intuition, and First Examples
Distributed Implementability
Unacceptable Method: Refinement by -Transitions
Acceptable Method: Isomorphism
Acceptable Method: Renaming
Distributed and Non-distributed Diamonds
Acceptable Method: Unfolding
Towards a Systematic Approach
Dangerous Non-distributed (Half-)Persistency
Bad Cycles
A Class of Transition Systems
Concluding Remarks
References
Connector Algebras, Petri Nets, and BIP
Introduction
Background
The BIP Component Framework
Nets with Boundaries
Encoding BIP into Nets
Monolithic Mapping
Composite BI(P) Systems
Structural Mapping
Encoding Nets with Boundaries into BI(P)
The BIP Algebra of Connectors
Related Work
Conclusion
References
Models of Provenance
End-to-End Guarantees in Embedded Control Systems
Mining Precise Specifications
Detecting Entry Points in Java Libraries
Motivation
Information Hiding in Java
Java Visibilities
Java Modularization Attempts
Metric: Method Weight
Definition
Limitations
Tool-Support for Computing MW
Experiments
ckjm - Spinellis' Implementation of Chidamber and Kemerer Metrics for Java
jarAnalyzer
Apache Commons IO
Discussion
Related Work
Conclusions
References
Static Analysis of Run-Time Modes in Synchronous Process Network
Introduction
Representation of Process Networks
Extraction of Mealy Machines
Abstraction of Paths and Their Execution
Identification of States
Determination of Edges and Tags
Mealy Machine of an Individual Process and the Whole Network
Implementation and Case Study
Related Work
Conclusion and Future Work
References
Compositional Methods in Characterizationof Timed Event Structures
Introduction
Timed Event Structures
From State-Space to Class Graph
Formula Construction
Compositional Methods
Conclusion
References
Algorithmic Debugging of SQL Views
Introduction
SQL Semantics
Declarative Debugging Framework
Conclusions
References
Timed Transition Systems with Independenceand Marked Scott Domains: An Adjunction
Introduction
Timed Transition Systems with Independence
Unfolding of Timed Transition Systems with Independence
Relating Timed Occurrence Transition Systems with Independence and Timed Event Structures
MarkedScottDomains
References
An Extensible System for Enhancing Social Conference Experience
Introduction
System Architecture and Implementation
Conference Services
History of the Project
Evaluation
Results
Related Work
Future Work
Conclusions
References
Exponential Acceleration of Model Checking for Perfect Recall Systems
Introduction
Background Logics and Models
Model Checking of Cut-Trees
Well-Structured Cut-Trees
Conclusion
References
Bootstrapping Compiler Generators from Partial Evaluators
Introduction
How to Bootstrap Compiler Generators
An Online Compiler Generator for Recursive Flowchart
Experimental Assessment
Related Work
Conclusion
References
A Logic Characteristic for Timed Extensions of Partial Order Based Equivalences
Introduction
Timed Event Structures
Observational Equivalences
Open Maps Bisimulation
Preliminaries
Category CTSL
Path Bisimulation
References
Proving the Correctness of Unfold/Fold Program Transformations Using Bisimulation
Introduction
Language
Bisimulation
Positive Supercompilation
Generalization
Folding
The Folding Transformation
Conclusion and Related Work
Homeomorphic Embedding for Supercompilation
Generalization Algorithm for Supercompilation
Residualization
Secure Multi-execution in Haskell
Introduction
Secure Multi-execution
Secure Multi-execution in Haskell
An Interpreter for the Monad ME
A Motivating Example
Related Work
Concluding Remarks
References
Towards an Open Framework for C Verification Tools Benchmarking
Introduction
Requirements for an Open Verification Framework
Related Work
LDVArchitecture
Key Components
User Interface
Summary
Verification Tools Benchmarking
Conclusion
References
Solving Coverability Problem for MonotonicCounter Systems by Supercompilation
Introduction
BasicNotions
Transition Systems
Configurations
Residual Graph, Tree and Set
Operations on Configurations
Restricted Ordering of Configurations of Counter Systems
Generalization
Algorithms
Supercompilation of Well-Structured Transitions Systems
Deciding the Coverability Problem for Counter Systems
Correctness
Related Work
Conclusion
References
Multi-result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions
Introduction
Diversity of Higher-Level Supercompilation
Branching Growth of the Penultimate Level in Metasystem Transitions
Multi-result Supercompilation and Program Analysis
The Synergy of Two-Level and Multi-result Supercompilation
Stage 0. Proving the Equivalence of Expressions: Rudiments of Control
Stage 1. Two-Level Supercompilation: Shaping of Control
Stage 2. Multi-result Supercompilation: Branching Growth of the Penultimate Level
Stage 3. Multi-generalization: Refinement of Control
MRSC: A Multi-result Supercompilation Framework
Constructing Two-Level Supercompilers
Working with Multi-result Supercompilers
The Current State and Directions of Future Work
Conclusion
References
Symbolic Loop Bound Computation for WCET Analysis
Introduction
Related Work
Motivating Example
Theoretical Considerations
Symbolic WCET Analysis
Recurrence Solving in Simple Loops
Non-deterministic Analysis in Shift-Loops
Flow Analysis on Multi-path Loops
Experimental Evaluation
Conclusion
References
GoRRiLA and Hard Reality
Introduction
GoRRiLA
Hard Reality
Conclusion
References
Reachability in One-Dimensional Controlled Polynomial Dynamical Systems
Introduction
Problem Description
Relative Properties of Integral Curves
An Algorithm Synthesising Finite Control Strategies
Conclusion, Related, and Future Work
References
Insertion Modeling System
Introduction
The Architecture of Insertion Modeling System
Input Languages of Insertion Machines
Examples of Insertion Machines
Restrictions on Insertion Functions
Verification Machine for Programming Languages
Conclusion
References
Decidability of Modular Logics for Concurrency
Introduction
Preliminaries on Process Algebra
Modular Logic
Decision Problems for Second Order Modular Logics
The Satisfiability Problem
The Model-Checking Problem
Decision Problems for Propositional Modular Logics
Decidability of PML2 and PML3
The Model-Checking Problems
Conclusive Remarks
References
Partial Evaluation of Janus Part 2: Assertions and Procedures
Introduction
The Reversible Language Janus
Informal Semantics of Janus
Reverse Execution
Partial Evaluation
Summary of Previous Work
Improved Handling of Assertions
Procedure Calls
Unfolding
Residualising
Implementation
Experiments and Results
Conclusion and Future Work
References
Scalable Parallel Interval Propagationfor Sparse Constraint Satisfaction Problems
Introduction
Software Parallelization Techniques
Interval Constraint Propagation
Parallel Interval Constraint Propagation
Scalability of Parallel Interval Constraint Propagation
Concluding Remarks
References
A Combined Technique for Automatic Detectionof Backward Binary Compatibility Problems
Introduction
Types of Backward Binary Compatibility Problems and Their Root Causes
Existing Approaches to Address Backward Compatibility
Suggested Method and Tool
Conclusion
References
Weighted Lumpability on Markov Chains
Introduction
Continuous-Time Markov Chains
Weighted Lumpability
Preservation of DTA Specifications
Preservation of MTL Specifications
Conclusions
References
Development of the Computer Language Classification Knowledge Portal
The Problem of Computer Language Classification
The Syntactic-Semantic-Pragmatic Approach
Towards an Open Temporal Evolving Ontology for the Classification of Computer Languages
Current State of the Project
References
Justified Terminological Reasoning
Introduction
The Description Logic ALC
Syntax of JALC
Semantics of JALC
Applications
Related Work
Conclusion
References
Implementing Conflict Resolution
Introduction
Preliminaries
The Conflict Resolution Algorithm
Strategies for Conflict Resolution
Strategies for Selecting Conflicts
Strategies for Assignment Refinement
Strategies for Selecting the Order on Variables
Optimization-Related Strategies
Benchmarks
Preprocessing
Experimental Evaluation
Randomly Generated Benchmarks
Real-Life Benchmarks
CRA vs. State-of-the-Art SMT Solvers
Summary
References
Symbolic Tree Transducers
Introduction
Preliminaries
Background Structure
Top-Down Tree Transducers
Symbolic Tree Transducers
Composition and Equivalence of STTs
Composition of STTs
Equivalence of Linear Single-Valued STTs
Checking Non-equivalence Symbolically
Related Work
Conclusions
References
Probabilistic Concepts in Formal Contexts
Introduction
Preliminaries
Probabilistic Concepts on Classes of Contexts
Probabilistic Concepts on One Context
Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken