At ECOOP'99, ECOOP'2000, and ECOOP'2001, workshops have been organized
under the title "Formal Techniques for Java Programs".
These all attracted in the order of 30 participants, and many asked
us to arrange a fourth event on this topic.
The topic is formal techniques to analyze programs, to precisely
describe program behavior, and to verify program properties. Whereas
the earlier workshops were restricted to Java, we have chosen to
widen the scope to include closely related languages such as C#.
Languages like Java and C# provide a good platform to bridge the
gap between formal techniques and practical program development,
because of their reasonably clear semantics and standardized libraries.
Moreover, these languages are an interesting target for formal techniques,
because the novel paradigm for program deployment introduced with
Java, with its improved portability and mobility, opens up new possibilities
for abuse and causes concern about security.
Possible topics include:
• specification techniques and interface specication languages
• specification of software components and library packages
• automated checking and verification of program properties
• verification logics
• language semantics
• type systems
• dynamic linking and loading
• security issues