Hanbing Liu/Professional

He studies in the broad field of the formal methods in software engineering. He is pariticularly interested machine virtualization technology, computing platform security.

His Ph.D.research focuses on techniques for program specification and verification with ACL2. (http://www.cs.utexas.edu/users/moore/acl2/)

For his Ph.D. dissertation project, he is working towards

• Formalize the JVM and its safety guarantee
• Construct a realistic safe "defensive" JVM and prove it is safe
• Check the correctness of the bytecode verifier:

For people who may want to get a quick overview about his work, his dissertation proposal presentation slides should be a good starting point: [/pub/proposal-slides.ps]. His actual dissertation proposal is availabe online at: [/pub/proposal.ps]. He is interested to hear from people's comments and suggestions on the proposed work.

Besides working on modeling and verifying the JVM and its bytecode verifier, he also did some preliminary work and case study in supporting Java program verification with ACL2.

Publications

• Formal Models of Java at the JVM Level A Survey from the ACL2 Perspective --- position paper, studying properties of Java program via its bytecode program. With J Strother Moore. Appeared in ECOOP 2001.

(http://www.cs.utexas.edu/users/moore/publications/jvm-models/full.ps.gz)

• Executable JVM model for analytical reasoning: a study --- executable JVM simulator with precise semantics suitable for reasoning mathematically. With J Strother Moore. Appeared in IVME 2003. An journal version appears in the Science of Computer Programming, Elsevier. 2005

(http://www.cs.utexas.edu/~hbl/publications/jvm-modeling/jvm-model.journal.pdf)

• Java Program Verification via a JVM Deep Embedding in ACL2 --- Proofs for two simple Java programs to illustrate the approach for verifying the correctness of Java programs. With J Strother Moore. Appeared in TPHOLS 2004.

(http://www.cs.utexas.edu/~hbl/publications/reasoning-about-java-programs/tphol.ps)

• A Solution to the Rockwell Challenge --- using ACL2 to reason about operations on low level data structures laid out in linear address memory (It may be extended to reason about mark and sweep operations used in a garbage collector). Appeared in ACL2 Workshop 2003.

(http://coldice.csres.utexas.edu/~hbl/currentwork/papers/rockwell-challenge/dynamic-hbl.ps)

Unpublished Drafts and Work in Progress

• A Verified CLDC JVM Class Loader in ACL2 --- describe the bootstrap class loader implementation in our JVM model. Explain how correctness of the class loader is formalized. Present the bootstrap class loader correctness specification and a mechanically checked proof. unpublished.

(http://www.cs.utexas.edu/~hbl/publications/unpublished/verified-class-loader/verified-class-loader.ps)

• CLDC JVM Bytecode Verifier and Its Formal Model in ACL2 -- describe the new JVM bytecode verification algorithm. describe the translation from official Prolog-like specification into implementations in ACL2. present one formal proof of a simple property of the bytecode verifier implementation.

(http://www.cs.utexas.edu/~hbl/publications/unpublished/bcv-modeling/modeling-BCV.ps)

• A Formal Study of the Java Bytecode Verification in ACL2 -- models the original iterative Bytecode verification algorithm. Present a proof that the bytecode verification of arbitrary bytecode method always terminates.

(http://www.cs.utexas.edu/~hbl/publications/unpublished/iterative-bcv/java-bcv-acl2.ps)

Global Read-only mode in effect. To edit, please check Preferences, replace the * with nihaox or "MF generic password" in the Administrator Password, click Save