Now showing items 3-12 of 12

    • A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks 

      Kidd, Nicholas; Lammich, Peter; Touili, Tayssir; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2009)
      We present a new decision procedure for detecting property violations in pushdown models for concurrent programs that use lock-based synchronization, where each thread's lock operations are properly nested (a la ...
    • Dissolve: A Distributed SAT Solver Based on Stalmarck's Method 

      Henry, Julien; Thakur, Aditya; Kidd, Nicholas; Reps, Thomas (2017-03-08)
      Creating an effective parallel SAT solver is known to be a challenging task. At present, the most efficient implementations of parallel SAT solvers are portfolio solvers with some heuristics to share learnt clauses. In ...
    • 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 ...
    • Static Detection of Atomic-Set-Serializability Violations 

      Kidd, Nicholas; Reps, Thomas; Dolby, Julian; Vaziri, Mandana (University of Wisconsin-Madison Department of Computer Sciences, 2007)
      Vaziri et al. propose a data-centric approach to synchronization. The key underlying concept of their work is the atomic set, which specifies the existence of an invariant that holds on a set of fields of an object type. ...
    • Static Verification of Data-Consistency Properties 

      Kidd, Nicholas (University of Wisconsin-Madison Department of Computer Sciences, 2009)
      Writing correct shared-memory concurrent programs is hard. Not only must a programmer reason about the correctness of the sequential execution of code, but also about the possible side effects caused by interleaved ...
    • Towards the Analysis of Transactional Software 

      Kidd, Nicholas; Moore Kevin; Reps, Thomas; Wood, David (University of Wisconsin-Madison Department of Computer Sciences, 2007)
      The computer-architecture community's recent focus on multi-core architectures has spurred renewed interest in concurrent-programming techniques and abstractions. For programmers to take advantage of the processing power ...
    • Verifying Concurrent Message-Passing C Programs with Recursive Calls 

      Chaki, Sagar; Clarke, Edmund; Kidd, Nicholas; Reps, Thomas; Touili, Tayssir (University of Wisconsin-Madison Department of Computer Sciences, 2005)
      We consider the model-checking problem for C programs with (1) data ranging over very large domains, (2) (recursive) procedure calls, and (3) concurrent parallel components that communicate via synchronizing actions. We ...
    • 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 ...
    • Verifying Information Flow Control Over Unbounded Processes 

      Harris, William; Kidd, Nicholas; Chaki, Sagar; Jha, Somesh; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2009)
      Decentralized Information Flow Control (DIFC) systems enable programmers to express a desired DIFC policy, and to have the policy enforced via a reference monitor that restricts interactions between system objects, such ...
    • 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 ...