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...
Những tác giả chính: | Schäfer, M, Ekman, T, Moor, O |
---|---|
Tác giả khác: | Castagna, G |
Định dạng: | Conference item |
Được phát hành: |
Springer
2009
|
Những quyển sách tương tự
-
Formalising and Verifying Reference Attribute Grammars in Coq
Bằng: Schäfer, M, et al.
Được phát hành: (2009) -
Verifying the correct composition of distributed components: Formalisation and Tool
Bằng: Ludovic Henrio, et al.
Được phát hành: (2015-02-01) -
A systematic derivation of the STG machine verified in Coq
Bằng: Pirog, M, et al.
Được phát hành: (2010) -
Formalising policies for insider-threat detection: A tripwire grammar
Bằng: Agrafiotis, I, et al.
Được phát hành: (2017) -
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Bằng: Burak Ekici, et al.
Được phát hành: (2019-08-01)