Browsing MINDS@UW Madison by Subject "abstract interpretation"
Now showing items 6-12 of 12
-
A Method for Symbolic Computation
(2011-12)In 1979, Cousot and Cousot gave a specification of the ?best? (most-precise) abstract transformer possible for a given concrete transformer and a given abstract domain. Unfortunately, their specification does not lead to ... -
A Method for Symbolic Computation of Abstract Operations
(2012-02)In 1979, Cousot and Cousot gave a specification of the best (most-precise) abstract transformer possible for a given concrete transformer and a given abstract domain. Unfortunately, their specification does not lead to an ... -
A New Abstraction Framework for Affine Transformers
(2017-05-16)Abstract. This paper addresses the problem of abstracting a set of affine transformers v' = v C + d, where v and v' represent the pre-state and post-state, respectively. We introduce a framework to harness any base abstract ... -
PostHat and All That: Attaining Most-Precise Inductive Invariants
(2013-04-16)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'', ... -
Satisfiability Modulo Abstraction for Separation Logic with Linked Lists
(University of Wisconsin-Madison Department of Computer Sciences, 2014-07-17)Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes ... -
Satisfiability Modulo Abstraction for Separation Logic with Linked Lists
(University of Wisconsin-Madison Department of Computer Sciences, 2014-02-13)Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for deciding unsatisfiability of formulas in a fragment of separation logic that ... -
Symbolic Abstraction: Algorithms and Applications
(2014-08-21)This dissertation explores the use of abstraction in two areas of automated reasoning: verification of programs, and decision procedures for logics. Establishing that a program is correct is undecidable in general. ...