Now showing items 1-12 of 12

    • Abstract Error Projection 

      Lal, Akash; Kidd, Nicholas; Reps, Thomas; Touili, Tayssir (University of Wisconsin-Madison Department of Computer Sciences, 2006)
      To improve the reporting of results from model checking and programanalysis systems, we introduce the notion of an error projection and annotated error projection. An error projection is a set of program nodes N such that ...
    • Advanced Querying for Property Checking 

      Kidd, Nicholas; Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2007)
      Extended weighted pushdown systems (EWPDSs) are an extension of pushdown systems that incorporate infinite-state data abstractions. Nested-word automata (NWAs) are able to recognize languages that exhibit context-free ...
    • 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 ...