Hanbing Liu graduated with a Ph.D. in Computer Science from University of Texas at Austin in 2006
He works at AMD since graduation, verifying and (more recently) designing floating point data path unit. He also maintains and develops the multiprocessor coherence/consistency checker and memory model for x86 and arm architecture.
At UT, he used ACL2 (http://www.cs.utexas.edu/users/moore/acl2/)
to formalize the JVM and its bytecode verifier. His current focus is on formalizing and proving
the correctness of the bytecode verification specification as described in JSR139.
Also at UT, he also did some preliminary work in Java program verification by studying
the executions of the corresponding bytecode programs on their JVM models.
Publications
- [http://www.cs.utexas.edu/users/moore/publications/jvm-models/full.ps.gz 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.
- Executable JVM model for analytical reasoning: a study --- executable JVM simulator with precise semantics suitable for reasoning mathematically. With J Strother Moore
- 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.
- 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).
He has been a member of MeltonFoundation (http://www.meltonfoundation.org) since 1996.
He has a private wiki since Oct. 2002. (http://zu.meltonfoundation.org/cgi-bin/wiki.pl?Hanbing_Liu)
I like the mods you did to UseModWiki. Did you use Usemod 1.0? Is your version available?
I did some hacks to the 0.92 that comes with Debian.
- I changed upload.pl from Andrew Gray <andrew@andrewgray.uklinux.net> so that it posts an entry to the Uploads page
- I changed wiki.pl to add an interface for me to write extensions (mostly in Python).
- List of things on http://zu.meltonfoundation.org/cgi-bin/wiki.pl?WikiDevelopment are mostly written as external python scripts that are invoked via wiki.pl's hack.
I should say those are ugly hacks. It will take some efforts to adapt it to some other site. I don't know if someone still want it. I can make it available.
CategoryHomePage RecentChanges
Hanbing Liu