@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@InProceedings{holcomb-memocode12,
  author = 	 {Daniel Holcomb and Alexander Gotmanov and Michael Kishinevsky and Sanjit A. Seshia},
  title = 	 {Compositional Performance Verification of NoC Designs},
  booktitle = 	 {Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, 
  month = {July},
  year = 	 {2012},
  abstract = {We present a compositional approach to formally verify
  quality-of-service (QoS) properties of network-on-chip (NoC)
  designs. A major challenge to scalability is the need to verify
  latency bounds for hundreds to thousands of cycles, which are beyond
  the capacity of state-of-the-art model checkers. We address this
  challenge by a compositional form of k-induction. The overall
  latency bound problem is divided into a number of sub-problems,
  termed latency lemmas. Each latency lemma states that a packet
  spends a smaller number of cycles at a particular ``stage'' of
  progress. We present a partially-automated method of computing these
  stages based on the topology of the network and a subset of relevant
  state, and verify the latency lemmas using k-induction.  The
  effectiveness of this compositional technique is demonstrated on
  illustrative examples as well as an industrial ring interconnection
  network.},
}