Publications of René Rydhof Hansen

Journal papers

Julia L. Lawall, Julien Brunel, Nicolas Palix, René Rydhof Hansen, Henrik Stuart, and Gilles Muller. WYSIWIB: Exploiting Fine-Grained Program Structure in a Scriptable API-Usage Protocol Finding Process. Software: Practice and Experience. Forthcoming.
Rocco De Nicola, Daniele Gorla, René Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, Christian W. Probst, and Rosario Pugliese. From Flow Logic to Static Type Systems for Coordination Languages . Science of Computer Programming, 75(6):376-397, 2010, Elsevier.
[ doi ]
Thomas Bolander and René Rydhof Hansen. Hybrid Logical Analyses of the Ambient Calculus. Information and Computation, 208(5):433-449, 2010.
Flemming Nielson, René Rydhof Hansen, and Hanne Riis Nielson. Abstract Interpretation of Mobile Ambients. Science of Computer Programming, 47(2-3):145-175, 2003.
Flemming Nielson, Hanne Riis Nielson, and René Rydhof Hansen. Validating Firewalls using Flow Logics. Theoretical Computer Science, 283(2):381-418, 2002.

Invited

Christian W. Probst and René Rydhof Hansen. An Extensible Analysable System Model. Information Security Technical Report, 13(4):235-246, 2008. Elsevier.

