Ralf Huuck

NICTA Senior Researcher,
Senior Lecturer, CSE, UNSW
CTO & co-Founder, Red Lizard Software

I am a project leader in the Software Systems Group at NICTA and I am heading the research and development of the Goanna tool that combines model checking with static analysis for C/C++ source code analysis. Goanna is available commercially as well as for academic use.

Previously, I worked at the University of New South Wales, Australia, together with Kai Engelhardt and Ron von der Meyden on the refinement synchronous agents with knowledge and time; I held several visiting researcher positions at VERIMAG, Grenoble, with Yassine Lakhnech, at AIST, Tokyo, with Cyrille Artho, and at HKBU, Hong Kong, with Wei Wong. I received my PhD in theoretical computer science in the group of Willem-Paul de Roever at the University of Kiel, Germany, in 2003.

---

NEW: Check out the Goanna tool at http://www.redlizards.com

---

NEW: read about DIY Security Testing as part of a recent interview series with the Sydney Morning Herald.

---

NEW: FTSCS 12: International Workshop on Formal Techniques for Safety-Critical Systems
NEW: Conference on Systems Software Verification 2012 (SSV)

---

Research Areas

My main research interests are in the formal analysis and verification of large scale real-life
embedded systems. This includes working on tools an techniques related to model checking,
abstract interpretation, SMT solving and static analysis. Applications areas are software
bug detection, automated quality assurance and software security.

Funding and Principle Investigator

• Goanna

  Novel solution for model checking based static analysis of industrial C/C++ code to detect previously unknown security vulnerabilities and serious software bugs. Now available for academic and commercial customers. Funded by NICTA.

• BugMT

  Australian Academy of Science grant to discover software bugs in large scale complex multi-threaded code. Principle investigation on run-time verification and static analysis together with Cyrille Artho, AIST, Japan.

• SoftSpez

  German DFG funded project on developing formal analysis techniques for industrial control systems. Outcomes include the first complete formal semantics for the SFC and IL programming languages as used in industrial controllers (PLCs) and automated verification tools for both languages. Joint work with the Process Dynamics and Operations lead group by Sebatian Engell, Dortmund, Germany.

• KONDISK

  German DFG funded project that developed new automata theoretic approaches for the specification and verification of discrete-continuous systems. Joint work with the Process Dynamics and Operations group lead by Sebatian Engell, Dortmund, Germany.

• VHS

  European ESPRIT project on the Verification of Hybrid Systems. Developed automata based models for hybrid systems analysis and applied work on a number of industrial case studies. I have been an investigator only in this multi-national large scale project.

Staff and Students

I have had the pleasure to work with a number of great staff and students I (co-)supervised. Below a list of a selected few and their last known whereabouts. If you feel you belong to the list and I forgot, please email me.

Students

• Spas Bojanov (Google, US)
• Joerg Brauer (RWTH Aachen, Germany)
• Christian Breil (University of Augsburg, Germany)
• Clemens Dubslaff (TU Dresden, Germany)
• Maximilian Junker (TU Munich, Germany)
• Jakob Mund (TU Munich, Germany)
• Stefan Rinderle (Zühlke, Germany)
• Wolf Roediger (TU Munich, Germany)
• Michael Viestein (University of Augsburg, Germany)
• Andreas Vogelsang (TU Munich, Germany)

Staff

• David Crawshaw (Google, US)
• Felix Rauch (Google, Australia)
• Sean Seefried (NICTA, Australia)
• Paul Steckler (US)
• Lee Sun (Goldman Sachs, US?)

Other Activities

Apart from the usual reviewing and PC activities I am a:

• Steering Committee Member for the internal workshop on Systems Software verification (SSV)
• reviewer for the Deutsche Forschungsgesellschaft (DFG), Germany
• reviewer for the Netherlands Organisation for Scientific Research (NWO), Netherlands
• member of the IEEE

Contact Me

Office: Room E523, L5 Building, UNSW campus

