Now showing items 6-12 of 12

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