Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

On local reasoning in verification

MPG-Autoren
/persons/resource/persons44669

Ihlemann,  Carsten
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons44687

Jacobs,  Swen
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Ihlemann, C., Jacobs, S., & Sofronie-Stokkermans, V. (2008). On local reasoning in verification. In C. R. Ramakrishnan, & J. Rehof (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008 (pp. 265-281). New York: Springer.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-1C78-1
Zusammenfassung
We present a general framework which allows to identify complex theories important in verification for which efficient reasoning methods exist. The framework we present is based on a general notion of locality. We show that locality considerations allow us to obtain parameterized decidability and complexity results for many (combinations of) theories important in verification in general and in the verification of parametric systems in particular. We give numerous examples; in particular we show that several theories of data structures studied in the verification literature are local extensions of a base theory. The general framework we use allows us to identify situations in which some of the syntactical restrictions imposed in previous papers can be relaxed.