We develop quantifier elimination procedures for a fragment of higher order logic arising from the formalization of distributed sys- tems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of Pre/Post images and of projections. We show in particular that our procedures are quite effec- tive in producing counter abstractions that can be model-checked using standard SMT technology.
Second Order Quantifier Elimination: Towards Verification Applications / S. Ghilardi, E. Pagani (CEUR WORKSHOP PROCEEDINGS). - In: Second-Order Quantifier Elimination and Related Topics : SOQE 2017 / [a cura di] P. Koopmann, S. Rudolph, R. A. Schmidt, C. Wernhard. - Prima edizione. - [s.l] : CEUR, 2017 Dec. - pp. 36-50 (( convegno Second-Order Quantifier Elimination and Related Topics tenutosi a Dresden nel 2017.
Second Order Quantifier Elimination: Towards Verification Applications
S. GhilardiPrimo
;E. PaganiSecondo
2017
Abstract
We develop quantifier elimination procedures for a fragment of higher order logic arising from the formalization of distributed sys- tems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of Pre/Post images and of projections. We show in particular that our procedures are quite effec- tive in producing counter abstractions that can be model-checked using standard SMT technology.File | Dimensione | Formato | |
---|---|---|---|
SOQE_PRINTED.pdf
accesso aperto
Descrizione: articolo pubblicato
Tipologia:
Publisher's version/PDF
Dimensione
422.65 kB
Formato
Adobe PDF
|
422.65 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.