Sara Kalvala and Richard Warburton. A Formal Approach to Fixing Bugs. 2011. in Formal Methods: Foundations and Applications. LNCS vol 7021, Springer Verlag

Bugs within programs typically arise within well-known motifs, such as complex language features or misunderstood programming interfaces. We present a language for specifying program transformations which is paired with a novel methodology for identifying and fixing bug patterns within Java source code. We propose a combination of source code and bytecode analyses: this allows for using the control flow in the bytecode to help identify the bugs while generating corrected source code. The specification language uses a combination of syntactic rewrite rules and dataflow analysis generated from temporal logic based conditions.

Sara Kalvala, Richard Warburton and David Lacey. Program transformations using temporal logic side conditions. 2009. ACM Transactions On Programming Languages And Systems, vol 31.

This article describes an approach to program optimization based on transformations, where temporal logic is used to specify side conditions, and strategies are created which expand the repertoire of transformations and provide a suitable level of abstraction. We demonstrate the power of this approach by developing a set of optimizations using our transformation language and showing how the transformations can be converted into a form which makes it easier to apply them, while maintaining trust in the resulting optimizing steps. The approach is illustrated through a transformational case study where we apply several optimizations to a small program.

Richard Warburton and Sara Kalvala. From Specification to Optimisation: An Architecture for Optimisation of Java Bytecode. 2009. in Compiler Construction ,18th International Conference (CC 2009). Springer-Verlag.

We present the architecture of the Rosser toolkit that allows optimisations to be specified in a domain specic language, then com- piled and deployed towards optimising object programs. The optimisers generated by Rosser exploit model checking to apply data ow analysis to programs to nd optimising opportunities. The transformational lan- guage is derived from a formal basis and consequently can be proved sound. We validate the technique by comparing the application of opti- misers generated by our system against hand-written optimisations using the Java based Scimark 2.0 benchmark.

Antony Holmes, Sara Kalvala and David Whitworth. Myxobacteria motility: a novel 3D model of rippling behaviour in Myxococcus xanthus. 2009. in 2nd International Conference on Bioinformatics and Systems Biology (BSB 2009).

Bacterial populations provide interesting examples of how relatively simple signalling mechanisms can result in complex behaviour of the colony. A well studied example of this phenomenon can be found in myxobacteria; cells can coordinate themselves to form intricate rippling patterns and fruiting bodies using localised signalling. Our work attempts to understand and model this emergent behaviour. We developed an off-lattice Monte Carlo simulation of ripple formation using a using a software framework we have created and show how rippling is a consequence of the combined effect of cell biochemistry and cell physics.

Antony Holmes, Sara Kalvala and David Whitworth. A stochastic model of myxobacteria explains several features of myxobacterial motility and development. 2009. in European Conference on Complex Systems 2009.

Bacterial populations provide interesting examples of how relatively simple signalling mechanisms can result in complex behaviour of the colony. A well studied model is myxobacteria; cells can coordinate themselves to form intricate rippling pat- terns and fruiting bodies using localised signalling. Our work attempts to understand and model this emergent behaviour. We developed an o-lattice Monte Carlo simula- tion of cell motility and show it can be used to generate both rippling and fruiting body formations.

Anthony Nash and Sara Kalvala. A framework proposition for cellular locality of Dictyostelium modelled in Pi-Calculus. 2009. in 2nd Complex Systems Modelling and Simulation (CoSMoS) Workshop.

The aim of this paper is to review the use of process calculi as a means of representing various biochemical networks and processes. Recent literature, ideas and formulated systems are explored in conjunction with their respective biological examples. We then show how -Calculus can be used to model various aspects of cell locality in a cellular automaton, in addition to the signal transduction responsible for Dictyostelium discoideum aggregation.

Dominic Orchard, Jonathan Gover, Lee Lewis Herrington, James Lohr, Duncan Stead, Cathy Young, and Sara Kalvala. muCell - Interdisciplinary Research in Modelling and Spatial Simulation of Multi-cellular Environments. 2009. Reinvention: A Journal of Undergraduate Research, vol 2.