Phone: +61 2 8306 0493

Fax: +61 2 8306 0405

Email: ralf.huuck@nicta.com.au

Mail:

National ICT Australia Limited

University of NSW, Locked Bag 6016,

NSW 1466, Australia

For urgent matters it is better to email instead of phoning me!

Publications

Find an up-to-date list of my publications.

---

Ralf Huuck
Formal Verification, Engineering and Business Value
Proceedings of Formal Techniques for Safety-Critical Systems (FTSCS 12) Kyoto, Japan, November 12-16, 2012. To appear in Electronic Proceedings in Theoretical Computer Science.

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck
Model Checking Driven Static Analysis for the Real World
Journal of Innovations in Systems and Software Engineering Springer-Verlag, doi:10.1007/s11334-012-0192-5, pages 1-12, August 2012.

Paper: [PDF file]

---

Maximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp
SMT-Based False Positive Elimination in Static Program Analysis
Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM 2012) Kyoto, Japan, November 12-16, 2012. Lecture Notes in Computer Science, Volume 7635, pages 316-331.

Paper: [PDF file]

---

Mark Bradley, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, Ralf Huuck
GoannaSMT - A Static Analyzer with SMT-based Refinement
Proceedings Tools for Automatic Program AnalysiS (TAPAS 2012) Deauville, France, December 2012. Tool presenation

Paper: [PDF file]

---

Mark Bradley, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, Ralf Huuck
High Performance Static Analysis for Industry
Proceedings Tools for Automatic Program AnalysiS (TAPAS 2012) Deauville, France, December 2012. Electronic Notes in Theoretical Computer Science (ENTCS), Volume 289, Pages 3-14

Paper: [PDF file]

---

Ralf Huuck, Ansgar Fehnker, and Rodiger Wolf
Model Checking Dataflow for Malicious Input
Proceedings of the 6th Workshop on Embedded Systems Security Taipei, Taiwan, Oct 2011. ACM, Article 4, 10 pages, ISBN: 978-1-4503-0819-9

Paper: [PDF file]

---

Mark Bradley, Ansgar Fehnker, Ralf Huuck, and Paul Steckler
Goanna Static Analysis at the NIST Static Analysis Tool Exposition
Report on the Third Static Analysis Tool Exposition (SATE 2010) U.S. National Institute of Standards and Technology (NIST) Special Publication (SP) 500-283, October, 2011.

Paper: [PDF file]

---

Mark Bradley, Ansgar Fehnker, and Ralf Huuck
Cyber security at software development time
Proceedings of the IEEE Defense Science Research Conference and Expo (DSR), 2011 Singapore, Aug 3-5 2011. IEEE, ISBN: 978-1-4244-9276-3

---

Andreas Vogelsang, Ansgar Fehnker, Ralf Huuck and Wolfgang Reif
Software Metrics in Static Program Analysis
12th International Conference on Formal Engineering Methods (ICFEM 2010) Lecture Notes in Computer Science, 2010, Volume 6447/2010, 485-500

Paper: [PDF file]

---

Kai Engelhardt, Ralf Huuck
Smaller Abstractions for ACTL* without Next
In the Festschrift of Correctness, Concurrency, and Compositionality for Willem-Paul de Roever, Lecture Notes in Computer Science, 2010, Volume 5930, Pages 250-259

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck, Sean Seefried
Counterexample Guided Path Reduction for Static Program Analysis
In the Festschrift of Correctness, Concurrency, and Compositionality for Willem-Paul de Roever, Lecture Notes in Computer Science, 2010, Volume 5930, Pages 322-341

Paper: [PDF file]

---

Michael Vistein, Frank Ortmeier, Wolfgang Reif, Ralf Huuck, Ansgar Fehnker
An Abstract Specification Language for Static Program Analysis
4th International Workshop on Systems Software Verification (SSV 2009) Electronic Notes in Theoretical Computer Science (ENTCS) Volume 254, Pages 181-197, October, 2009

