The 2nd Workshop on the State of the Art in Automated Software Engineering took place on the 27 th of July 2005, at City University, London - UK. During the workshop there were seven presentations about various aspects concerning the theory and practice of automating the software engineering process. The presentations generated interesting discussions among the participants of the workshop. The title, name of the speaker, and abstract of each presentation are given below in the order that they were presented during the workshop. We would like to take this opportunity to thank all the presenters and participants of the workshop who helped make the day possible and interesting. [2] S. Ishtiaq, P. O'Hearn, BI as an Assertion Language for Mutable Data Structures, In the Proceedings of the 28th Annual ACM Symposium on Principles of Programming Languages, ACM, 2001. [3] J. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, In the Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2002. Recent Evolutions of the Tobias Combinatoria.

Physics-based animation programs can often be modeled in terms of hybrid automata. A hybrid automaton includes both discrete and continuous dynamical variables. The discrete variables define the automaton's modes of behavior. The continuous variables are governed by mode-dependent differential equations. This paper describes a system for specifying and automatically synthesizing physics-based animation programs based on hybrid automata. The system presents a program developer with a family of parameterized specification schemata. Each scheme describes a pattern of behavior as a hybrid automaton passes through a sequence of modes. The developer specifies a program by selecting one or more schemata and supplying application-specific instantiation parameters for each of them. Each scheme is associated with a set of axioms in logic of hybrid automata. The axioms serve to document the semantics of the specification scheme. Each scheme is also associated with a set of implementation rules. The rules synthesize program components implementing the specification in general physics-based animation architecture. The system allows animation programs to be developed and tested in an incremental manner. The system itself can be extended to incorporate additional schemata for specifying new patterns o behavior, along with new sets of axioms and implementation rules. It has been implemented and tested on over a dozen examples. We believe this research is a significant step toward a specification and synthesis system that is flexible enough to handle a wide variety of animation programs, yet restricted enough to permit programs to be synthesized automatically.

Physics-based animation programs are important in a variety of contexts, including education, science and entertainment among others. Manual construction of such programs is expensive, time consuming and prone to error. We have developed a system for automatically synthesizing physics-based animation programs for a significant class of problems: constrained systems of rigid bodies, subject to driving and dissipative forces. Our system includes a graphical interface for specifying a physical scenario, including objects, geometry, dynamical variables and coordinate systems, along with a symbolic interface for specifying forces and constraints operating in the scenario. The entities defined in the graphical interface serve as the underlying vocabulary for specifications constructed in the symbolic interface. We use an algorithmically controlled rewrite system to construct a numerical simulation program that drives a real-time animation of the specified scenario. The algorithm operates by partitioning the constraints and dynamic variables into classes, assigning each class to be implemented in a different component of a general simulation program scheme. Our approach provides many of the benefits of formal deductive methods of program synthesis, while keeping the computational costs of program synthesis more in line with conventional program generator technology. We have successfully tested our system on numerous examples.