Browsing CS Technical Reports by Subject "abstract interpretation"
Now showing items 1-12 of 12
-
An Abstract Domain for Bit-Vector Inequalities
(University of Wisconsin-Madison Department of Computer Sciences, 2013-04-16)This paper advances the state of the art in abstract interpretation of machine code. It tackles two of the biggest challenges in machine-code analysis: (1) holding onto invariants about values in memory, and (2) identifying ... -
Abstract Domains of Affine Relations
(University of Wisconsin-Madison Department of Computer Sciences, 2013-05-13)This paper considers some known abstract domains for affine-relation analysis, along with several variants, and studies how they relate to each other. The various domains represent sets of points that satisfy affine ... -
An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs
(2016-01-08)This paper addresses the problem of proving a given invariance property phi of a loop in a numeric program, by inferring automatically a stronger inductive invariant psi. The algorithm we present is based on both abstract ... -
Bilateral Algorithms for Symbolic Abstraction
(University of Wisconsin-Madison Department of Computer Sciences, 2012-03-28)Given a concrete domain C, a concrete operation tau: C -> C, and an abstract domain A, a fundamental problem in abstract interpretation is to find the best abstract transformer tau#: A -> A that over-approximates tau. ... -
A Generalization of Staalmarck's Method
(University of Wisconsin-Madison Department of Computer Sciences, 2011-12)This paper gives an account of Staalmarck's method for validity checking of propositional-logic formulas, and explains each of the key components in terms of concepts from the field of abstract interpretation. We then ... -
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. ...