Paper: [PDF file] Volume 254, Pages 65-83, October, 2009

---

Jörg Brauer, Ralf Huuck and Bastian Schlich
Interprocedural Pointer Analysis in Goanna
4th International Workshop on Systems Software Verification (SSV 2009) Electronic Notes in Theoretical Computer Science (ENTCS)

Paper: [PDF file] Volume 254, Pages 65-83, October, 2009

---

Ansgar Fehnker, Ralf Huuck, Sean Seefried, Michael Tapp
Fade to Grey: Tuning Static Program Analysis
3rd International Workshop on Harnessing Theories for Tool Support in Software (TTSS'09) Electronic Notes in Theoretical Computer Science (ENTCS) Volume 266, pp. 17-32 October, 2010.

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck and Sean Seefried
Incremental False Path Elimination for Static Software Analysis
ATVA '09 Proceedings of the 7th International Symposium on Automated Technology for Verification and AnalysisLecture Notes in Computer Science, 2009, Volume 5799/2009.

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck, Bastian Schlich, and Michael Tapp
Automatic Bug Detection in Microcontroller Software by Static Program Analysis
35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), January 24-30, 2009, Czech Republic

Paper: [PDF file]

---

Ansgar Fehnker, Joerg Brauer, Ralf Huuck, Sean Seefried
Goanna: Syntactic Software Model Checking
6th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 20-23, 2008 Seoul, Korea.

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck, Felix Rauch, Sean Seefried
Some Assembly Required - Program Analysis of Embedded System Code
Proceedings of the Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 28th-29th September 2008, Beijing, China

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck, Felix Rauch and Sean Seefried
Analysing Embedded System Software
Proceedings of C/C++ Verification Workshop, Oxford, UK, July, 2007

Extended Abstract: [PDF file]

---

Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch
Model checking software at compile time
Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, Shanghai, China, June, 2007

Paper: [PDF file]

---

Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch
Goanna - A Static Model Checker In the proceedings of 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), Bonn, Germany, August, 2006.

Paper: [PDF file]

---

Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco.
L4cars. In the proceedings of Embedded Security in Cars (escar 2005), Cologne, Germany, November, 2005.

Paper: [PDF file]

---

Gerwin Klein, Ralf Huuck
High Assurance System Software. In: Tony Cant (ed), Proc. 10th Australian Workshop on Safety Critical Systems and Software (SCS'05), Conferences in Research and Practice in Information Technology, 55, 2005.

---

Ralf Huuck
Semantics and Analysis of Instruction List Programs
Proceedings of the Second Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2004). Electronic Notes in Theoretical Computer Science 115, Elsevier, pages 3-18, January 2005.

Paper: [PDF file]

---

Nanette Bauer, Ralf Huuck, Ben Lukoschus, Sebastian Engell.
A Unifying Semantics for Sequential Function Charts.
Integration of Software Specification Techniques for Applications in Engineering, Priority Program SoftSpez of the German Research Foundation (DFG), Final Report. Lecture Notes in Computer Science 3147, Springer 2004, pages 400-418. ISBN 3-540-23135-8

Paper: [Link to Electronic Version]

---

Nanette Bauer, Sebastian Engell, Ralf Huuck, Sven Lohmann, Ben Lukoschus, Manuel Remelhe, Olaf Stursberg.
Verification of PLC Programs given as Sequential Function Charts.
Integration of Software Specification Techniques for Applications in Engineering, Priority Program SoftSpez of the German Research Foundation (DFG), Final Report. Lecture Notes in Computer Science 3147, Springer 2004, pages 517-540. ISBN 3-540-23135-8

Paper: [Link to Electronic Version]

---

Nanette Bauer, Ralf Huuck, Sven Lohmann, Ben Lukoschus.
Sequential Function Charts: Die Notwendigkeit formaler Analyse.
atp - Automatisierungstechnische Praxis, pages 61-67. Oldenbourg Wissenschaftsverlag, August 2004. ISSN 0178-2320.

