Ben Selfridge
PhD Student

Department of Computer Science
College of Natural Sciences
The University of Texas at Austin

Email: benself 'at'

Mail Address:
Department of Computer Science
The University of Texas at Austin
2317 Speedway, Stop D9500
Austin, Texas 78712

Supervisor: Dr. Warren A. Hunt, Jr.

I've been working on ACL2-related projects since I joined the Formal Methods group in 2013. My research mostly involves formal correctness proofs of hardware and software in multiprocessor environments. I use ACL2 to write simulators of some kind of multiprocessor or multi-agent design or protocol, and then construct correctness proofs of those designs, or the programs written for them, in ACL2.

Here are some independent projects I've done.

topsort: Performs a topological sort of a graph. Just like unix's "tsort" program, only a lot faster. (I have no clue why most UNIX versions are so slow.) Also includes a tool for checking the correctness of a topological sort against a graph, and a tool for generating random acyclic graphs. I've tested my program against tsort, and mine always beats it. With a graph with >1000 nodes, it sorts the input with an order of magnitude faster than tsort. This project is licensed under the GPL.