Search
Now showing items 1-10 of 11
Verifying Concurrent Message-Passing C Programs with Recursive Calls
(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 ...
A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks
(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 ...
Advanced Querying for Property Checking
(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 ...
Towards the Analysis of Transactional Software
(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 ...
Static Detection of Atomic-Set-Serializability Violations
(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. ...
Verifying Information Flow Control Over Unbounded Processes
(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 ...
Dissolve: A Distributed SAT Solver Based on Stalmarck's Method
(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 ...
Weighted Pushdown Systems and Weighted Transducers
(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 ...
Interprocedural Analysis of Concurrent Programs Under a Context Bound
(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 ...
Abstract Error Projection
(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 ...