Ansgar Fehnker

Mail: Ansgar
P.O. Box 217
7500 AE Enschede
The Netherlands
Office:
Zilverling 3120
University of Twente
Enschede
The Netherlands
Phone:
+31 53 489 2583
E-mail:
ansgar.fehnker@utwente.nl
Work

I am Associate Professor for Programming Education at the Faculty of Electrical Engineeering, Mathematics, and Computer Science, at the University of Twente. I am part of the Formal Methods and Tools group.

Bio

I was previously professor in CS/IS and Head of School at the School of Computing, Information and Mathematical Science (SCIMS) at the University of the South Pacific. I was until 2011 researcher at Australia's ICT research centre NICTA, where I on static analysis for C/C++, which led to the commercial industrial analysis tool Goanna, and on analysis of wireless network protocols with model checking. Prior to joining NICTA I was a PostDoc in the model checking teams at Carnegie Mellon University. He received his PhD from the Radboud University Nijmegen on verification of real-time and hybrid systems.

Research

My research interest is formal verification, in particular model checking and static analysis, and the application of formal methods in design and development of software systems.

PhD and MSc projects

Please contact me if you are interested in pursuing a PhD or MSc in the areas of formal methods, software analysis, protocol analysis, tertiary teaching of programming.

Benchmarks and Models
  • Together with Franjo Ivančić I compiled a number of benchmarks for hybrid systems verification. The instances and models can be found here.
  • Together with Angelika Mader and Lodewijk van Hoesel we modelled the LMAC protocol. The models and properties can be found here.
  • Together with Vinay Mahta and Maryam Kamali we modelled mobility in Wireless Netowrks. The models and properties can be found here.
