|
The Verified Software Laboratory is a software engineering research laboratory in the Department of Computer and Information Sciences at the University of Delaware. The VSL conducts research into one of the most important unsolved problems in computer science: how to develop verifiably correct complex software systems.
|
The VSL is
directed by Stephen F. Siegel. We are
always looking for motivated undergraduate and graduate students to
join our research team. If you are interested in learning more
about what we do, email siegel@udel.edu or stop by the lab
in Smith Hall room 421.
Ph.D. student Alex Wilton is
working on methods to automatically verify CUDA-C programs, with a
particular emphasis on programs implementing graph algorithms, such
as those in the Indigo suite.
M.S. student Venkata Dhavala is applying CIVL to the
PETSc code base, focusing
on formal correctness verification of the Vector module.
B.S./M.S. student Devin
Cummings is helping design the lab's next generation model checking
tool, SymPIL. In this project, he also supports rigorous software
engineering techniques, including testing, coverage analysis, and
automated build systems.
Former students include John Edenhofner, Dan Fix, Zane Greenholt, Sydney Hester, Ziqing Luo (Apple), Pujan Kafle, Michael Karpeles, Andre Marianiello, Tim McClory, Sam Moelius, Elizabeth Strobel, Ben Perry, Yi Wei, Wenhao Wu (Google), Yihao Yan (Google), Alex You, Matthew Zelisnki, and Tim Zirkel (MITRE). Manchun Zheng served as a postdoctoral researcher.
Currently, the VSL is focusing on parallel programs used for
scientific computation and is developing tools that can find
defects in these programs or establish their correctness. A
variety of methods are being brought to bear on the problem,
drawing on techniques from logic, compiler theory, symbolic
computation, and model checking.