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 (level B) at National ICT Australia in the Formal Methods group. My research interest is formal verification, in particular model checking, for timed and hybrid systems, and the application of formal methods in design and development of embedded systems.

I am involved in two research projects. Goanna is a project and a tool that combines static analysis and model checking techniques for source code analysis. Pewna is a project that explores the use of formal method techniques, such as model checking, for perfomance evaluation of wireless network applications.

Teaching
Together with Ralf Huuck I offered in 2006 the course COMP4151 - Algorithmic Verification at UNSW. This course will be continued in 2007 as COMP3153.
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.
Special Session at WPDRTS
Sriram Sankaranarayanan and I are chairing the special formal methods session at the Workshop on Parallel and Distributed Real-Time Systems (WPDRTS), held in conjunction with IDPDS in Long Beach, CA, 2007 .
Publications
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, Matthias 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, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Model Checking Software at Compile Time. TASE 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. We (Melanie, Mowie, Mies and me) moved to Sydney .