Browsing by Author "Kidd, Nicholas"
Now showing items 9-12 of 12
-
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 ...