Sara K.
Profile Summary
Reader in Computer Science, with research expertise in the area of Compiler Verification and Optimisation, Formal Methods, Logic and Verification, and Computational Biology. Particular interests include synthetic biology, emergent behaviour in multicellular systems, interactive theorem-proving, higher-order, temporal and substructural logics.
Expertise
Technology Researcher
> 5 Year Experience5/5
Employment History
Lecturer, Associate Professor, Reader
Lecturer 1995–2009, Associate Professor 2009–2019, Reader 2019–
Courses taught. Compiler Design (16 ×), Programming Language Design and Semantics (6 ×), Programming with Java (3 ×), Project Management for Computer Scientists (1 ×), Postgraduate Research Methods (2 ×), Logic for Computer Scientists (3 ×), Concurrent Processes (3 ×), Advanced Specification Methodologies (2 ×), Operating Systems (3 ×), Software Lifecycle Management (2 ×), Computational Biology (2 ×), Gene Design (for Synthetic Biology CDT) (3 ×) Supervision of undergraduate and MSc projects.
Leadership. Computer Science and Computing Systems Course Manager. First Year Tutor. Representative on Board of Examiners of the Faculty of Science. Undergraduate Studies Committee. Postgraduate Research Committee. Staff-student Liaison Committee. Welfare and Communication Committee. Exam Secretary. ATHENA Swan Lead. Deputy Director of UG Studies. Director of Student Experience.
PhD Supervisor. Computational Models of Morphology on Cellular Dynamics (2017), Epigenetic Adaptation to Environmental Stress in Plants (2013). On the Generation and Analysis of Program Transformations (2010). Understanding Morphogenesis in Myxobacteria from a Theoretical and Experimental Perspective (2009). Formalisation of Message Sequence Charts (2009).
PhD Examiner. Australian National University, Canberra (10/94), University of Ghent, Belgium (08/99), University of Cambridge, UK (01/08), University of Sussex (05/09), University of Stirling (07/11, 05/16), University of Illinois (04/14), University of Sheffield (01/18). Internal examiner for over a dozen PhD and MSc candidates.
Research Associate
Research Associate, Combining HOL with Isabelle. Investigated the applicability of Isabelle proof system by verifying hardware designs and formalising mathematical proofs. Developed environments for modal and linear logics and embeddings of programming logics such as Hoare Logic and the Temporal Logic of Actions. Dr. Larry Paulson and Prof. Mike Gordon.
Education
PhD - Computer Science
A Methodology for Integrating Design and Verification.
Advisors: Prof. Karl Levitt and Prof. Myla Archer.
MSc, Computer Science
Formal Methods, Software Systems, Computer Architecture.
BSc, Biomedical Science
Biophysics and Biochemistry
Languages
English
Full Professional Proficiency
Looking For
Preferred work-style
Publications
Postcondition-Preserving Fusion of Postorder Tree Transformations Davies and Kalvala, Proceedings of ACM Conference on Compiler Construction, San Diego 2020, ISBN 978-1-4503-7120-9/20/02.
A P-system model of swarming and aggregation in a Myxobacterial colony Nash and Kalvala, Journal of Membrane Computing Vol 1 Issue 2, Springer 2019.
Designing Artificial Biofilms, Kalvala, International Conference on Artificial Life (late breaking paper) Tokyo 2018.
An Integrated In Silico Simulation and Biomatter Compilation Approach tp Cellular Computation, Konur, Fellermann, Mierla, Sanassy, Ladroue, Kalvala, Gheorghe, Krasnogor, Advances in Un- conventional Computing: Volume 2 (ed. Adamatzky) Springer 2017.
Filamentation Grants Bacterial Colonies the Ability to Spread More Efficiently. Luo, Sirec, Asally, Kalvala. PNAS, 04/2017
On the importance of modelling the internal spatial dynamics of biological cells. Sayyid, Kalvala, DOI: 10.1016/j.biosystems.2016.05.012. BioSystems, 2016.
PlasMatch: a tool for choosing usable restriction enzymes and plasmid backbones. Goel, Kalvala. Proceedings of the 6th ACM Conference on Bioinformatics, Computational Biology and Health Informatics, BCB 2015
Constraint-Based Genetic Compilation. Ladroue, Kalvala. Algorithms for Computational Biology AlCoB 2015. pp 25-38, Springer International LNBI 9199, 2015.
Modelling and Stochastic Simulation of Synthetic Biological Boolean Gates. Sanassy, Fellermann, Konur, Ladroue, Mierla, Kalvala, Gheorghe, Krasnogor. Proceedings of 16th IEEE International Conference on High Performance Computing and Communications, pp. 404-408, Paris, France, 2014.
Modeling and Analysis of Genetic Boolean Gates using Infobiotics Workbench. S. Konur, C. Ladroue, Harold Fellermann, D. Sanassy, L. Mierla, F. Ipate, S. Kalvala, M. Gheorghe and N. Krasnogor. Proceedings of Workshop on Verification of Engineered Molecular Devices and Programs 2014 (CAV 2014), pp. 26-37, Vienna, Austria, 2014.
Predicting Promoter Activity from Sequence Analysis. Foster, Ladroue, Kalvala, SB 6.0, July 2013 (Poster presentation)
atgc: Assistant To Genome Compilation. Ladroue, Kalvala, SB 6.0, July 2013 (Poster presentation) A Formal Approach to Fixing Bugs. Kalvala, Warburton, in LNCS 7021, Springer-Verlag, 2011
Spatial Simulations of Myxobacterial Development. Holmes, Kalvala, Whitworth, PLoS Computa- tional Biology, Vol 6 (2), 2010
A framework proposition for cellular locality of Dictyostelium modelled in Pi-Calculus. Anthony Nash and Sara Kalvala. in 2nd Complex Systems Modelling and Simulation Workshop, 2009
Program transformations using temporal logic side conditions. Kalvala, Warburton, Lacey, ACM Transactions On Programming Languages And Systems, Vol 31 (4), 2009
A stochastic model of myxobacteria explains several features of myxobacterial motility and devel- opment, Holmes, Kalvala, Whitworth, in European Conference on Complex Systems 2009.
muCell - Interdisciplinary Research in Modelling and Spatial Simulation of Multi-cellular Environ- ments. Dominic. Orchard et al, in Reinvention: A Journal of Undergraduate Research, vol 2, 2009.
Race Conditions in Message Sequence Charts, Chen, Kalvala, Sinclair, APLAS 2005.
A Process-Based Semantics for Message Sequence Charts with Data, Chen, Kalvala, Sinclair, ASWEC 2005
Formal Modeling and Analysis of a Preliminary SATS Concept, Carreno, Gotliebsen, Butler, Kalvala, Nasa Langley, NASA/TM-2004-212999, 2004
Controller Synthesis for Object Petri Nets, Farwer, Kalvala, Misra, in Formal Methods in Systems Engineering, Springer Verlag, LNCS 2885, 2003
Accomplishments
Community Service:
ACM-Women Scholarships Programme, Committee member, 2020-
External Examiner (MSc programme) Oxford University, 2019-
External examiner (UG programme) Edinburgh University, 2016-2020
Fellow of The Higher Education Academy UK, 2016-
Cafe Scientifique Leamington Spa presentations, 05/16 and 03/17. ́
Outreach: Headstart programme (07/15), Sutton Trust Summer Schools (07/17, 07/18, 07/19), BCS App-athon (06/15), numerous school visits.
Workshop on Logic, Language, Information and Computation (WoLLIC), 2015. Programme Committee Member.
Committee Member ACM SIGLOG Women in Logic (2017–)
UK Software Sustainability Institute. Fellowship Mentor, 2015.
Athena SWAN Charter, Departmental Coordinator and Institutional Committee, 2012–
Frequent reviewer for ACM Computing Reviews, 2011– (Including two ‘Best Reviews’ for 2013)
EPSRC College Member, 2013– (Commendation 2018, 2019). Prioritisation (4 ×), Fellowship (2 ×), and Platform Grant panel member.
Grant reviewer BBSRC (2016–), NSF (2019)
6th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2012. Programme Committee Member.
3rd International Conference on Bioinformatics and Systems Biology, 2010. Programme Committee Member.
IEEE International Conference on Engineering of Complex Computer Systems, 2009. Programme Committee Member.
Bytecode Workshop @ ETAPS, 2009. Programme Committee Member.
British Colloquium on Theoretical Computer Science, 2009. Local Organiser and Scientific Co-Chair.
International Conference on Women in Games, 2008. Co-Organiser.
Research Grants:
CoInvestigator, Warwick Integrative Synthetic Biology Centre. Use of state-of-the-art principles of computational design and control engineering to optimise the development and application of novel synthetic biology tools. Part of the Synthetic Biology Research Centres (SBRC) Initiative, BBSRC/EPSRC. 11/14 05/20.
Principal Investigator, Towards Programmable Defensive Bacterial Coatings and Skins. Design and development of a Biomatter Compiler for use in Synthetic Biology. Application of compiler optimization and verification techniques to generate viable, robust, and adaptable genetic circuits. Specific goal is to apply new techniques in developing heterogenous biofilms. EPSRC grant for £261, 000. Partners at Nottingham, Newcastle, Sheffield and Bradford. 02/12 08/16.
Travel Grant, Performance Optimizations of Web Applications based on XQuery. Application of the program transformation methodology to optimize database queries. Collaboration with Being University of Technology. Royal Academy of Engineering Short Exchange award for £2, 115. 08/11.
Principal Investigator, Verification of the Optimising Phase of Compilers. Developing tools for applying optimisations to intermediate code and using formal methods on control flow graphs to verify their correctness. EPSRC grant for £78, 000. 08/06 09/09.
Principal Investigator, A Substructural Logic for Verification. Addressing some limitations of higher-order logic for verification of dynamic systems by adapting substructural logics (such as Linear Logic) as an extension of higher-order logic, and using them to build specification and verification tools. EPSRC grant for £50, 000. 10/98 09/01.
Principal Investigator, Formal Validation of Program Implementation. Development of a methodology for the practical verification of object code, exploiting TLA (temporal logic) and process algebras such as CCS. Proofs of code taken from compiled C libraries. Development of tools based on flow-diagram analysis and program abstraction. EPSRC grant for £300, 000. 10/95 09/98.
