This book constitutes the thoroughly refereed postconference proceedings of the 5th International Andrei Ershov Memorial Conference, PSI 2003, held in Akademgorodok, Novosibirsk, Russia in July 2003.
The 55 revised full papers presented were carefully reviewed and selected from 110 submissions during two rounds of evaluation and improvement. The papers are organized in topical sections on programming, software engineering, software education, program synthesis and transformation, graphical interfaces, partial evaluation and supercompilation, verification, logic and types, concurrent and distributed systems, reactive systems, program specification, verification and model checking, constraint programming, documentation and testing, databases, and natural language processing.
Author(s): Tony Hoare (auth.), Manfred Broy, Alexandre V. Zamulin (eds.)
Series: Lecture Notes in Computer Science 2890
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003
Language: English
Pages: 572
Tags: Logics and Meanings of Programs; Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Computation by Abstract Devices
Front Matter....Pages -
The Verifying Compiler: A Grand Challenge for Computing Research....Pages 1-12
Linear Types for Cashflow Reengineering....Pages 13-21
Storing Properties in Grouped Tagged Tuples....Pages 22-29
A Polymorphic Radix- n Framework for Fast Fourier Transforms....Pages 30-36
Intersecting Classes and Prototypes....Pages 37-45
Bending without Breaking: Making Software More Flexible....Pages 46-49
Program Construction in the Context of Evolutionary Computation....Pages 50-57
A Layered Architecture Sustaining Model-Driven and Event-Driven Software Development....Pages 58-65
The Outside-In Method of Teaching Introductory Programming....Pages 66-78
Numeric Types in Formal Synthesis....Pages 79-90
On the Possibility of Provably Secure Obfuscating Programs....Pages 91-102
Verification-Oriented Language C-Light and Its Structural Operational Semantics....Pages 103-111
Proofs-as-Imperative-Programs: Application to Synthesis of Contracts....Pages 112-119
On the Visualization and Aesthetics of Large Graphs....Pages 120-120
Data Mappings in the Model-View-Controller Pattern....Pages 121-132
The Translation Power of the Futamura Projections....Pages 133-147
A Compiler Generator for Constraint Logic Programs....Pages 148-161
The Supercompiler SCP4: General Structure....Pages 162-170
Partial Evaluation for Common Intermediate Language....Pages 171-177
Timed Verification with μ CRL....Pages 178-191
Verification of Distributed Dataspace Architectures....Pages 192-206
Using SPIN and STeP to Verify Business Processes Specifications....Pages 207-213
Integrating Tools for Automatic Program Verification....Pages 214-221
A Logical Reconstruction of Reachability....Pages 222-237
Recent Advances in Σ-Definability over Continuous Data Types....Pages 238-247
Open Maps and Trace Semantics for Timed Partial Order Models....Pages 248-259
Confidentiality for Multithreaded Programs via Bisimulation....Pages 260-273
Dynamic Modification of System Structures Using LLPNs....Pages 274-293
Principles for Entity Authentication....Pages 294-306
Causality and Replication in Concurrent Processes....Pages 307-318
Event-Driven Traversal of Logic Circuits for Re-evaluation of Boolean Functions in Reactive Systems....Pages 319-328
Teams of Pushdown Automata....Pages 329-337
Algebraic State Machines: Concepts and Applications to Security....Pages 338-343
Combining Aspects of Reactive Systems....Pages 344-349
OCL Extended with Temporal Logic....Pages 351-357
The Definition of Transitive Closure with OCL – Limitations and Applications –....Pages 358-365
Improving the Consistency Checking Process by Reusing Formal Verification Knowledge....Pages 366-380
Complexity of Model Checking by Iterative Improvement: The Pseudo-Boolean Framework....Pages 381-394
Polynomial Approximations for Model Checking....Pages 395-400
Separating Search and Strategy in Solver Cooperations....Pages 401-414
Industrial Application of External Black-Box Functions in Constraint Programming Solver....Pages 415-422
LGS: Geometric Constraint Solver....Pages 423-430
On Strategies of the Narrowing Operator Selection in the Constraint Propagation Method....Pages 431-437
PROG $\mathcal{DOC}$ — A New Program Documentation System....Pages 438-449
Integration of Functional and Timed Testing of Real-Time and Concurrent Systems....Pages 450-461
Test Case Generation for UML Statecharts....Pages 462-468
Conceptual Content Modeling and Management....Pages 469-493
A Relational Algebra for Functional Logic Deductive Databases....Pages 494-508
Implication of Functional Dependencies for Recursive Queries....Pages 509-519
TeXOR: Temporal XML Database on an Object-Relational Database System....Pages 520-530
Functional Dependencies, from Relational to XML....Pages 531-538
Data-Object Replication, Distribution, and Mobility in Network Environments....Pages 539-545
Multi-classification of Patent Applications with Winnow....Pages 546-555
Automatic Evaluation of Quality of an Explanatory Dictionary by Comparison of Word Senses....Pages 556-562
An Approach to Automatic Construction of a Hierarchical Subject Domain for Question Answering Systems....Pages 563-569
Back Matter....Pages -
