Ansgar Fehnker

Mail: Ansgar02a (32K)
   Locked Bag 6016
The University of NSW
Sydney NSW 1466
Australia
Office:
   Office E520
223 Anzac Parade
Kensington NSW 2052
Phone:
   +61 2 8306 0490
E-mail:
   ansgar at cse.unsw.edu.au
Research

I am a researcher at National ICT Australia in the Managing Complexity research theme. My research interest is formal verification, in particular model checking and static analysis, and the application of formal methods in design and development of embedded systems.

I am currently working on the Goanna, a tool for C/C++ that combines static analysis with model checking. This tools is the result of a NICTA research project also called Goanna. I previously also worked on the Pewna project that explored the use of formal method techniques, such as probabilistic model checking, for perfomance evaluation of wireless network applications.

Teaching
Together with Ralf Huuck I offer since 2006 the course COMP3153 - Algorithmic Verification at UNSW.
Benchmarks
Together with Franjo Ivančić I compiled a number of benchmarks for hybrid systems verification. The the instances and models can be found here.
Publications
M. Vistein, R. Huuck, F. Ortmeier, A. Fehnker, W. Reif. An Abstract Specification Language for Static Program Analysis. In SSV 2009. ENTCS, 2009 . (pdf)
A. Fehnker, R. Huuck, S. Seefried, and M. Tapp. Automatic Bug Detection in Microcontroller Software by Static Program Analysis. In SofSem 2009, LNCS 5404, Springer, 2009. (pdf)
S. Edelkamp, V. Schuppan, D. Bosnacki, A. Wijs, A. Fehnker, and H. Al- jazzar. Survey on Directed Model Checking. In MOCHART 2008, LNAI 5348, Springer, 2009. (pdf)
A. Fehnker, M. Fruth, and A. McIver. Graphical modelling for simulation and formalanalysis of wireless network protocols. MeMot 2007, Journal Version, LNCS 5454, 2009. (pdf).
A. Fehnker. Creating Correct Network Protocols - PhD Defence Oskar Wibling. Lecture - Uppsala University, December, 2008. (pdf).
A. Boulis, A. Fehnker, M. Fruth, and A. McIver. CaVi -- Simulation and Model Checking for Wireless Sensor Networks. Qest 2008. (pdf).
A. Fehnker, R. Huuck, F. Rauch and S. Seefried. Some Assembly Required -- Program Analysis of Embedded System Code. SCAM 2008. (pdf)
A. Fehnker, R. Huuck, S. Seefried and J. Brauer. Goanna: Syntactic Software Model Checking ATVA 2008. (pdf)
A. Fehnker, M. Fruth, and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. MeMot 2007. (pdf).
A. Fehnker, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Model Checking Software at Compile Time. TASE 2007. (pdf)
A. Fehnker, L. van Hoesel, and A. Mader. Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. IFM 2007. (pdf)
A. Fehnker and A. McIver. Formal Techniques for the Analysis of Wireless Networks. ISOLA 2006. (pdf)
A. Fehnker, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Goanna - A Static Model Checker. FMICS 2006. (pdf)
A. Fehnker and B. Krogh. Hybrid Systems Verification in is not a Sinecure, IJFCS, Vol. 17, No. 4, 2006. (pdf)
A. Fehnker and P. Gao. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. AdHocNow 2006 (pdf). AdHocNow Presentation (pdf)
A. Fehnker, E.M. Clarke, S. Jha and B.H. Krogh. Refining Abstractions of Hybrid Systems Using Counterexample Fragments. HSCC 2005. (pdf)
E.M. Clarke, A. Fehnker , S. Jha and Helmut Veith . Temporal logic model checking. In Handbook of Networked and Embedded Control Systems, pages 539--558. 2005
B. Aldrich, A. Fehnker, P.H. Feiler, Zhi Han, B.H. Krogh, E. Lim and S. Sivashankar, Managing Verification Activities Using SVM, ICFEM 2004. (pdf)
A. Fehnker and B. Krogh. Hybrid Systems Verification in is not a Sinecure, ATVA 2004. (pdf)
A. Fehnker. and F. Ivančić Benchmarks for Hybrid Systems Verification . Proc. HSCC'2004. (pdf). The web site with the instances can be found here.
O. Stursberg, A. Fehnker, Zhi Han, B. Krogh. Verification of a Cruise Control System using Counterexample-guided Search. Control Engineering Practice, 2004. (ps)
A. Fehnker, Miaomiao Zhang and F.W. Vaandrager. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. Third International Conference on Quality Software (QSIC 2003). Full version in M. Broy and M. Pizka, editors. Models, Algebras, and Logic of Engineering Software, Nato ASI Series III: Computer and Systems Sciences, Volume 191, pages 385-402, IOS Press, 2003. Also available as Technical Report NIII-R0308, University of Nijmegen, March 2003.
O. Stursberg, A Fehnker, Zhi Han, B. Krogh. Specification-Guided Analysis of Hybrid Systems using a Hierachy of Validation Methods.. Proc of the ADHS 2003.(ps)
E.M. Clarke, A Fehnker, Zhi Han, B. Krogh, J. Ouaknine, O. Stursberg, M. Theobald. Abstraction and Counterexample-guided Refinement of Hybrid Systems. International Journal of Foundations of Computer Science, Vol 14, Number 3. (pdf)
E.M. Clarke, A Fehnker, Zhi Han, B. Krogh, O. Stursberg, M. Theobald. Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. Proc. TACAS'2003.
Ansgar Fehnker, Citius, Vilius, Melius - Guiding and Cost-Optimality in Model Checking of Timed and Hybrid Systems, PhD thesis, KUNijmegen, 2002, (pdf)
E. Brinksma and A. Mader and A. Fehnker Verification and Optimization of a PLC Control Schedule , Int. Journal on Software Tools for Technology Transfer, 4 (1), pp. 21-33, 2002. (ps)
Kim Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas S. Hune, Paul Pettersson and Judi Romijn. As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata . CAV 2001. (ps)
Gerd Behrmann, Ansgar Fehnker, Thomas S. Hune, Kim Larsen, Paul Pettersson and Judi Romijn Efficient Guiding Towards Cost-Optimality in Uppaal. Proc. TACAS'2001. (ps)
Gerd Behrmann, Ansgar Fehnker, Thomas S. Hune, Kim Larsen, Paul Pettersson, Judi Romijn and Frits Vaandrager . Minimum-Cost Reachability for Linearly Priced Timed Automata. Proc. HSCC'2001. (ps)
Gerd Behrmann, Ansgar Fehnker, Thomas S. Hune, Kim Larsen, Paul Pettersson and Judi Romijn. Guiding and Cost-Optimality in Uppaal. AAAI Spring Symposium Model-Based Validation of Intelligence, 2001. (ps)
Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'Argenio, Alexandre David, Ansgar Fehnker, Thomas S. Hune, Bertrand Jeannet, Kim Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, and Wang Yi. UPPAAL - Now, Next, and Future. MOVEP'2k, LNCS Tutorial 2067, 2001. (ps)
Ansgar Fehnker. Scheduling a Steel Plant with Timed Automata. RTCSA'99, IEEE Computer Society Press, 1999. (pdf)
Henning Dierks, Ansgar Fehnker, Angelika Mader and Frits Vaandrager . Operational and Logical Semantics for Polling Real-Time Systems. Proc. FTRTFT'98, LNCS 1486, 1998. (ps)
Ansgar Fehnker. Automotive Control Revisited -- Linear Inequalities as Approximation of Reachable Sets.Proc. HSCC'98, LNCS 1386, 1998. (ps)
Ansgar Fehnker. Heuristic Reachability Analysis of Hybrid Systems. Draft, 2000. (ps)
Ansgar Fehnker. Bounding and Heuristics in forward reachability algorithms.Computing Science Institute Nijmegen, Tech. rep. CSI-R0002, 2000. (ps)
Ansgar Fehnker. Scheduling a Steel Plant with Timed Automata. Computing Science Institute Nijmegen, Tech. rep. CSI-R9910, 1999. (ps)
Henning Dierks, Ansgar Fehnker, Angelika Mader and Frits Vaandrager . Operational and Logical Semantics for Polling Real-Time Systems. Computing Science Institute Nijmegen, Tech. rep. CSI-R9813, 1998. (ps)
Ansgar Fehnker. Automotive Control Revisited Linear Inequalities as Approximation of Reachable Sets. Computing Science Institute Nijmegen, Tech. rep. CSI-R9723, 1997. (ps)
Ansgar Fehnker. Two Identification Methods for an Active Sludge Model. Master's Thesis, Rijksuniversiteit Groningen, 1996.
 
A short CV Miscellaneous
I was born 1971 in Teglingen, No 25. My office mate in Nijmegen was Mariëlle
Later, I went for four years to the primary school in Teglingen, and ... There is a link to my page on Mariekes homepage .
... spent 9 years on the secondary school Gymnasium Marianum in Meppen. I used to live in the ORKZ, first on station A2midden, later on station A2rechts. This is where I met Melanie.
I then left Teglingen to study Mathematics at the Philipps-Universität Marburg for two years ... In 1998 I made some predictions for our soccer pool with reasonable results.
... and continued studying Mathematics at the Rijksuniversiteit Groningen for four years. In the summer of 1999 I moved to Ravenstein, together with Melanie and our two cats (called Mies and Mowie).
I spent about 4 years in Nijmegen to work on my PhD. I lived in the Walnut Palace for one year. When Melanie came with the cats we moved to an apartment 2 blocks further on Walnut St.
From 2001 to 2004 I was a PostDoc at Carnegie Mellon University. Melanie and I married in 2003 in Sandfirden.
From 2004 on I work at NICTA. From 2009 involved with the Red Lizards. We (Melanie, Mowie, Mies and me) moved to Sydney .