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)

Thumbnail Image

Date

2015

Authors

Heizmann, Matthias
Dietsch, Daniel
Leike, Jan
Musa, Betim
Podelski, Andreas

Journal Title

Journal ISSN

Volume Title

Publisher

Conference Organising Committee

Abstract

Ultimate 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.

Description

Keywords

Keywords: Algorithms; Interpolation; Verification; Array interpolation; C programs; Interpolants; Memory safety; Reachability; Software verification tools; Unsatisfiable core; Variable analysis; C (programming language)

Citation

URI

http://hdl.handle.net/1885/102662

Collections

ANU Research Publications

Source

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Type

Conference paper

Book Title

Entity type

Access Statement

License Rights

DOI

10.1007/978-3-662-46681-0_43

Restricted until

2037-12-31

Downloads

File
Description
01_Heizmann_ULTIMATE_AUTOMIZER_with_array_2015.pdf (101.58 KB)

DSpace software copyright © 2002-2026 LYRASIS