EmBounded Project
Publications and Talks

Worst-Case Execution Times for a Purely Functional Language
Armelle Bonenfant, Christian Ferdinand, Kevin Hammond and Reinhold Heckmann, Proc. Implementation of Functional Languages (IFL 2006) , Lecture Notes in Computer Science 4449 , 2007 .
PDF (339K bytes) [BibTeX]
Towards Resource-Certified Software: A Formal Cost Model for Time and its Application to an Image-Processing Example
Armelle Bonenfant, Zenzhi Chen, Kevin Hammond, Greg Michaelson, Andy Wallace and Iain Wallace, ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15 , 2007 .
PDF (328K bytes) [BibTeX]
A Dependently Typed Framework for Static Analysis of Program Execution Costs
Edwin Brady and Kevin Hammond, Proc. Implementation and Applications of Functional Language (IFL) 2005 , Lecture Notes in Computer Science 4015 , Springer-Verlag , 2006 .
PDF (External Link) [BibTeX]
A Verified Staged Interpreter is a Verified Compiler: Multi-stage Programming with Dependent Types
Edwin Brady and Kevin Hammond, Proc. Conf. Generative Programming and Component Engineering (GPCE '06), Portland, Oregon , Stan Jarzabek, Douglas C. Schmidt and Todd L. Veldhuizen, ed. , ACM , 2006 .
PDF (External Link) [BibTeX]
Static Memory and Timing Analysis of Embedded Systems Code
Christian Ferdinand, Reinhold Heckmann, and B\"{a}rbel Franzen, Proceedings of VVSS2007 - 3rd European Symposium on Verification and Validation of Software Systems, 23rd of March 2007, Eindhoven , Perry Groot, ed. , 2007 .
PDF (149K bytes) [BibTeX]
Using Mean-Shift Tracking Algorithms for Real-Time Tracking of Moving Images on an Autonomous Vehicle Testbed Platform
Benjamin Gorry, Zezhi Chen, Kevin Hammond, Andy Wallace, and Greg Michaelson, IRMA 2007, International Conference on Intelligent Robotics and Manufacturing Automation, Venice, Italy, November 23-25, 2007, 2007 , World Academy of Science, Engineering and Technology (PWASET) , 2007 .
PDF (767K bytes) [BibTeX]
Towards a Box Calculus for Hierarchical Hume
Gudmond Grov and Greg Michaelson, Trends in Functional Programming , Marco T. Morazan, ed. , Intellect , 2007 .
PDF (External Link) [BibTeX]
Formal Verification of Concurrent Scheduling Strategies using TLA
Gudmund Grov, Greg Michaelson, and Andrew Ireland, 3rd IEEE International Workshop on Scheduling and Resource Management for Parallel and Distributed Systems , IEEE , 2007 .
PDF (External Link) [BibTeX]
Preserving Coordination Properties when Transforming Concurrent System Components
Gudmund Grov, Robert Pointon, Greg Michaelson, and Andrew Ireland, Coordination Models, Languages and Applications Track of the 23rd Annual ACM Symposium on Applied Computing , 2008 .
PDF (External Link) [BibTeX]
Exploiting Purely Functional Programming to Obtain Bounded Resource Behaviour: the Hume Approach
Kevin Hammond, First Central European Summer School, CEFP 2005, Budapest, Hungary, July 4-15, 2005, Revised Selected Lectures , Zoltan Horvath, ed. , Lecture Notes in Computer Science 4164 , Springer-Verlag , 2006 .
PDF (330K bytes) [BibTeX]
The EmBounded project (project paper)
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Serot and Andy Wallace, Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005 , Intellect , 2006 .
PDF (195K bytes) [BibTeX]
Towards Formally Verifiable Resource Bounds for Real-Time Embedded Systems
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hoffmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn S\'erot and Andy Wallace, Proc. Workshop on Innovative Techniques for Certification of Embedded Systems , 2006 .
PDF (597K bytes) [BibTeX]
Towards Formally Verifiable WCET Analysis for a Functional Programming Language
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn S\'erot and Andy Wallace, Proc. 6th Intl Workshop on Worst-Case Execution Time (WCET) Analysis , 2006 .
PDF (External Link) [BibTeX]
Bounded Space Programming using Finite State Machines and Recursive Functions: the Hume Approach
Kevin Hammond, Greg Michaelson and Pedro Vasconcelos, ACM Transactions on Software Engineering Methodology .
PDF (439K bytes) [BibTeX]
Automatic Amortised Worst-Case Execution Time Analysis
Christoph A. Herrmann and Armelle Bonenfant and Kevin Hammond and Steffen Jost and Hans-Wolfgang Loidl and Robert Pointon, 7th Int'l Workshop on Worst-Case Execution Time (WCET) Analysis, Proceedings , 2007 .
PDF (External Link) [BibTeX]
Type-Based Amortised Heap-Space Analysis.
Martin Hofmann and Steffen Jost, Proc. ESOP 2006 -- 2006 European Symposium on Programming , Peter Sestoft, ed. , Lecture Notes in Computer Science 3924 , Springer-Verlag , 2006 .
PDF (External Link) [BibTeX]
HW-Hume in Isabelle
Chunxu Liu and Greg Michaelson, Draft Proceedings of 19th International Symposium on Implementation and Application of Functional Languages , O. Chitil, ed. , Computing Laboratory, University of Kent , 2007 .
PDF (External Link) [BibTeX]
Toward Resource Certified Image Processing Software
Greg Michaelson, Andy Wallace, Kevin Hammond, Iain Wallace, Armelle Bonenfant and Zenzhi Chen, Proc. of Joint Annual Technical Conferences: Systems Engineering for Autonomous Systems Defence Technology Centre and Electro-Magnetic Remote Sensing Defence Technology Centre, Edinburgh , 2006 .
PDF (External Link) [BibTeX]
Costing by Construction: Compositional Design and Verification of Embedded Applications using the Hume Software Development Methodology
Norman Scaife, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson and Jocelyn Serot, In preparation , 2008 .
PDF (501K bytes)

This page was last modified on Friday 24 April 2009 12:48:38. This site is maintained by Robert Rothenberg (r r at cs dot st - andrews dot ac dot uk).