EmBounded Project - Bibiography

2009

Domain Specific Languages (DSLs) for Network Protocols: Saleem Bhatti, Edwin Brady, Kevin Hammond, and James McKinna. Proc. International Workshop on Next Generation Network Architecture (NGNA 2009), Montreal, Canada, 2009. to appear; [BibTeX]
Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols: Edwin Brady and Kevin Hammond. Fundamenta Informatica, 2009. to appear; [BibTeX]
Reasoning about Correctness Properties of a Coordination Language: Gudmund Grov. PhD Thesis. School of Mathematics and Computer Science, Heriot-Watt University, 2009.; [BibTeX]
Hume Cost Analyses for Imperative Programs: Gudmund Grov, Greg Michaelson, Christoph Herrmann, Hans-Wolfgang Loidl, Steffen Jost, and Kevin Hammond. Proc. 2009 International Conference on Software Engineering Theory and Practice (SETP 2009), 2009.; [BibTeX]
The Hume Report: K. Hammond and G. Michaelson. 2009 Version 0.3; [BibTeX] [PS]
Analysis Robustification: Jost, S. and Hammond, K. 2009 Deliverable D43; [BibTeX]
A Resource Logic for Hume: H-W. Loidl and L. Beringer. FM09 --- 16th International Symposium on Formal Methods, Eindhoven, The Netherlands, November 2--6, 2009. Submitted; [BibTeX]
Web site of the EmBounded Project (IST-510255): Robert Rothenberg. 2009; [BibTeX] [URL]
Costing-by-construction Exemplar: Scaife, N; Loidl, H-W; Michaelson, G; and S'erot, J. 2009 Deliverable D44; [BibTeX]
Lazy Amortised Analysis?: Hugo Sim~oes. PhD Thesis. School of Computer Science, University of St Andrews, ?? 2009.; [BibTeX]

2008

