PostHat and All That: Attaining Most-Precise Inductive Invariants

dc.contributor.author	Reps, Thomas
dc.contributor.author	Lim, Junghee
dc.contributor.author	Lal, Akash
dc.contributor.author	Thakur, Aditya
dc.date.accessioned	2013-04-18T15:09:25Z
dc.date.available	2013-04-18T15:09:25Z
dc.date.issued	2013-04-16
dc.identifier.citation	TR1790	en
dc.identifier.uri	http://digital.library.wisc.edu/1793/65368
dc.description.abstract	In abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (``strongest'', ``best'') inductive A-invariant for each program. Many techniques have been developed in abstract interpretation for finding over-approximate solutions, but only a few algorithms have been given that can achieve the fundamental limits that abstract-interpretation theory establishes. In this paper, we present an algorithm that solves the following problem: Given program P, an abstract domain A, and access to an SMT solver, find the most-precise inductive A-invariant for P.	en
dc.subject	machine code	en
dc.subject	predicate abstraction	en
dc.subject	symbolic abstraction	en
dc.subject	inductive invariants	en
dc.subject	abstract interpretation	en
dc.title	PostHat and All That: Attaining Most-Precise Inductive Invariants	en
dc.type	Technical Report	en

CS Technical Reports
Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison