Now showing items 5-14 of 14

    • Improving Pushdown System Model Checking 

      Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2006)
      In this paper, we reduce pushdown system (PDS) model checking to a graph-theoretic problem, and apply a fast graph algorithm to improve the running time for model checking. We use \textit{weighted} PDSs as a generalized ...
    • Interprocedural Analysis and the Verification of Concurrent Programs 

      Lal, Akash (University of Wisconsin-Madison Department of Computer Sciences, 2009)
      In the modern world, not only is software getting larger and more complex, it is also becoming pervasive in our daily lives. On the one hand, the advent of multi-core processors is pushing software towards becoming more ...
    • Interprocedural Analysis of Concurrent Programs Under a Context Bound 

      Lal, Akash; Touili, Tayssir; Kidd, Nicholas; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2007)
      Analysis of recursive programs in the presence of concurrency and shared memory is undecidable. A common approach is to remove the recursive nature of the program while dealing with concurrency. A different approach is ...
    • MCDASH: Refinement-Based Property Verification for Machine Code 

      Lal, Akash; Lim, Junghee; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2009)
      This paper presents MCDASH, a refinement-based model checker for machine code. While model checkers such as SLAM, BLAST, and DASH have each made significant contributions in the field of verification/flaw-detection, ...
    • 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'', ...
    • Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis 

      Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2008)
      This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only ...
    • Solving Multiple Dataflow Queries Using WPDSs 

      Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2008)
      A dataflow query asks for the set of reachable (abstract) states, given a starting set of states. In this paper, we show how to optimize multiple queries on the same program (each with a different starting set of states) ...
    • Symbolic Analysis via Semantic Reinterpretation 

      Lim, Junghee; Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2008)
      In recent years, the use of symbolic analysis in systems for testing and verifying programs has experienced a resurgence. By ``symbolic program analysis'', we mean logic-based techniques to analyze state changes along ...
    • Verifying Concurrent Programs via Bounded Context-Switching and Induction 

      Prabhu, Prathmesh; Reps, Thomas; Lal, Akash; Kidd, Nicholas (University of Wisconsin-Madison Department of Computer Sciences, 2011)
      This paper presents a new approach to the problem of verifying safety properties of concurrent programs with shared memory and interleaving semantics. The method described leverages recent work on context-bounded analysis ...
    • Weighted Pushdown Systems and Weighted Transducers 

      Lal, Akash; Touili, Tayssir; Kidd, Nicholas; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2006)
      Pushdown Systems (PDSs) are an important formalism for modeling programs. Reachability analysis on PDSs has been used extensively for program verification. A key result, which made PDSs popular in the model-checking ...