Merge pull request #24 from netverify/2.0-fix-links

2.0 fix links

Author: ratulm

_posts/2020-12-15-network-verification-2-0.md

@@ -38,7 +38,7 @@ The monolithic approach was helpful for the first generation of network verifica
 
 ## A linguistic approach
 
-There are multiple ways to tackle the Network Verification 2.0 challenges above, but a linguistic approach is particularly appealing (which we are exploring; see here and here). To make it easy for engineers to specify inputs, along with their networks’ unwritten assumptions, we should design an invariant language that can naturally express sets of values and set operations like unions and differences. We may consider a language that blends SQL-like queries over a data model of the network and regular expressions over path constraints. 
+There are multiple ways to tackle the Network Verification 2.0 challenges above, but a linguistic approach is particularly appealing (which we are exploring; see [here](https://ratul.org/papers/hotnets2019-putting.pdf) and [here](https://ratul.org/papers/hotnets2020-zen.pdf)). To make it easy for engineers to specify inputs, along with their networks’ unwritten assumptions, we should design an invariant language that can naturally express sets of values and set operations like unions and differences. We may consider a language that blends SQL-like queries over a data model of the network and regular expressions over path constraints. 
 
 A high-level invariant language over a well-defined data model also makes it easy to track which network elements (e.g., devices, interfaces, paths) are “covered” by an invariant. This basic capability can then be the basis for providing feedback to network engineers about how well their invariant set covers the network. This is similar to how test frameworks for software can quantify the extent of software coverage, though we will need custom measures for network coverage given the differences in the two domains (e.g., a network is not a sequence of statements or basic blocks, which is the model employed by software test frameworks).