|
PLDog submit an article | search | rss feed | register | feedback | about |
| Registration | |
| You need to register to submit articles and post comments. Read this to find out how. |
| A hybrid of counterexample-based and proof-based abstraction | |||
|
|||
| Counterexample- and proof-based refinement are complementary approaches to iterative abstraction. In the former case, a single abstract counterexample is eliminated by each refinement step, while in the latter case, all counterexamples of a given length are eliminated. In counterexample-based abstraction, the concretization and refinement problems are relatively easy, but the number of iterations tends to be large. Proof-based abstraction, on the other hand, puts a greater burden on the refinement step, which can then become the performance bottleneck. In this paper, we show that counterexample- and proof-based refinement are extremes of a continuum, and propose a hybrid approach that balances the cost and quality of refinement. In a study of a large number of industrial verification problems, we find that there is a strong relation between the effort applied in the refinement phase and the number of refinement iterations. For this reason, proof-based abstraction is substantially more efficient than counterexample-based abstraction. However, a judicious application of the hybrid approach can lessen the refinement effort without unduly increasing the number of iterations, yielding a method that is somewhat more robust overall. | |||
| Nina Amla and Ken McMillan | |||
| Appears in FMCAD 2004 | |||
| Case says: [ You must be logged in to view this comment. ] | |||
|
|||
| The Model Checker SPIN | |||
|
|||
| SPIN is a generic verification system that supports the design and verification of asynchronous process systems. SPIN verification models are focused on proving the correctness of process interactions, and they attempt to abstract as much as possible from internal sequential computations. Process interactions can be specified in SPIN with rendezvous primitives, with asynchronous message passing through buffered channels, through access to shared variables, or with any combination of these. In focusing on asynchronous control in software systems, rather than synchronous control in hardware systems, SPIN distinguishes itself from other well-known approaches to model checking. | |||
| Gerard Holzmann | |||
| Appears in IEEE Transactions on Software Engineering | |||
|
|||
| DITTO: Automatic Incrementalization of Data Structure Invariant Checks (in Java) | |||
|
|||
| We present DITTO, an automatic incrementalizer for dynamic, side effect-free data structure invariant checks. Incrementalization speeds up the execution of a check by reusing its previous executions, checking the invariant anew only on the changed parts of the data structure. DITTO exploits properties specific to the domain of invariant checks to automate and simplify the process without restricting what mutations the program can perform. Our incrementalizer works for modern imperative languages such as Java and C#. It can incrementalize, for example, verification of red-black tree properties and the consistency of the hash code in a hash table bucket. Our source-to-source implementation for Java is automatic, portable, and efficient.DITTO provides speedups on data structures with as few as 100 elements; on larger data structures, its speedups are characteristic of non-automatic incrementalizers: roughly 5-fold at 5,000 elements, and growing linearly with data structure size. | |||
| Ajeet Shankar, Ras Bodik | |||
| Appears in PLDI '07 | |||
|
|||
| Effective Typestate Verification in the Presence of Aliasing | |||
|
|||
| This paper addresses the challenge of sound typestate verification,with acceptable precision, for real-world Java programs. We present a novel framework for verification of typestate properties,including several new techniques to precisely treat aliases without undue performance costs. In particular, we present a flow-sensitive,context-sensitive, integrated verifier that utilizes a parametric abstract domain combining typestate and aliasing information. To scale to real programs without compromising precision,we present a staged verification system in which faster verifiers run as early stages which reduce the workload for later, more precise,stages. We have evaluated our framework on a number of real Java programs,checking correct API usage for various Java standard libraries. The results show that our approach scales to hundreds of thousands of lines of code, and verifies correctness for 93% of the potential points of failure. |
|||
| Appears in ISSTA 06 | |||
|
|||
| Yesterday, my program worked. Today, it does not. Why? | |||
|
|||
| Presenter: Shoaib Kamil Imagine some program and a number of changes. If none of these |
|||
| Andreas Zeller | |||
| Appears in ESEC / FSE 1999 | |||
| Meyerovich says: [ You must be logged in to view this comment. ] | |||
|
|||
| Stochastic Search for Signal Processing Algorithm Optimization | |||
|
|||
| Many difficult problems can be viewed as search problems. However, given a new task with an embedded search problem, it is challenging to state and find a truly effective search approach. In this paper, we address the complex task of signal processing optimization. We first introduce and discuss the complexities of this domain. In general, a single signal processing algorithm can be represented by a very large number of different but mathematically equivalent formulas. When these formulas are implemented in actual code, unfortunately their running times differ significantly. Signal processing algorithm optimization aims at finding the fastest formula. We present a new approach that successfully solves this problem, using an evolutionary stochastic search algorithm, STEER, to search through the very large space of formulas. We empirically compare STEER against other search methods, showing that it notably can find faster formulas while still only timing a very small portion of the search space. Keywords: |
|||
| Bryan Singer and Manuela Veloso | |||
| Appears in Proc. Supercomputing (SC), pp. 22, 2001 | |||
|
|||
| Dynamic Partial Order Reduction of Model Checking Software | |||
|
|||
| We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless. | |||
| Cormac Flanagan and Patrice Godefroid | |||
| Appears in POPL 2005 | |||
|
|||
| Mining Jungloids: Helping to Navigate the API Jungle, | |||
|
|||
| Reuse of existing code from class libraries and frameworks is often difficult because APIs are complex and the client code required to use the APIs can be hard to write. We observed that a common scenario is that the programmer knows what type of object he needs, but does not know how to write the code to get the object. In order to help programmers write API client code more easily, we developed techniques for synthesizing jungloid code fragments automatically given a simple query that describes that desired code in terms of input and output types. A jungloid is simply a unary expression; jungloids are simple, enabling synthesis, but are also versatile, covering many coding problems, and composable, combining to form more complex code fragments. We synthesize jungloids using both API method signatures and jungloids mined from a corpus of sample client programs. We implemented a tool, PROSPECTOR, based on these techniques. PROSPECTOR is integrated with the Eclipse IDE code assistance feature, and it infers queries from context so there is no need for the programmer to write queries. We tested PROSPECTOR on a set of real programming problems involving APIs; PROSPECTOR found the desired solution for 18 of 20 problems.We also evaluated PROSPECTOR in a user study, finding that programmers solved programming problems more quickly and with more reuse when using PROSPECTOR than without PROSPECTOR. |
|||
| David Madelin, Lin Xu, Ras Bodik, Doug Kimelman | |||
| Appears in PLDI 2005 | |||
|
|||
| http://portal.acm.org/ft_gateway.cfm?id=96731&type=pdf&coll=GUIDE&dl=GUIDE&CFID=42871785&CFTOKEN=21379085 | |||
|
|||
| We need a programming model that combines the advantages of the synchronous and asynchronous parallel styles. Synchronous programs are determinate (thus easier to reason about) and avoid synchronization overheads. Asynchronous programs are more flexible and handle conditionals more efficiently. Here we propose a programming model with the benefits of both styles. We allow asynchronous threads of control but restrict shared-memory accesses and other side effects so as to prevent the behavior of the program from depending on any accidents of execution order that can arise from the indeterminacy of the asynchronous process model. These restrictions may be enforced either dynamically (at run time) or statically (at compile time). In this paper we concentrate on dynamic enforcement, and exhibit an implementation of a parallel dialect of Scheme based on these ideas. A single successful execution of a parallel program in this model constitutes a proof that the program is free of race conditions (for that particular set of input data). We also speculate on a design for a programming language using static enforcement. The notion of distinctness is important to proofs of noninterference. An appropriately designed programming language must support such concepts as "all the elements of this array are distinct," perhaps through its type system. This parallel programming model does not support all styles of parallel programming, but we argue that it can support a large class of interesting algorithms with considerably greater efficiency (in some cases) than a strict SIMD approach and considerably greater safety (in all cases) than a full-blown MIMD approach. |
|||
| Guy L. Steele Jr. | |||
| Appears in POPL '90 | |||
|
|||
| Type-dependence Analysis and Program Transformation for Symbolic Execution | |||
|
|||
| Symbolic execution can be problematic when applied to real applications. This paper addresses two of these problems: (1) the constraints generated during symbolic execution may be of a type not handled by the underlying decision procedure, and (2) some parts of the application may be unsuitable for symbolic execution (e.g., third-party libraries). The paper presents type-dependence analysis, which performs a context- and field-sensitive interprocedural static analysis to identify program entities that may store symbolic values at run-time. This information is used to identify the above two problematic cases and assist the user in addressing them. The paper also presents a technique to transform real applications for efficient symbolic execution. Instead of transforming the entire application, which can be inefficient and infeasible (mostly for pragmatic reasons), our technique leverages the results of type-dependence analysis to transform only parts of the program that may interact with symbolic values. Finally, the paper discusses the implementation of our analysis and transformation technique in a tool, stinger, and an empirical evaluation performed on two real applications. The results of the evaluation show the effectiveness of our approach. | |||
| S. Anand, A. Orso, and M.J. Harrold | |||
| Appears in TACAS 2007 | |||
|
|||
| Role-Based Exploration of Object-Oriented Programs | |||
|
|||
| We present a new technique for helping developers understand heap properties of object-oriented programs and how the actions of the program affect these properties. Our dynamic analysis uses the aliasing properties of objects to synthesize a set of roles; each role represents an abstract object state intended to be of interest to the developer. We allow the developer to customize the analysis to explore the object states and behavior of the program at multiple different and potentially complementary levels of abstraction. The analysis uses roles as the basis for three abstractions: Together, these abstractions provide useful information |
|||
| Brian Demsky, Martin Rinard | |||
| Appears in ICSE 2002 | |||
|
|||
| ESP: Path-Sensitive Program Verification in Polynomial Time | |||
|
|||
| In this paper, we present a new algorithm for partial program verification that runs in polynomial time and space. We are interested in checking that a program satisfies a given temporal safety property. Our insight is that by accurately modeling only those branches in a program for which the property-related behavior differs along the arms of the branch, we can design an algorithm that is accurate enough to verify the program with respect to the given property, without paying the potentially exponential cost of full path-sensitive analysis.We have implemented this "property simulation" algorithm as part of a partial verification tool called ESP. We present the results of applying ESP to the problem of verifying the file I/O behavior of a version of the GNU C compiler (gcc, 140,000 LOC). We are able to prove that all of the 646 calls to fprintf in the source code of gcc are guaranteed to print to valid, open files. Our results show that property simulation scales to large programs and is accurate enough to verify meaningful properties. | |||
| Manuvir Das, Sorin Lerner, Mark Seigle | |||
| Appears in PLDI 2002 | |||
|
|||
| view previous 12 articles |