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)