Sciweavers

TAPSOFT
1997
Springer
13 years 7 months ago
Protective Interface Specifications
Gary T. Leavens, Jeannette M. Wing
TAPSOFT
1997
Springer
13 years 8 months ago
A Typed Intermediate Language for Flow-Directed Compilation
We present a typed intermediate language λCIL for optimizing compilers for function-oriented and polymorphically typed programming languages (e.g., ML). The language λCIL is a ty...
J. B. Wells, Allyn Dimock, Robert Muller, Franklyn...
TAPSOFT
1997
Springer
13 years 8 months ago
A Type-Based Approach to Program Security
This paper presents a type system which guarantees that well-typed programs in a procedural programming language satisfy a noninterference security property. With all program input...
Dennis M. Volpano, Geoffrey Smith
TAPSOFT
1997
Springer
13 years 8 months ago
What Does the Future Hold for Theoretical Computer Science?
Prospects for research in theoretical computer science are discussed. The maintenance of a genuine link between theory and practice is seen as key to the future health of both.
Donald Sannella
TAPSOFT
1997
Springer
13 years 8 months ago
On the Complexity of Function Pointer May-Alias Analysis
This paper considers the complexity of interprocedural function pointer may-alias analysis, i.e., determining the set of functions that a function pointer (in a language such as C...
Robert Muth, Saumya K. Debray
TAPSOFT
1997
Springer
13 years 8 months ago
Inclusion Constraints over Non-empty Sets of Trees
Abstract. We present a new constraint system called INES. Its constraints are conjunctions of inclusions t1 t2 between rst-order terms (without set operators) which are interpreted...
Martin Müller, Joachim Niehren, Andreas Podel...
TAPSOFT
1997
Springer
13 years 8 months ago
Traces of I/O-Automata in Isabelle/HOLCF
Abstract. This paper presents a formalization of nite and in nite sequences in domain theory carried out in the theorem prover Isabelle. The results are used to model the metatheor...
Olaf Müller, Tobias Nipkow
TAPSOFT
1997
Springer
13 years 8 months ago
A Compositional Proof of a Real-Time Mutual Exclusion Protocol
Kåre J. Kristoffersen, François Larou...
TAPSOFT
1997
Springer
13 years 8 months ago
Using LOTOS Patterns to Characterize Architectural Styles
We show how the formal description language LOTOS can be used to de ne software architectures and how patterns over LOTOS can serve to characterize architectural styles. We charact...
Maritta Heisel, Nicole Lévy