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)