SymNV: Symbolic Network Verification

In modern networks, implementations of services and protocols for resource discovery, equipment configuration and network management are complex and error-prone. Implementation bugs in network protocols are hard to detect because they are often triggered by complex sequences of events that occur only after deployment and prolonged operation.

SymNV explores how future networks can exploit runtime verification techniques. The goal is to develop an architecture for runtime verification in networks based on bounded model-checking and symbolic execution of network services.

EPSRC/MobileVCE (2009-2010)
Cristian Cadar (Imperial College London)
JaeSeung Song (Sejong University, South Korea)
Tiejun Ma (University of Southampton, UK)

Related Publications

JaeSeung Song, Cristian Cadar, and Peter Pietzuch
IEEE Transactions on Software Engineering (TSE), 2014
Volume 40, Issue 7, p.695--709
JaeSeung Song, Tiejun Ma, Cristian Cadar, and Peter Pietzuch
20th IEEE International Conference on Computer Communications and Networks (ICCCN), 2011
Maui, Hawaii, USA
Tiejun Ma, and Peter Pietzuch
10th International Conference on Networking (IFIP/TC6 Networking), 2011
Valencia, Spain
JaeSeung Song, Tiejun Ma, and Peter Pietzuch
Sixth IEEE PerCom Workshop on Pervasive Wireless Networking (PWN), 2010
Mannheim, Germany