---

Ralf Huuck
Software Verification for Programmable Logic Controllers
Dissertation, Institute of Computer Science and Applied Mathematics, University of Kiel, April 17, 2003.

Electronic Version [PDF file]

---

Ralf Huuck, Ben Lukoschus, Nanette Bauer.
A Model-Checking Approach to Safe SFCs.
CESA 2003: IMACS Multiconference on Computational Engineering in Systems Applications, Lille, France, July 9-11, 2003. ISBN 2-9512309-5-8.

Paper (updated version): [PDF file]

---

Ralf Huuck
Software Verification for Embedded Systems.
In the Proceedings of MMAR '02: The 8th IEEE International Conference on Methods and Models in Automation and Robotics, Szczecin, Poland, 2-5 September 2002

Paper: [PDF file]

---

Ralf Huuck, Ben Lukoschus, Goran Frehse, and Sebastian Engell
Compositional Verification of Continuous-Discrete Systems
Modelling, Analysis and Design of Hybrid Systems, Lecture Notes in Control and Information Sciences 279, pages 225-246. Springer-Verlag, 2002. ISBN 3-540-43812-2

---

Goran Frehse, Olaf Stursberg, Sebastian Engell, Ralf Huuck, Ben Lukoschus.
Modular Analysis of Discrete Controllers for Distributed Hybrid Systems.
b '02: The XV. IFAC World Congress, Barcelona, Spain, July 21-26, 2002.

Paper: [PDF file]

---

Nanette Bauer, Ralf Huuck, Ben Lukoschus
A grenatch Semantics for Hybrid Controllers.
b '02: The XV. IFAC World Congress, Barcelona, Spain, July 21-26, 2002.

Paper: [ gzip-compressed PostScript]

---

Nanette Bauer, Ralf Huuck
A Parameterized Semantics for Sequential Function Charts.
In the proceedings of SFEDL (Semantic Foundations of Engineering Design Languages) 2002, Satellite Event of ETAPS 2002, 6-14.4.2002, pages 69-83.

Paper: [ gzip-compressed PostScript]

---

Nanette Bauer, Ralf Huuck
Towards Automatic Verification of Embedded Control Software
APAQS 2001: IEEE Asian Pacific Conference on Quality Software, Hong Kong, December 10-11, pages 375-383, 2001. ISBN 0-7695-1287-9.

Paper: [gzip-compressed PostScript]

---

Ralf Huuck, Ben Lukoschus, Yassine Lakhnech.
Verifying Untimed and Timed Aspects of the Experimental Batch Plant.
European Journal of Control, 7(4):400-415, September 2001. Special Issue: Verification of Hybrid Systems - Results of a European Union Esprit Project. Hermes Science Publishing. ISSN 0947-3580.

Paper: [gzip-compressed PostScript]

---

Goran F. Frehse, Olaf Stursberg, Sebastian Engell, Ralf Huuck, Ben Lukoschus.
Verification of Hybrid Controlled Processing Systems based on Decomposition and Deduction.
ISIC 2001: 2001 IEEE International Symposium on Intelligent Control, Mexico City, Mexico, September 5-7, 2001, pages 150-155. IEEE Press. ISBN 0-7803-6733-2 (CD-ROM: 0-7803-6735-9).

Paper: [gzip-compressed PostScript]

---

Stefan Kowalewski, Peter Herrmann, Sebastian Engell, Heiko Krumm, Heinz Treseler, Yassine Lakhnech, Ralf Huuck, Ben Lukoschus.
Approaches to the Formal Verification of Hybrid Systems.
at-Automatisierungstechnik, 49(2):66-74, February 2001. Special Issue: Hybrid Systems II: Analysis, Modeling, and Verification. Oldenbourg Verlag. ISSN 0178-2312.

Paper: [gzip-compressed PostScript]

