Now showing items 1-2 of 2
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 ...
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 ...