Publications
  • Davis, M., Fehnker, A., McIver, A., Voronkov, A. (Eds.) Logic for Programming, Artificial Intelligence, and Reasoning 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings.
  • K. Chaudhary, and A. Fehnker, Model Checking a Server-Side Micro Payment Protocol FMICS 2015, 2015, (link)
  • K. Chaudhary, and A. Fehnker, Modeling and verification for the server-side Netpay protocol APWCCSE 2014, 2014, (link)
  • R. Huuck, A. Fehnker, P. Jayet and F. Rauch. Generating a transition system for use with model checking US Patent 8,850,415. 2014. (link)
  • R. Huuck, C. Artho, A. Fehnker and J. Mund. The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis. In ATVA 2013. URL (link)
  • A. Fehnker,R. van Glabbeek, P. Höfner, A. McIver, M. Portmann and Wee Lum Tan, A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV 2013, (link)
  • A. Fehnker, P. Hoefner, M. Kamali and V. Mehta. Topology-Based Mobility Models for Wireless Networks. In QEST 2013. (link)
  • A. Fehnker, and R. Huuck. Model checking driven static analysis for the real world: designing and tuning large scale bug detection. ISSE 9(1): 45-56, 2013. (link)
  • M. Bradley, F. Cassez, A. Fehnker, Th. Given-Wilson, and R. Huuck: High Performance Static Analysis for Industry. Electr. Notes Theor. Comput. Sci. 289: 3-14, 2012. (link)
  • C. Dubslaff and A. Fehnker. Inter-procedural analysis of computer programs US 20110209126 A1, 2012. (link)
  • M. Junker, R. Huuck, A. Fehnker, and A. Knapp. SMT-Based False Positive Elimination in Static Program Analysis. ICFEM 2012: 316-331, 2012 (link)
  • P. Höfner, R. van Glabbeek, Wee Lum Tan, M. Portmann, A. McIver, and Ansgar Fehnker. A rigorous analysis of AODV and its variants. MSWiM 2012: 203-212, 2012. (link)
  • A. Fehnker, R. J. van Glabbeek, P. Höfner A. McIver, M. Portmann, W. L. Tan. A Process Algebra for Wireless Mesh Networks. In ESOP 2012. 2012. (link)
  • A. Fehnker, R. J. van Glabbeek, P.Höfner, A. McIver, M. Portmann, W. L. Tan. Automated Analysis of AODV using UPPAAL. In TACAS 2012. 2012. (link)
  • M. Bradley, A. Fehnker, and R. Huuck. Goanna Static Analysis at the NIST Static Analysis Tool Exposition. National Institute for Standards and Technology (NIST) special report, Gaithersburg, MD, 2011. (link)
  • A. Fehnker, R. van Glabbeek, P. Höfner A. McIver, M. Portmann, and Wee Lum Tang. Modelling and Analysis of AODV in UPPAAL. In WRIPE 2011. 2011. URL (link)
  • R. Huuck, A. Fehnker, and W. Roediger. Model Checking Dataflow for Malicious Input. In WESS 2011. 2011. URL (link)
  • M. Bradley, A. Fehnker, and R. Huuck. Cyber Security at Software Development Time. Defense Science Research Conference and Expo (DSR). 2011. (link)
  • A. Fehnker, R. Huuck and A. Vogelsang and W. Reif. Software Metrics in Static Program Analysis. In ICFEM 2010. LNCS, 2010. URL (link)
  • A. Fehnker, R. Huuck and S. Seefried. Counterexample Guided Path Reduction for Static Program Analysis. In Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever. LNCS 5930, pages 322--341. Springer. 2010. (link)
  • A. and R. Bakhshi. On the Impact of Modelling Choices for Distributed Information Spread -- A Comparative Study. In \emph(QEST 2009). LNCS, 2009. (link)
  • A. Fehnker, M. Fruth, and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. In Methods, Models and Tools for Fault Tolerance. Extended Version, LNCS 5454, Springer,2009. (link)
  • A. Fehnker, R. Huuck, S. Seefried and M. Tapp. Fade to Grey: Tuning Static Program Analysis. In TTSS 2009. ENTCS, 2009. URL (link)
  • A. Fehnker, R. Huuck, and S. Seefried. Incremental False Path Elimination for Static Software Analysis. In ATVA 2009. LNCS 5799, 2009. (link)
  • M. Vistein, R. Huuck, F. Ortmeier, A. Fehnker, and W. Reif. An Abstract Specification Language for Static Program Analysis. In SSV 2009. ENTCS 254, 2009 URL (link)
  • 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. (link)
  • S. Edelkamp, V. Schuppan, D. Bosnacki, A. Wijs, A. Fehnker, and H. Aljazzar. Survey on Directed Model Checking. In MOCHART 2008 LNAI 5348, Springer, 2009. URL (link)
  • A. Boulis, A. Fehnker, M. Fruth, and A. McIver. CaVi -- Simulation and Model Checking for Wireless Sensor Networks. In QEST 2008. IEEE Computer Society, 2008. (link)
  • A. Fehnker, R. Huuck, F. Rauch and S. Seefried. Some Assembly Required -- Program Analysis of Embedded System Code. In SCAM 2008. IEEE Computer Society, 2008. (link)
  • A. Fehnker, R. Huuck, S. Seefried and J. Brauer. Goanna: Syntactic Software Model Checking. In ATVA 2008. LNCS 5311, Springer, 2008. (link)
  • A. Fehnker, M. Fruth, and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. MeMot 2007. (link)
  • A. Fehnker, R. Huuck, F. Rauch, and S. Seefried. Analysing Embedded Software. In C/C++ Verification Workshop. Tech. Report ICIS-R07015, Radboud University Nijmegen, 2007. (link)
  • A. Fehnker, L. van Hoesel, and A. Mader. Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In IFM 2007 LNCS 4591, Springer, 2007. (link)
  • A. Fehnker, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Model Checking Software at Compile Time. In TASE 2007 IEEE Computer Society, 2007. URL (link)
  • A. McIver and A. Fehnker. Formal techniques for the analysis of wireless networks. In Isola 2006 IEEE on-site proceedings, 2006.(link)
  • A. Fehnker and B. Krogh. Hybrid Systems Verification is not a Sinecure International Journal of Foundations of Computer Science Vol. 17, No. 4, 2006. (link)
  • A. Fehnker, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Goanna - A Static Model Checker. In FMICS 2006 LNCS 4346, Springer, 2006. (link)
  • A. Fehnker and P. Gao. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In AdHocNow LNCS 4104, Springer, 2006. URL (link)
  • E. Clarke, A. Fehnker, S. Kumar Jha, and H. Veith. Temporal logic model checking. In Handbook of Networked and Embedded Control Systems pages 539--558. 2005. (link)
  • A. Fehnker, E. Clarke, S. Jha, and B. Krogh. Refining abstractions of hybrid systems using counterexample fragments. In HSCC 2005 LNCS 3414, Springer, 2005. (link)
  • A. Fehnker and B. Krogh. Hybrid system verification is not a sinecure: The electronic throttle control case study. In Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC.. LNCS 3299, Springer, 2004. URL (link)
  • A. Fehnker and F. Ivancic. Benchmarks for hybrid systems verification. In Proc. of HSCC'04. LNCS 2993, Springer, 2004. (link)
  • B. Aldrich, A. Fehnker, P. Feiler, Zhi Han, B. Krogh, E. Lim, and S. Sivashankar. Managing verification activities using SVM. In Sixth International Conference on Formal Engineering Methods (ICFEM). LNCS 3308, Springer, 2004. (link)
  • O. Stursberg, A. Fehnker, Zhi Han, and B. Krogh. Verification of a cruise control system using counterexample-guided search. Control Engineering Practice 12:1269--1278, 2004. (link)
  • E. Clarke, A. Fehnker, Z. Han, B. Krogh, J. Ouaknine, O. Stursberg, and M. Theobald. Abstraction and counterexample-guided refinement in model checking of hybrid systems. International Journal of Foundations of Computer Science 14(4):583--604, 2003. (link)
  • Miaomiao Zhang A. Fehnker and F.W. Vaandrager. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. In Third International Conference on Quality Software (QSIC 2003). IEEE Computer Society Press, 2003. (link)
  • Miaomiao Zhang A. Fehnker and F.W. Vaandrager. Nato ASI Series III: Computer and Systems Sciences volume 191, chapter Modeling and Verifying a Lego Car Using Hybrid I/O Automata pages 385--402. IOS Press, 2003. (link)
  • O. Stursberg, A. Fehnker, Zhi Han, and B. Krogh. Specification-guided analysis of hybrid systems using a hierachy of validation methods. In Proc. IFAC Conference ADHS. Elsevier, 2003. (link)
  • E. Clarke, A. Fehnker, Z. Han, B. Krogh, O. Stursberg, and M. Theobald. Verification of hybrid systems based on counterexample-guided abstraction refinement. In Proc. $9^th$ Int. Conf. TACAS volume 2619 of LNCS pages 192--207. Springer, 2003. (link)
  • A. Fehnker. Citius, Vilius, Melius -- Guiding and Cost-Optimality in Model Checking of Timed and Hybrid Systems. PhD thesis, University of Nijmegen, 2002. (link)
  • E. Brinksma, A. Mader, and A. Fehnker. Verification and optimization of a PLC control schedule. International Journal on Software Tools for Technology Transfer, 4(1):21--33, 2002. (link)
  • G. Behrmann, A. Fehnker, T.S. Hune, K.G. Larsen, P. Petterson, J.M.T. Romijn, and F.W. Vaandrager. Minimum-Cost Reachability for Linearly Priced Timed Automata. In 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'2001) LNCS 2034, Springer, 2001. (link)
  • G. Behrmann, A. Fehnker, T.S. Hune, K.G. Larsen, P. Petterson, and J.M.T. Romijn. Efficient Guiding Towards Cost-Optimality in UPPAAL. In TACAS'2001 LNCS 2031, Springer, 2001. (link)
  • K.G. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T.S. Hune, P. Petterson, and J.M.T. Romijn. As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In 13th Conference on Computer Aided Verification (CAV'01) LNCS 2102, Springer, 2001. (link)
  • G. Behrmann, A. Fehnker, T.S. Hune, K.G. Larsen, P. Petterson, and J.M.T. Romijn. Guiding and Cost-Optimality in UPPAAL. In The 2001 AAAI Spring Symposium Series: Model-Based Validation of Intelligence. AAAI, 2001. URL (link)
  • T. Amnell, G. Behrmann, J. Bengtsson, P.R. D'Argenio, A. David, A. Fehnker, T.S. Hune, B. Jeannet, K.G. Larsen, M.O. M\ouml;ller, P. Pettersson, C. Weise, and W. Yi. UPPAAL - Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. Ryan, editors, Modelling and Verification of Parallel Processes (MOVEP'2k) LNCS 2067, Springer, 2001. (link)
  • A. Fehnker. Bounding and Heuristics in forward reachability algorithms. Technical Report CSI-R0002, Computing Science Institute Nijmegen, 2000. (link)
  • A. Fehnker. Scheduling a Steel Plant with Timed Automata. In Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99). IEEE Computer Society Press, 1999. (link)
  • A. Fehnker. Automotive control revisited -- Linear inequalities as approximation of reachable sets. In HSCC '98 LNCS 1386, Springer, April 1998. (link)
  • H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In A.P. Ravn and H. Rische, editors, Proceedings FTRTFT'98 LNCS 1486, Springer, 1998. (link)
  • A. Fehnker. Two identification methods for an active sludge model. Master's thesis, Rijksuniversiteit Groningen, 1996. (link)