In this paper we present mu-Cell, an interdisciplinary research project undertaken by undergraduates at the University of Warwick, seeking to aid systems biology intuition. The project's main contribution is a modelling and simulation tool for multi-cellular environments aimed at simulating higher-level cellular behaviours based on the interoperation of biochemical signalling pathway models and procedural models of cell components and structures, such as flagella. Based on these interoperated models, mu-Cell is able to simulate spatial properties and behaviours of cells, such as chemotaxis. This paper introduces mu-Cell, gives a case study model and simulation of flagella-based chemotaxis in E. coli, and discusses the pedagogical outcomes of the project for the students.

Chien-An Chen, Sara Kalvala and Jane Sinclair. Race Conditions in Message Sequence Charts. 2005. in Programming Languages and Systems, Third Asian Symposium, pages 195-211. Springer-Verlag.

Message Sequence Charts (MSCs) are a graphical language for the description of scenarios in terms of message exchanges between communicating components in a distributed environment. The language has been standardised by the ITU and given a formal semantics by means of a process algebra. In this paper, we review a design anomaly, called race condition, in an MSC specification and argue that the current solution correcting race conditions is too weak when implementation is considered. In this paper, we provide an algorithm on partial orders as our solution. The result is a strengthened partial order, which is race-free and remains race-free in the implementation.

Chien-An Chen, Sara Kalvala and Jane Sinclair. Race-free Scenarios of Message Sequence Charts. 2005. in 12th Asia-Pacific Software Engineering Conference (APSEC), pages 138-148. IEEE Computer Society.

Message Sequence Charts (MSCs) capture system requirements in the design of reactive systems and communication protocols. In this paper, we review a design anomaly, called race conditions, in an MSC specification and present a few drawbacks with the current solution. We propose a new approach to correcting race conditions, and the limitation of this approach is also discussed.

Chien-An Chen, Sara Kalvala and Jane Sinclair. A Process-Based Semantics for Message Sequence Charts with Data. 2005. in 16th Australian Software Engineering Conference (ASWEC 2005), pages 130-139. IEEE Computer Society.

Message Sequence Charts (MSCs) are a graphical language for scenarios of communicating components exchanging messages in a distributed environment. The language has been standardised by the International Telecommunication Union (ITU) and given a formal semantics by means of a process algebra. Nevertheless, little attention has been given to MSCs where a message with data is a building block. In this paper, we investigate the impact that the concept of data flow brings to the conventional semantics, and propose a CCS-like process calculus as an alternative formal framework. The proposed semantics captures the data flow properties while maintaining the expressiveness of the conventional semantics. Equivalence of MSCs is also discussed from the perspective of the corresponding process equivalence.

Berndt Farwer, Saraswati Kalvala and Kundan Misra. Controller Synthesis for Object Petri Nets. 2003. in 5th International Conference on Formal Engineering Methods (ICFEM 2003), pages 432-451. Springer-Verlag.

A large class of real-world systems can be modelled as Petri nets, and complex systems are more conveniently modelled as object Petri nets. Ensuring that Petri net models avoid forbidden states has attracted much research effort. The work presented addresses the forbidden state problem for object Petri nets, through a method for controller synthesis. A simple illustrative example is given as well as an illustration in a flexible manufacturing system. The concept of place invariants plays an important role in Petri net theory. For the first time, place invariants are defined for object Petri nets.

Marco Benini, Sara Kalvala and Dirk Nowotka. Program Abstraction in a Higher-Order Logic Framework. 1998. in Theorem Proving in Higher Order Logics. Springer-Verlag.

We present a hybrid approach to program verification: a higher-order logic, used as a specification language, and a human-driven proof environment, with a process-algebraic engine to allow the use of process simulation as an abstraction technique. The domain of application is the validation of object code, and our intent is to adapt and mix existing formalisms to make the verification of representative programs possible. In this paper, we describe the logic in question and an underlying semantics given in terms of a process algebra.

Sara Kalvala. A Formulation of TLA in Isabelle. 1995. in Higher Order Logic Theorem Proving and its Applications. Springer-Verlag.

Sara Kalvala and Valeria de Paiva. Linear Logic in Isabelle. 1995. in Proceedings of the First Isabelle Users Workshop. University of Cambridge Computer Laboratory.

Sara Kalvala. Annotations in Formal Specifications and Proofs. 1994. Formal Methods in Systems Design, 5(1/2):119-144.