Now showing items 10-14 of 14

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