Refereed conferences / workshops

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen Adaptable Value-Set Analysis for Low-Level Code . In Proceedings of The 6th International Workshop on Systems Software Verification (SSV2011). To appear.
Andreas Engelbredt Dalsgaard, René Rydhof Hansen, Kenneth Yrke Jørgensen, Kim G. Larsen, Mads Chr. Olesen, Petur Olsen, and Jiri Srba opaal: A Lattice Model Checker (tool paper). In Proceedings of The 3rd NASA Formal Methods Symposium (NFM 2011) , volume 6617 og Lecture Notes in Computer Science, pages 487-493, Pasadena, CA, USA, April 2011, Springer Verlag.
Hans Søndergaard, Bent Thomsen, Anders P. Ravn, René R. Hansen, and Thomas Bøgholm. Refactoring Real-Time Java profiles In Proceedings of The 14th International Symposium on Object/Component/Service-oriented Real-time Distributed Computing (ISORC 2011) , pages 109-116, Newport Beach, CA, USA, March 2011, IEEE Computer Society.
Mads Chr. Olesen, René Rydhof Hansen, Julia L. Lawall, Nicolas Palix. Clang and Coccinelle: Synergising program analysis tools for CERT C Secure Coding Standard certification In Proceedings of The 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33 of Electronic Communications of the EASST, Pisa, Italy, September 2010.
Thomas Bøgholm, René Rydhof Hansen, Anders P. Ravn, Hans Søndergaard, Bent Thomsen. Schedulability Analysis for Java Finalizers. In Proceedings of The 8th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2010) , pages 1-7, Prague, Czech Republic, August 2010, ACM.
Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In Proceedings of the 10th International Workshop on on Worst-Case Execution-Time Analysis (WCET2010) , pages 114-124, Brussels, Belgium, July 2010. OCG vol. 268.
Julia Lawall, Ben Laurie, René Rydhof Hansen, Nicolas Palix, and Gilles Muller. Finding Error Handling Bugs in OpenSSL using Coccinelle (experience report). In Proceedings of The 8th European Dependable Computing Conference (EDCC-2010) , pages 191-196, Valencia, Spain, April 2010. IEEE Computer Society.
Thomas Bøgholm, René Rydhof Hansen, Anders P. Ravn, Bent Thomsen, Hans Søndergaard. A predictable Java profile - rationale and implementations . In Proceedings of The 7th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2009), pages 150-159, Madrid, Spain, September 2009. ACM.
Christian W. Probst and René Rydhof Hansen. Fluid Information Systems. In Proceedings of the New Security Paradigms Workshop (NSPW'09), pages 125-132, Oxford, England, September 2009. ACM Press.
Christian W. Probst and René Rydhof Hansen. Analysing Access Control Specifications. In Proceedings of the Fourth International IEEE Workshop on Systematic Approaches to Digital Forensic Engineering (SADFE-2009), pages 22-33, Oakland, CA, USA, May 2009. IEEE Computer Society.
Julia L. Lawall, Julien Brunel, Nicolas Palix, René Rydhof Hansen, and Gilles Muller. WYSIWIB: A Declarative Approach to Finding API Protocols and Bugs in Linux Code. In Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'09), pages 43-52. Estoril, Portugal. July 2009.
Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, and Gilles Muller. A Foundation for Flow-Based Program Matching Using Logic and Model Checking. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL'09), pages 114-126. Savannah, GA, USA. January 2009.
Andrew D. Gordon, Hans Hüttel, and René Rydhof Hansen. Type inference for correspondence types. In Proceedings of the 6th International Workshop on Security Issues in Concurrency (SecCo'08), volume 242(3) of Electronic Notes in Theoretical Computer Science (ENTCS), pages 21-36, Toronto, Canada, August 2008.
Rocco De Nicola, Daniele Gorla, René Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, Christian W. Probst, and Rosario Pugliese. From Flow Logic to Static Type Systems for Coordination Languages. In Proceedings of the 10th International Conference on Coordination Models and Languages (Coordination'08), volume 5052 of Lecture Notes in Computer Science, pages 100-116. Oslo, Norway, June 2008. Springer Verlag.
Yoann Padioleau, Julia Lawall, René Rydhof Hansen, and Gilles Muller. Documenting and Automating Collateral Evolutions in Linux Device Drivers. In Proceedings of the European Conference on Computer Systems 2008 (EuroSys 2008), pages 247-260. ACM. Glasgow, Scotland, April 2008.
René Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, and Christian W. Probst. Static Validation of License Conformance Policies. In Proceedings of the First International Workshop on Advances in Policy Enforcement (APE'08), pages 1104-1111. IEEE Computer Society. Barcelona, Spain, March 2008.
Neil D. Jones and René Rydhof Hansen. The Semantics of "Semantic Patches" in Coccinelle: Program Transformation for the Working Programmer. In Proceedings of the ASIAN Symposium on Programming Languages and Systems (APLAS 2007), volume 4807 of Lecture Notes in Computer Science, pages 303-318. Singapore, November/December 2007. Springer Verlag.
Henrik Stuart, René Rydhof Hansen, Julia L. Lawall, Jesper Andersen, Yoann Padioleau, and Gilles Muller. Towards Easing the Diagnosis of Bugs in OS Code. In Proceedings of the Workshop on Linguistic Support for Modern Operating Systems (PLOS'07). Skamania Lodge/Stevenson, Washington, USA. October 2007.
Thomas Bolander and René Rydhof Hansen. Hybrid Logical Analyses of the Ambient Calculus. In Proceedings of the Workshop on Logic, Language, Information and Computation (WoLLIC'2007), volume 4576 of Lecture Notes in Computer Science, pages 83-100. Rio de Janeiro, Brazil, July 2007. Springer Verlag.
Yoann Padioleau, René Rydhof Hansen, Julia L. Lawall, and Gilles Muller. Semantic Patches for Documenting and Automating Collateral Evolutions. In Proceedings of the Workshop on Linguistic Support for Modern Operating Systems (PLOS'06). San Jose, California, USA.
Terkel K. Tolstrup, Flemming Nielson, and René Rydhof Hansen. Locality-based Security Policies. In Proceedings of the Workshop on Formal Aspects of Security and Trust (FAST'06), volume 4691 of Lecture Notes in Computer Science, pages 185-201. Hamilton, Ontario, Canada. Springer Verlag.
Christian W. Probst, René Rydhof Hansen, and Flemming Nielson. Where can an Insider Attack?. In Proceedings of the Workshop on Formal Aspects of Security and Trust (FAST'06), volume 4691 of Lecture Notes in Computer Science, pages 127-142. Hamilton, Ontario, Canada. Springer Verlag.
Dan Søndergaard, Christian W. Probst, Christian Damsgaard Jensen, and René Rydhof Hansen. Program Partitioning using Dynamic Trust Models. In Proceedings of the Workshop on Formal Aspects of Security and Trust (FAST'06), volume 4691 of Lecture Notes in Computer Science, pages 170-184. Hamilton, Ontario, Canada. Springer Verlag.
René Rydhof Hansen, Christian W. Probst, and Flemming Nielson. Sandboxing in myKlaim. In Proceedings of the First International Conference on Availability, Reliability and Security (ARES'06). IEEE Computer Society. Vienna, Austria, April 2006.
René Rydhof Hansen and Christian W. Probst. Non-Interference and Erasure Policies for Java Card Bytecode. In Proceedings of the 6th International Workshop on Issues in the Theory of Security (WITS'06), Vienna, Austria, March 2006.
René Rydhof Hansen and Christian W. Probst. Secure Dynamic Program Repartitioning. In Proceedings of Nordic Workshop on Secure IT-Systems (NORDSEC'05), Tartu, Estonia, October 2005.
René Rydhof Hansen and Igor A. Siveroni. Towards Verification of Well-Formed Transactions in Java Card Bytecode. In Proceedings of the First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'05), volume 141(1) of Electronic Notes in Theoretical Computer Science (ENTCS), pages 145-162, Edinburgh, Scotland, April 2005. Elsevier.
René Rydhof Hansen. A Hardest Attacker for Leaking References. In Proceedings of European Symposium on Programming (ESOP'04), volume 2986 of Lecture Notes in Computer Science, pages 310-324, Barcelona, Spain, March/April 2004. Springer Verlag.
Flemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, René Rydhof Hansen, Henrik Pilegaard, and Helmut Seidl. The Succinct Solver Suite. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 251-265, Barcelona, Spain, March/April 2004. Springer Verlag.
René Rydhof Hansen. A Prototype Tool for JavaCard Firewall Analysis. In Proceedings of Nordic Workshop on Secure IT-Systems (NORDSEC'02), Karlstad, Sweden, November 2002. Proceedings published as Karlstad University Studies 2002:31.
René Rydhof Hansen, Jacob Grydholt Jensen, Flemming Nielson, and Hanne Riis Nielson. Abstract Interpretation of Mobile Ambients. In Proceedings of Static Analysis Symposium (SAS'99), volume 1694 of Lecture Notes in Computer Science, pages 134-148, Venice, Italy, September 1999. Springer Verlag.
Flemming Nielson, Hanne Riis Nielson, René Rydhof Hansen, and Jacob Grydholt Jensen. Validating Firewalls in Mobile Ambients. In Proceedings of Concurrency Theory (CONCUR'99), volume 1664 of Lecture Notes in Computer Science, pages 464-477, Eindhoven, The Netherlands, August 1999. Springer Verlag.

Other publications

Henrik Søndberg Karlsen, Erik Ramsgaard Wognsen, Mads Chr. Olesen, and René Rydhof Hansen. Study, Formalisation, and Analysis of Dalvik Bytecode. To appear in the informal proceedings of The Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2012) . March 2012.
Julia Lawall, René Rydhof Hansen, Nicolas Palix, and Gilles Muller. Improving the Security of Infrastructure Software using Coccinelle. In ERCIM News 83, page 54, October 2010.
Thomas Bøgholm, René Rydhof Hansen, Anders P. Ravn, Hans Søndergaard, and Bent Thomsen. Formal Modelling and Analysis of Predictable Java . In ERCIM News 81, pages 52-53, April 2010.
Martin Toft, Mads Christian Olesen, Andreas Dalsgaard, René Rydhof Hansen, and Kim Guldstrand Larsen. WCET Analysis of ARM Processors using Real-Time Model Checking . In Proceedings of Doctoral Symposium on Systems Software Verification (DS SSV'09) , pages 4-6, Aachen, Germany, June 2009. Proceedings published as technical report: Aachener Informatik Berichte number AIB-2009-14 .
Gilles Muller, Yoann Padioleau, Julia L. Lawall, and René Rydhof Hansen. Semantic Patches Considered Helpful. Position paper. In ACM SIGOPS Operating Systems Review, 40(3):90-92, July 2006.
René Rydhof Hansen. Non-Interference and Simple Erasure Policies for Java Card Bytecode. Extended abstract. In Proceedings of the 2nd International Workshop on Programming Language Interference and Dependence (PLID'05) . London, England, September 2005.
René Rydhof Hansen and Igor Siveroni. Java Card Safety and Security through Static Analysis. Short presentation (not in proceedings) at Fifth ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP'2003) . Darmstadt, Germany, July 2003.
René Rydhof Hansen. Flow Logics for Carmel(abstract). In Proceedings of Nordic Workshop on Programming Theory (NWPT'01). Lyngby, Denmark, October 2001. Abstracts published as DTU Technical Report IMM-TR-2001-12.
René Rydhof Hansen and Jacob Grydholt Jensen. Computer Security in the Mobile Ambients calculus(abstract). In Proceedings of Nordic Workshop on Programming Theory (NWPT'98). Turku, Finland, October 1998. Abstracts published as TUCS General Publication no. 11.

Theses

René Rydhof Hansen. Flow Logic for Language-Based Safety and Security. PhD thesis, Informatics and Mathematical Modelling, Technical University of Denmark, 2005.
René Rydhof Hansen and Jacob Grydholt Jensen. Flow Logics for Mobile Ambients. Master's thesis, Department of Computer Science (DAIMI), Aarhus University, 1999.

Technical Reports

Julien Brunel, Damien Doliguez, René Rydhof Hansen, Julia Lawall, Gilles Muller. A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking. Research report 08/2/INFO, Ecole des Mines de Nantes, July 2008.
Julia L. Lawall, Julien Brunel, René Rydhof Hansen, Henrik Stuart and Gilles Muller. WYSIWIB: A Declarative Approach to Finding Protocols and Bugs in Linux Code. Research report 08/1/INFO, Ecole des Mines de Nantes, July 2008.
Yoann Padioleau, René Rydhof Hansen, Julia Lawall, Gilles Muller. Towards Documenting and Automating Collateral Evolutions in Linux Device Drivers. INRIA Research Report RR-6090, January 2007.
René Rydhof Hansen. Hardest Attackers and Leaking References. SecSafe Project Report: SECSAFE-IMM-012.
René Rydhof Hansen and Igor A. Siveroni. Java Card Safety and Security through Static Analysis. SecSafe Project Report: SECSAFE-IMM-011.
René Rydhof Hansen. A Prototype Tool for JavaCard Firewall Analysis. SecSafe Project Report: SECSAFE-IMM-006.
René Rydhof Hansen. Implementing the Flow Logic for Carmel. SecSafe Project Report: SECSAFE-IMM-004.
René Rydhof Hansen. Extending the Flow Logic for Carmel. SecSafe Project Report: SECSAFE-IMM-003.
René Rydhof Hansen. Flow Logic for Carmel. SecSafe Project Report: SECSAFE-IMM-001.
René Rydhof Hansen. Java Bibliography. SecSafe Project Report: SECSAFE-DAIMI-004.
René Rydhof Hansen. Computer Security Bibliography. SecSafe Project Report: SECSAFE-DAIMI-003.