Search
Now showing items 1-9 of 9
Symbolic Analysis via Semantic Reinterpretation
(University of Wisconsin-Madison Department of Computer Sciences, 2008)
In recent years, the use of symbolic analysis in systems for testing
and verifying programs has experienced a resurgence. By ``symbolic
program analysis'', we mean logic-based techniques to analyze state
changes along ...
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
(University of Wisconsin-Madison Department of Computer Sciences, 2008)
This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only ...
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 ...
Solving Multiple Dataflow Queries Using WPDSs
(University of Wisconsin-Madison Department of Computer Sciences, 2008)
A dataflow query asks for the set of reachable (abstract) states, given a starting set of states. In this paper, we show how to optimize multiple queries on the same program (each with a different starting set of states) ...
MCDASH: Refinement-Based Property Verification for Machine Code
(University of Wisconsin-Madison Department of Computer Sciences, 2009)
This paper presents MCDASH, a refinement-based model checker for
machine code. While model checkers such as SLAM, BLAST, and DASH have
each made significant contributions in the field of
verification/flaw-detection, ...
Improving Pushdown System Model Checking
(University of Wisconsin-Madison Department of Computer Sciences, 2006)
In this paper, we reduce pushdown system (PDS) model checking to a graph-theoretic problem, and apply a fast graph algorithm to improve the running time for model checking. We use \textit{weighted} PDSs as a generalized ...
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 ...