Now showing items 1-14 of 14

• #### 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 ...
• #### 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 ...
• #### BTrace: Path Optimization for Debugging ﻿

(University of Wisconsin-Madison Department of Computer Sciences, 2005)
We present and solve a path optimization problem on programs. Given a set of program nodes, called critical nodes, we find a shortest path through the program's control flow graph that touches the maximum number of these ...
• #### Graph Isomorphism for Colored Graphs with Color Multiplicity Bounded by 3 ﻿

(University of Wisconsin-Madison Department of Computer Sciences, 2005)
The colored graph isomorphism problem is a restricted version of the general graph isomorphism (GI)problem that involves deciding the existence of a color preserving isomorphism between a pair of colored graphs. In this ...
• #### 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 ...
• #### Interprocedural Analysis and the Verification of Concurrent Programs ﻿

(University of Wisconsin-Madison Department of Computer Sciences, 2009)
In the modern world, not only is software getting larger and more complex, it is also becoming pervasive in our daily lives. On the one hand, the advent of multi-core processors is pushing software towards becoming more ...
• #### 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 ...
• #### 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, ...
• #### PostHat and All That: Attaining Most-Precise Inductive Invariants ﻿

(2013-04-16)
In abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (strongest'', ...
• #### 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 ...
• #### 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) ...
• #### 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 ...
• #### Verifying Concurrent Programs via Bounded Context-Switching and Induction ﻿

(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 ...
• #### 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 ...