A type system with usage aspects: David Aspinall, Martin Hofmann, and Michal Konecný. J. Funct. Program. 18 (2), 2008, pp. 141-178.; [BibTeX] [EE]
Lightweight Invariants with Full Dependent Types: Edwin Brady, Christoph Herrmann, and Kevin Hammond. Proc. International Symposium on Trends in Functional Programming (TFP 2008), 2008.; [BibTeX]
Nominal Renaming Sets: Murdoch James Gabbay and Martin Hofmann. LPAR, 2008, pp. 158-173.; [BibTeX] [EE]
Destructive Update and Dynamic Data Structures: Grov, G. and Michaelson, G. 2008 Deliverable D35; [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 (SAC 2008), 2008.; [BibTeX] [URL]
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.; [BibTeX] [PDF]
Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories: Masahito Hasegawa, Martin Hofmann, and Gordon D. Plotkin. Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich (eds.) , 2008, pp. 367-385.; [BibTeX] [URL]
Pure Pointer Programs with Iteration: Martin Hofmann and Ulrich Schöpp. CSL, 2008, pp. 79-93.; [BibTeX] [EE]
Validation of Space analyses: Jost, S. and Hammond, K. 2008 Deliverable D30; [BibTeX]
``Carbon Credits'' for Resource-Bounded Computations: Jost, S; Hammond, K; Loidl, H-W; and Hofmann, M. ICFP'08 --- Intl. Conference on Functional Programming, 2008. Submitted; [BibTeX]
A Semantic Proof of Polytime Soundness of Light Affine Logic: Ugo Dal Lago and Martin Hofmann. CSR, 2008, pp. 134-145.; [BibTeX] [EE]
Certificates: Loidl, H-W. and Beringer, L. 2008 Deliverable D21; [BibTeX]
Hume to HAM Translator: Pointon, R.F. and Scaife, N. 2008 Deliverable D23; [BibTeX]
Hume Machine Code Compiler: Pointon, R.F. and Scaife, N. 2008 Deliverable D24; [BibTeX]
Analyses Integrated into Compiler: Pointon, R.F; Scaife, N; and Loidl, H-W. 2008 Deliverable D25; [BibTeX]
Evaluation of Hume and the Hume Methodology: Scaife, N; Loidl, H-W; Michaelson, G; and Sérot, J. 2008 Deliverable D33; [BibTeX]
Real-time Computer Vision Algorithms: Sérot, J. and Scaife, N. 2008 Deliverable D27; [BibTeX]
Cost Inference and Analysis for Recursive Functional Programs: P.B. Vasconcelos. PhD Thesis. University of St Andrews, February 2008.; [BibTeX]
Space cost analysis using sized types: Pedro Baltazar Vasconcelos. PhD Thesis. School of Computer Science, University of St Andrews, November 2008.; [BibTeX] [URL]

2007

Automatic Amortised Worst-Case Execution Time Analysis: Christoph A.~Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. 7th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Christine Rochange (ed.) , Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2007.; [BibTeX] [URL]
Towards Resource-Certified Software: A Formal Cost Model for Time and its Application to an Image-Processing Example: Armelle Bonenfant, Zezhi Chen, Kevin Hammond, Greg Michaelson, Andy Wallace, and Iain Wallace. ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15, Seoul, Korea, 2007.; [BibTeX] [PDF] [URL]
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.; [BibTeX] [URL]
Worst-Case Execution Times for a Purely Functional Language: A. Bonenfant, C. Ferdinand, K. Hammond, and R. Heckmann. Proc. 2006 Intl. Symp. on Impl. and Appl. of Functional Langs. (IFL 2006), Springer-Verlag LNCS 4449, 2007, pp. 235--252.; [BibTeX]
Automatic Amortised Worst-Case Execution Time Analysis: C.~Herrmann, A.~Bonenfant, K.~Hammond, S.~Jost, H.-W.~Loidl, and R.~Pointon. 7th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, 2007.; [BibTeX]
Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types: Edwin Brady, James McKinna, and Kevin Hammond. Proc. International Symposium on Trends in Functional Programming (TFP 2007), 2007.; [BibTeX]
Static Memory and Timing Analysis of Embedded Systems Code: Christian Ferdinand, Reinhold Heckmann, and Bärbel Franzen. Proceedings of VVSS2007 - 3rd European Symposium on Verification and Validation of Software Systems, 23rd of March 2007, Eindhoven, Perry Groot (ed.) , 2007.; [BibTeX] [URL]
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, 25, World Academy of Science, Engineering and Technology (PWASET), 2007.; [BibTeX] [URL]
Compiler Support Tools: Grov, G. 2007 Deliverable D26; [BibTeX]
Towards a Box Calculus for Hierarchical Hume: Gudmond Grov and Greg Michaelson. Trends in Functional Programming, Marco T. Morazan (ed.) : 8, Intellect, 2007.; [BibTeX] [URL]
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.; [BibTeX] [URL]
Fourth Project Workshop: Hammond, K. 2007 Deliverable D19; [BibTeX]
Low-Level Programming in Hume: an Exploration of the HW-Hume Level: Kevin Hammond, Gudmund Grov, Greg Michaelson, and Andrew Ireland. Proc. Implementation of Functional Languages (IFL 2006), Springer-Verlag LNCS 4449, 2007, pp. 91--107.; [BibTeX]
Automatic Amortised Worst-Case Execution Time Analysis: Christoph A. Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. 7th Int'l Workshop on Worst-Case Execution Time (WCET) Analysis, Proceedings, Pisa, Italy, July 3, 2007, 2007, pp. 13--18.; [BibTeX] [PDF] [URL]
Prototype Implementation of Space Analyses: Jost, S. 2007 Deliverable D13; [BibTeX]
Prototype Implementation of Time Analysis: Jost, S. 2007 Deliverable D15; [BibTeX]
Validation of the Prototype Worst-Case Executation Time (WCET) analysis: Jost, S. and Hammond, K. 2007 Deliverable D16; [BibTeX]
Report on Stack-space Analysis: Jost, S; Loidl, H-W; and Hammond, K. 2007 Deliverable D5; [BibTeX]
Report on Heap-space Analysis: Jost, S; Loidl, H-W; and Hammond, K. 2007 Deliverable D11; [BibTeX]
Report on WCET Analysis: Jost, S; Loidl, H-W; and Hammond, K. 2007 Deliverable D14; [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.; [BibTeX] [URL]
Assertion Language: Loidl, H-W. and Grov, G. 2007 Deliverable D17; [BibTeX]
Mobile Resource Guarantees (project evaluation paper): D. Sannella, M. Hofmann, D. Aspinall, S. Gilmore, I. Stark, L. Beringer, H-W. Loidl, K. MacKenzie, A. Momigliano, and O. Shkaravska. TFP05: Trends in Functional Programing, Intellect, Tallinn, Estonia, 2007, pp. 211--226.; [BibTeX] [URL]
Intersection Types for Cost-analysis of Functional Programs: Hugo R. Simoes, Kevin Hammond, M'ario Florido, and Pedro Vasconcelos. Proc. 2006 International Conf. on Types (TYPES 2006), Springer-Verlag LNCS, 2007.; [BibTeX]
The Worst-Case Execution Time Problem --- Overview of Methods and Survey of Tools: Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström. ACM Transactions on Embedded Computing Systems, 2007. To appear; [BibTeX]

2006

Reading, Writing and Relations: N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Proc. Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006), Sydney, Australia, 2006.; [BibTeX]
A Bytecode Logic for JML and Types: L. Beringer and M. Hofmann. Proc. Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006), Sydney, Australia, 2006.; [BibTeX]
A Dependently Typed Framework for Static Analysis of Program Execution Costs: Edwin Brady and Kevin Hammond. Implementation of Functional Languages (IFL) 2005, Lecture Notes in Computer Science 4015, Springer, Berlin/Heidelberg, 2006, pp. 74-90.; [BibTeX] [DOI] [PDF]
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, Lecture Notes in Computer Science, Springer, 2006.; [BibTeX] [PDF]
A Proof System for the Linear Time <span class='mathrm'>μ</span>-Calculus: C. Dax, M. Hofmann, and M. Lange. Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, Kolkata, India, 2006.; [BibTeX]
EmBounded: Formally Embedded Systems: The EmBounded Project. The House Magazine, Dods Parliamentary Communications, Ltd, November 2006. Advertisement.; [BibTeX] [PDF]
Improved Worst-Case Execution Time Prediction via Execution Contexts: Christian Ferdinand and Reinhold Heckmann. Proc. Embedded World 2006 Conference,N"urnberg, Germany, 2006.; [BibTeX]
Verifying Timing Properties of Safety-Critical Embedded Software by Abstract Interpretation: Christian Ferdinand and Reinhold Heckmann. Proc. Embedded Real Time Software Congress (ERTS 2006), Toulouse, France, 2006.; [BibTeX]
An Abstract Machine Implementation for Hume: K. Hammond. 2006; [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, Zoltán Horváth (ed.) : Lecture Notes in Computer Science 4164, Springer-Verlag, 2006, pp. 100-134.; [BibTeX] [DOI] [PDF] [ISBN]
The EmBounded project (project paper): Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Sérot, and Andy Wallace. Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005, Trends in Functional Programming 6, Intellect, 2006.; [BibTeX] [PDF]
The EmBounded Project: Automatic Prediction of Resource Bounds for Embedded Systems: Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn S'erot, and Andy Wallace. Trends in Functional Programming, Volume 6, 2006.; [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érot, and Andy Wallace. Proc. Workshop on Innovative Techniques for Certification of Embedded Systems, 2006.; [BibTeX] [PDF]
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érot, and Andy Wallace. 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Frank Mueller (ed.) : Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 2006.; [BibTeX] [PDF] [URL]
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, 2006. Submitted; [BibTeX] [PDF]
Static Memory and Execution Time Analysis of Embedded Code: Reinhold Heckmann and Christian Ferdinand. Proc. SAE World Congress, Michigan, USA, 2006.; [BibTeX]
Type-based Amortised Heap-Space Analysis (for an Object-Oriented Language): Hofmann, Martin and Jost, Steffen. Proceedings of the 15th European Symposium on Programming (ESOP), Peter Sestoft (ed.) : Lecture Notes in Computer Science (LNCS) 3924, Springer-Verlag, 2006.; [BibTeX] [URL]
Type-based Amortised Heap-Space Analysis (for an Object-Oriented Language): Hofmann, Martin and Jost, Steffen. Proceedings of the 15th European Symposium on Programming (ESOP), Peter Sestoft (ed.) : Lecture Notes in Computer Science (LNCS) 3924, Springer-Verlag, 2006.; [BibTeX] [URL]
Type-Based Amortised Heap-Space Analysis.: Martin Hofmann and Steffen Jost. Programming Languages and Systems : 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Peter Sestoft (ed.) : Lecture Notes in Computer Science 3924, Springer-Verlag, 2006, pp. 22-37.; [BibTeX] [DOI] [ISBN]
Well-foundedness in Realizability: M. Hofmann, J. van Oosten, and T. Streicher. Archive for Mathematical Logic 45 (7), 2006, pp. 795--805.; [BibTeX]
Automated WCET Analysis based on Program Modes: Meng-Luo Ji, Ji Wang, Shuhao Li, and Zhi-Chang Qi. AST'06, ACM Press, 2006, pp. 36-42.; [BibTeX]
Formal Hume Semantics: Jost, S. 2006 Deliverable D12; [BibTeX]
Cost Model: Loidl, H-W. and Hammond, K. 2006 Deliverable D4; [BibTeX]
Recursion, Iteration and Hume Scheduling: Greg Michaelson and Robert Pointon. Trends in Functional Programming (TFP'06), Nottingham UK, 2006.; [BibTeX]
Toward Resource Certified Image Processing Software: Greg Michaelson, Andy Wallace, Kevin Hammond, Iain Wallace, Armelle Bonenfant, and Zezhi Chen. Systems Engineering for Autonomous Systems Defence Technology Centre (SEAS DTC), Annual Technical Conference, July 2006, Edinburgh, Conference Proceedings, Edinburgh, UK MoD, 2006, pp. A15.; [BibTeX] [PDF] [URL]
Compiling vs Costing - Experiences With Hume: Robert F. Pointon. Implementation of Functional Languages (IFL'06), Budapest Hungary, 2006.; [BibTeX]
Real-time Testbed Applications: Jocelyn Serot and Norman Scaife. 2006 Laboratoire LASMEA, Blaise Pascal University; [BibTeX]
Real-time Testbed Applications: Jocelyn Serot and Norman Scaife. 2006 Deliverable D7; [BibTeX]

2005

Mobile Resource Guarantees for Smart Devices: David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, and Ian Stark. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS 2004, Marseille, LNCS 3362, Springer, 2005, pp. 1--26.; [BibTeX] [PDF] [URL]
Automatic Certification of Heap Consumption: Beringer, L; Hofmann, M; Momigliano, A; and Shkaravska, O. LPAR 2004 --- Logic for Programming, Artificial Intelligence, and Reasoning, Franz Baader, Andrei Voronkov (ed.) : LNCS 3452, Springer, Montevideo, Uruguay, March 14--18, 2005, pp. 347--362.; [BibTeX] [PDF]
Exploiting Purely Functional Programming to Obtain Bounded Resource Behaviour: The Hume Approach: Kevin Hammond. CEFP, 2005, pp. 100-134.; [BibTeX] [EE]
Is it Time for Real-Time Functional Programming?: Kevin Hammond. Trends in Functional Programming, Volume 4, Stephen Gilmore (ed.) : Trends in Functional Programming 4, Intellect, 2005, pp. 1-14.; [BibTeX] [ISBN]
The EmBounded project (project paper): Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Sérot, and Andy Wallace. Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005, Institute of Cybernetics, 2005, pp. 220-235. Online; [BibTeX] [URL]
Certification of Quantitative Properties of Programs: M. Hofmann, H-W. Loidl, and L. Beringer, IOS Press, 2005. Marktoberdorf Summer School, Aug 2-13, 2005; [BibTeX] [URL]
FSM-Hume is Finite State: Greg Michaelson, Kevin Hammond, and Jocelyn Sérot. Trends in Functional Programming, Volume 4, Stephen Gilmore (ed.) : Trends in Functional Programming 4, Intellect, 2005, pp. 19-28.; [BibTeX] [ISBN]

Bibliography

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1986