Now showing items 4-12 of 12

    • 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 ...
    • 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'', ...
    • Property-Directed Shape Analysis 

      Itzhaky, Shachar; Bjorner, Nikolaj; Reps, Thomas; Sagiv, Mooly; Thakur, Aditya (2014-05-22)
      This paper addresses the problem of automatically generating quantified invariants for programs that manipulate singly and doubly linked-list data structures. Our algorithm is property-directed -- i.e., its choices are ...
    • 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. ...
    • WALi: Nested-Word Automata 

      Driscoll, Evan; Thakur, Aditya; Burton, Amanda; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2011)
      WALi-NWA is a C++ library for constructing, querying, and operating on nested-word automata. It is a portion of the WALi library, which provides types and operations for weighted automata. While the NWA portions of WALi ...