Formalising and Verifying Reference Attribute Grammars in Coq.
Reference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their meritin practical applications, no attempt has so far been made to rigorously verify correctness properties of the resulting systems. We present a general met...
Автори: | Schäfer, M, Ekman, T, Moor, O |
---|---|
Інші автори: | Castagna, G |
Формат: | Conference item |
Опубліковано: |
Springer
2009
|
Схожі ресурси
Схожі ресурси
-
Formalising and Verifying Reference Attribute Grammars in Coq
за авторством: Schäfer, M, та інші
Опубліковано: (2009) -
Verifying the correct composition of distributed components: Formalisation and Tool
за авторством: Ludovic Henrio, та інші
Опубліковано: (2015-02-01) -
A systematic derivation of the STG machine verified in Coq
за авторством: Pirog, M, та інші
Опубліковано: (2010) -
Formalising policies for insider-threat detection: A tripwire grammar
за авторством: Agrafiotis, I, та інші
Опубліковано: (2017) -
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
за авторством: Burak Ekici, та інші
Опубліковано: (2019-08-01)