Now showing items 1-12 of 12

    • An Abstract Domain for Bit-Vector Inequalities 

      Reps, Thomas; Thakur, Aditya; Sharma, Tushar (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 

      Elder, Matt; Lim, Junghee; Sharma, Tushar; Anderson, Tycho; Reps, Thomas (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 

      Mine, Antoine; Breck, Jason; Reps, Thomas (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 

      Reps, Thomas; Elder, Matt; Thakur, Aditya (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 

      Reps, Thomas; Thakur, Aditya (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 

      Reps, Thomas; Thakur, Aditya (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 

      Thakur, Aditya; Reps, Thomas (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 

      Reps, Thomas; Sharma, Tushar (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 

      Reps, Thomas; Lim, Junghee; Lal, Akash; Thakur, Aditya (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 

      Thakur, Aditya; Breck, Jason; Reps, Thomas (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 

      Thakur, Aditya; Breck, Jason; Reps, Thomas (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 

      Thakur, Aditya (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. ...