Skip to Main Content (Press Enter)

Logo UNITO
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione

UNI-FIND
Logo UNITO

|

UNI-FIND

unito.it
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione
  1. Pubblicazioni

Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?

Capitolo di libro
Data di Pubblicazione:
2011
Abstract:
This paper further investigates the potential and practical applicability of abstract compilation in two different directions. First, we formally define an abstract compilation scheme for precise prediction of uncaught exceptions for a simple Java-like language; besides the usual user declared checked exceptions, the analysis covers the runtime ClassCastException. Second, we present a general implementation schema for abstract compilation based on coinductive CLP with variance annotation of user-defined predicates, and propose an implementation based on a Prolog prototype meta-interpreter, parametric in the solver for the subtyping constraints.
Tipologia CRIS:
02A-Contributo in volume
Keywords:
Java - formal verification - microkernel - object orientation - object-oriented languages - program verification - type inference
Elenco autori:
Davide Ancona; Andrea Corradi; Giovanni Lagorio; Ferruccio Damiani
Autori di Ateneo:
DAMIANI Ferruccio
Link alla scheda completa:
https://iris.unito.it/handle/2318/81714
Titolo del libro:
Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers
Pubblicato in:
LECTURE NOTES IN COMPUTER SCIENCE
Journal
LECTURE NOTES IN COMPUTER SCIENCE
Series
  • Dati Generali

Dati Generali

URL

http://www.springer.com/computer/swe/book/978-3-642-18069-9; http://www.springerlink.com/content/t25jq107744016gn/
  • Utilizzo dei cookie

Realizzato con VIVO | Designed by Cineca | 25.6.1.0