---

Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
Utilizing Static Analysis for Programmable Logic Controllers.
ADPM 2000: The 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, Dortmund, Germany, September 18-19, 2000, pages 183-187, Aachen, Germany, 2000. Shaker Verlag. ISSN 0945-4659, ISBN 3-8265-7836-8.

Paper: [gzip-compressed PostScript]

---

Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
An Abstract Model for Sequential Function Charts.
Discrete Event Systems: Analysis and Control, Proceedings of WODES 2000: 5th Workshop on Discrete Event Systems, Ghent, Belgium, August 21-23, 2000, pages 255-264, Boston, Dordrecht, London, 2000. Kluwer Academic Publishers. ISBN 0-7923-7897-0.

Paper: [gzip-compressed PostScript]

---

Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
Verification of Sequential Function Charts using SMV.
PDPTA 2000: International Conference on Parallel and Distributed Processing Techniques and Applications, Monte Carlo Resort, Las Vegas, Nevada, USA, June 26-29, 2000, volume V, pages 2987-2993. CSREA Press, June 2000. ISBN 1-892512-51-3.

Paper: [gzip-compressed PostScript]

---

Sébastien Bornot, Ralf Huuck, Ben Lukoschus.
Statische Analysetechniken für speicherprogrammierbare Steuerungen.
FBT 2000: 10. GI/ITG-Fachgespräch: Formale Beschreibungstechniken für verteilte Systeme, Lübeck, Germany, June 22/23, 2000, pages 175-181, Aachen, Germany, June 2000. Shaker Verlag. ISSN 0945-0807, ISBN 3-8265-7491-5.

Paper: [gzip-compressed PostScript]

---

Ralf Huuck, Yassine Lakhnech, Ben Lukoschus, Luis Urbina, Sebastian Engell, Stefan Kowalewski, and Jörg Preußig.
Integrating Timed Condition/Event Systems and Timed Automata for the Verification of Hybrid Systems.
Parallel and Distributed Computing Practices, 1(2):45-60, June 1998.

Paper: [gzip-compressed PostScript]

---

Stefan Kowalewski, Sebastian Engell, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus, and Luis Urbina.
Using Model-Checking for Timed Automata to Parameterize Logic Control Programs.
8th European Symposium on Computer Aided Process Engineering (ESCAPE8), Brugge, Belgium, May 1998.
Proceedings appear in Computers and Chemical Engineering.

Paper: [gzip-compressed PostScript]

---

Ralf Huuck.
Transforming Timed Condition/Event Systems into Timed Automata: An Approach to Automatic Verification.
Master's Thesis, Christian-Albrechts-Universität zu Kiel, Germany, June 1998.

Paper: [gzip-compressed PostScript]

---

Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski and Jörg Preußig. Comparing Timed C/E Systems with Timed Automata.
Proceedings Int. Workshop on Hybrid and Real-Time Systems (HART'97), Grenoble, Frankreich, March 26-28, 1997, Lecture Notes in Computer Science 1201, Springer, pp. 81-86

Paper: [ gzip-compressed PostScript]

---

Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski and Jörg Preußig.
Combining a Computer Science and a Control Theory Approach to the Verification of Hybrid Systems.
5th Int. Workshop on Parallel and Distributed Real-Time Systems (WPDRTS'97), Geneva, Switzerland, April 1-3,1997, IEEE Computer Society, ISBN 0-8186-8096-2/97.

Paper: [ gzip-compressed PostScript]

---

Stefan Kowalewski, Jörg Preußig, Sebastian Engell, Ralf Huuck, Yassine Lakhnech, and Ben Lukoschus.
Analyse zeitbewerteter Bedingung/Ereignis-Systeme mittels Echtzeitautomaten-Tools.
5. Fachtagung Entwurf komplexer Automatisierungssysteme (EKA '97), 1:180-194, Braunschweig, Germany, May 1997.

More Stuff

To learn more about me, my other homepage is probably a good start