Tobias Gedell

I am a Ph.D. student at the Computing Science Department at Chalmers.

For more information have a look at my CV.

How to reach me

• Email: gedell (@) cs.chalmers.se
• Phone: +46 31 772 1075
• Office: room 5452 in the ED-building
• Postal Adress, Fax, etc.

Research Interests

• Program languages: program analysis, type systems, semantics, implementation, functional programming
• Program verification: interactive theorem proving, formal proofs
• Security: information flow, non-interference, language-based verification

Publications

• Abstract Interpretation Plugins for Type Systems
  Tobias Gedell, Daniel Hedin
  12th International Conference on Algebraic Methodology and Software Technology (AMAST'08)
  (To appear.)
• Verification by Parallelization of Parametric Code
  Tobias Gedell, Reiner Hähnle
  Algebraic and Proof-theoretic Aspects of Non-classical Logics Essays in honour of Professor Daniele Mundici on occasion of his 60th birthday
  Springer-Verlag, LNCS 4460, 2007.
  (Postscript - PDF - Abstract)
• Polymorphism, Subtyping, Whole Program Analysis and Accurate Data Types in Usage Analysis
  Tobias Gedell, Jörgen Gustavsson, Josef Svenningsson
  The Fourth ASIAN Symposium on Programming Languages and Systems (APLAS'06)
  Springer-Verlag, LNCS 4279, 2006.
  (Postscript - PDF - BibTeX - Abstract)
• Automating Verification of Loops by Parallelization
  Tobias Gedell, Reiner Hähnle
  13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'06)
  Springer-Verlag, LNCS 4246, 2006.
  (Postscript - PDF - BibTeX - Abstract)
• Static Analysis and Deductive Verification of Programs
  Tobias Gedell
  Licentiate thesis
  Chalmers University of Technology, 2006.
  (Postscript - PDF - BibTeX - Abstract)
• Embedding Static Analysis into Tableaux and Sequent based Frameworks
  Tobias Gedell
  14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'05)
  Springer-Verlag, LNCS 3702, 2005.
  (PDF - BibTeX - Abstract)
• A Case Study on the Scalability of a Constraint Solving Algorithm: Polymorphic Usage Analysis with Subtyping
  Tobias Gedell
  Master's thesis
  (Postscript - BibTeX - Abstract)

Drafts

• Plugins for Structural Weakening and Strong Updates
  Tobias Gedell, Daniel Hedin

Developed Software

• Fire - A laboration submission and administration system.
• CoreSA - Implementation of the usage analysis presented here in GHC.
• SSC - A complete compiler for the STG language. Features type inference, garabage collection, unboxing, black holing, graph reduction and separate compilation.
• CSHC - A Cache Sensitive Haskell Compiler which tries to generate cache optimized code.
• ResNet - A distributed file system for UNIX with built-in redeandancy and load-balancing.
• SOE - A framework for dynamic object worlds.
• laVProxy - A filtering HTTP proxy.
• Crystal - A small 3D-engine.