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. Ghilardi
Primo
;
E. Pagani
Secondo
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.
Settore INF/01 - Informatica
dic-2017
http://ceur-ws.org/Vol-2013/paper14.pdf
Book Part (author)
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/574409
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact