A schema for interprocedural modification side-effect analysis with pointer aliasing
The first interprocedural modification side-effects analysis for C (MODC) that obtains better than worst-case precision on programs with general-purpose pointer usage is presented with empirical results. The analysis consists of an algorithm schema ...
Synthesis of concurrent programs for an atomic read/write model of computation
Methods for mechanically synthesizing concurrent programs for temporal logic specifications have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually ...
Type elaboration and subtype completion for Java bytecode
Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely ...