Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

ULTIMATE AUTOMIZER with array interpolation (Competition contribution)

Simple item page
dc.contributor.authorHeizmann, Matthias
dc.contributor.authorDietsch, Daniel
dc.contributor.authorLeike, Jan
dc.contributor.authorMusa, Betim
dc.contributor.authorPodelski, Andreas
dc.contributor.editorRaskin J.-F.Chechik
dc.coverage.spatialLondon, United Kingdom
dc.date.accessioned2016-06-14T23:18:54Z
dc.date.createdApril 11-18 2015
dc.date.issued2015
dc.date.updated2024-01-07T07:15:38Z
dc.description.abstractUltimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.
dc.identifier.isbn9783662466803
dc.identifier.urihttp://hdl.handle.net/1885/102662
dc.publisherConference Organising Committee
dc.relation.ispartofseries21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
dc.sourceLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.subjectKeywords: Algorithms; Interpolation; Verification; Array interpolation; C programs; Interpolants; Memory safety; Reachability; Software verification tools; Unsatisfiable core; Variable analysis; C (programming language)
dc.titleULTIMATE AUTOMIZER with array interpolation (Competition contribution)
dc.typeConference paper
local.bibliographicCitation.lastpage457
local.bibliographicCitation.startpage455
local.contributor.affiliationHeizmann, Matthias, University of Freiburg
local.contributor.affiliationDietsch, Daniel, University of Freiburg
local.contributor.affiliationLeike, Jan, College of Engineering and Computer Science, ANU
local.contributor.affiliationMusa, Betim, University of Freiburg
local.contributor.affiliationPodelski, Andreas, University of Freiburg
local.contributor.authoruidLeike, Jan, u5485774
local.description.embargo2037-12-31
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.absfor080304 - Concurrent Programming
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
local.identifier.ariespublicationa383154xPUB2553
local.identifier.doi10.1007/978-3-662-46681-0_43
local.identifier.scopusID2-s2.0-84926673625
local.type.statusPublished Version

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
01_Heizmann_ULTIMATE_AUTOMIZER_with_array_2015.pdf
Size:
101.58 KB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS