Ohio University EECS

Software Verification & Security

The Software Verification and Security group — headquartered in the School of Electrical Engineering and Computer Science in Ohio University's Russ College of Engineering and Technology — applies mathematically rigorous methods and tools, such as interactive theorem proving in Coq, to facilitate the construction, maintenance, and proof of high-assurance software systems.
Coq logo

People

Faculty


Gordon Stewart

David Juedes

Graduate Students

Sam Merten Sam Merten (PhD)
Alex Bagnall Alex Bagnall (MS)
Undergrads/Alumni
  • Logan Leland (UG)
  • Charlie Murphy (UG, now at Princeton)
  • Nathan St. Amour (UG)

Research

Active Projects

Network
Languages, abstractions, and logics for distributed systems such as distributed network routers and load balancers, with particular focus on formal proof of liveness and complexity properties.
People: Alex Bagnall, Sam Merten, Gordon Stewart

Bipartite graph
Mechanized Graph Algorithms: In collaboration with David Juedes: Machine-checked graph algorithms — all independent sets, graph coloring, star bicoloring, etc. — for use in implementation and proof of algorithms relevant to scientific computing.
People: David Juedes, Sam Merten, Gordon Stewart