Research

I am a member of NetDB@PENN

Research Interests

Applying formal methods to networking

Formally Verifiable Networking (Also available outdated declarative networking verification at DNV)

Logic and Logic programming

Static analysis and synthesis from algebraic specification; Linear logic and model checking

Tools I am playing with

Theorem provers PVS, Coq and tool Maude

Publication

1. Formally Verifiable Networking Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu. 8th Workshop on Hot Topics in Networks (ACM SIGCOMM HotNets-VIII), New York, Oct 2009 (16.0% acceptance) [Paper] [Talk] [ICNP'09 poster] [Extended PX talk]
2. A Theorem Proving Approach Towards Declarative Networking Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky, Prithwish Basu., (TPHOLs 2009) Emerging Trends Section, August, 2009 [Paper] [Talk] [Group picture]
3. Formalizing Metarouting in PVS Anduo Wang, Boon Thau Loo., Automated Formal methods (AFM 2009), co-located with CAV09, July, 2009. [Paper] [Talk] [TPHOLs'09 poster] [PVS codes]
4. Verifiable Policy-based Routing with DRIVER Anduo Wang, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, Prithwash Basu., University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-CIS-09-12. [Technical Report]
5. Declarative Network Verification Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky., Eleventh International Symposium on Practical Aspects of Declarative Languages (PADL), co-located with ACM's Principles of Programming Languages, Jan, 2009. [Paper] [Talk] [Extended Technical Report]
6. Formalizing a Component Model in PVS., Kung-Kiu Lau, Anduo Wang., Formalizing a Component Model in PVS, preprint 40, Technical Report, School of Computer Science, The University of Manchester, Nov 2006
7. A Component Based Approach to Verified Software., Kung-Kiu Lau, Zheng Wang, Anduo Wang, Ming Gu.,A Component Based Approach to Verified Software: What, Why, How And What Next?, 1st Asian Working Conference on Verified Software, October 2006
8. Verifying Java Programs By Theorem Prover HOL., Anduo Wang, Fei He, Ming Gu, Xiaoyu Song., Verifying Java Programs By Theorem Prover HOL, appeared in proceedings of the 30th Annual International Computer Software and Applications Conference, September 2006

Research Experience

• Member of Network Security and Distributed System Group, University of Pennsylvania, May 2008-present.
  • Develop formal specification of declarative networks based on proof-theoretic interpretation of logic programming, establish various correctness proof (optimality, cycle-free, convergence) of various network protocols (distance-vector and path-vector protocols)
  • Extend formal specification and verification of declarative networks to soft-states, where logical facts that expire over time are involved
• Member of Real Time System Group, University of Pennsylvania, Sep 2007 to May 2008.
• Visiting Research Assistant, Formal Methods Group, School of Computer Science, The University of Manchester, from Apr 2006 to Jan, 2007
  • Develop formal specification of the component model proposed by Dr. Lau in general purpose theorem prover PVS
  • Extend standard state-chart to specify component based system
• Research assistant, Formal Methods Group, School of Software, Tsinghua University, Sep 2004 to Aug 2006.
  • Verifying Java Programs with general-purpose theorem prover HOL, a first Java program verification use case developed in HOL

Professional Service

• Reviewer, Conference on emerging Networking EXperiments and Technologies (ACM CoNEXT), 2009
• Reviewer, International Conference on Data Engineering (ICDE), 2010
• Reviewer, Symposium on Principles of Programming Languages (POPL), 2008
• Reviewer, International Conference on Data Engineering (ICDE), 2008