Perspectives of Systems Informatics
8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27 - July 1, 2011, Revised Selected Papers
Published on 13. May 2012
XIV, 411 pages
978-3-642-29709-0 (ISBN)
Description
This book contains thoroughly refereed and revised papers from the 8th International Andrei Ershov Memorial Conference on Perspectives of System Informatics, PSI 2011, held in Akademgorodok, Novosibirsk, Russia, in June/July 2011.
The 18 revised full papers and 10 revised short papers presented were carefully reviewed and selected from 60 submissions. The volume also contains 5 invited papers covering a range of hot topics in computer science and informatics. The papers are organized in topical sections on foundations of program and system development and analysis, partial evaluation, mixed computation, abstract interpretation, compiler construction, computer models and algorithms for bioinformatics, programming methodology and software engineering, information technologies, knowledge-based systems, and knowledge engineering.
More details
Other editions
Additional editions
Edmund Clarke | Andrei Voronkov
Perspectives of Systems Informatics
8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27 - July 1, 2011, Revised Selected Papers
Book
05/2012
Springer
€53.49
Shipment within 7-9 days
Content
- 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
