FehnkerA

Ansgar Fehnker

Researcher

Research Profile

I am a senior researcher at National ICT Australia in the Managing Complexity research theme. My research interest isformal verification, in particular model checking and staticanalysis, and the application of formal methods in design anddevelopment of embedded systems.

I am currently working on the Goanna, a tool for C/C++ thatcombines static analysis with model checking, and the Mesh Protocol project that explored the use of formal method techniques, such as probabilistic model checking, forthe analysis of wireless mesh network protocols.

Prior to joining NICTA I was a postdoc with Bruce Krogh and Edmund Clarke at Carnegie Mellon University. I received my PhD from the Radboud University Nijmegen, under the supervision of Frits Vaandrager.

From 2012 I will be joining the School of Computing, Informationand Mathematical Sciences at the University of the SouthPacific, and be a visiting researcher at NICTA.

Benchmarks

Together with FranjoIvančić I compiled a number of benchmarks forhybrid systems verification. Theinstances and models can be foundhere.

Contact

ansgar.fehnker@nicta.com.au

Publications

	A. Fehnker, R. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and Wee Lum Tan. A Process Algebra for Wireless Mesh Networks In ESOP 2012.
	A. Fehnker, R. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and Wee Lum Tan.Automated Analysis of AODV using UPPAAL In TACAS 2012.
	M. Vistein, R. Huuck, F. Ortmeier, A. Fehnker, W. Reif. AnAbstract Specification Language for Static Program Analysis. InSSV 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, andH. Al- jazzar. Survey on Directed Model Checking. In MOCHART2008, LNAI 5348, Springer, 2009. (pdf)
	A. Fehnker, M.Fruth, and A. McIver. Graphical modelling for simulation andformalanalysis of wireless network protocols. MeMot 2007,Journal Version, LNCS 5454, 2009. (pdf).
	A. Fehnker. Creating Correct Network Protocols - PhDDefence 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 ofEmbedded System Code. SCAM 2008. (pdf)
	A. Fehnker, R.Huuck, S. Seefried and J. Brauer. Goanna: Syntactic SoftwareModel Checking ATVA 2008. (pdf)
	A. Fehnker, M.Fruth, and A.McIver. Graphical modelling for simulation and formalanalysis 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 SensorNetworks. 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 - AStatic 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 withthe 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, MiaomiaoZhang and F.W.Vaandrager. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. Third International Conference on Quality Software (QSIC 2003). Fullversion in M. Broy and M. Pizka, editors. Models, Algebras, and Logic of Engineering Software, Nato ASI Series III: Computerand Systems Sciences, Volume 191, pages 385-402, IOS Press, 2003.Also available as Technical Report NIII-R0308, University ofNijmegen, 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 ADHS2003.(ps)
	E.M. Clarke, A. Fehnker, Zhi Han, B. Krogh, J. Ouaknine, O. Stursberg, M. Theobald.Abstraction and Counterexample-guided Refinement of HybridSystems. International Journal ofFoundations of Computer Science, Vol 14, Number 3. (pdf)
	E.M. Clarke, AFehnker, 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. Brinksmaand A. Mader and A. Fehnker Verification and Optimization of a PLC ControlSchedule , Int. Journal on Software Tools for TechnologyTransfer, 4 (1), pp. 21-33, 2002. (ps)
	Kim Larsen, Gerd Behrmann, Ed Brinksma, AnsgarFehnker, Thomas S.Hune, PaulPettersson and JudiRomijn. 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 TimedAutomata. Proc. HSCC'2001. (ps)
	Gerd Behrmann, AnsgarFehnker, Thomas S.Hune, Kim Larsen,Paul Pettersson and Judi Romijn. Guiding and Cost-Optimality in Uppaal. AAAI Spring SymposiumModel-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 Tutorial2067, 2001. (ps)
	Ansgar Fehnker. Scheduling aSteel Plant with Timed Automata. RTCSA'99, IEEE ComputerSociety Press, 1999. (pdf)
	Henning Dierks, Ansgar Fehnker, Angelika Mader and Frits Vaandrager .Operational and Logical Semantics for Polling Real-TimeSystems. 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 InstituteNijmegen, 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.