Catálogo de publicaciones - libros

Compartir en
redes sociales


Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25: Apr

Holger Hermanns ; Jens Palsberg (eds.)

En conferencia: 12º International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Vienna, Austria . March 25, 2006 - April 2, 2006

Resumen/Descripción – provisto por la editorial

No disponible.

Palabras clave – provistas por la editorial

Software Engineering/Programming and Operating Systems; Logics and Meanings of Programs; Software Engineering; Computer Communication Networks; Algorithm Analysis and Problem Complexity

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2006 SpringerLink

Información

Tipo de recurso:

libros

ISBN impreso

978-3-540-33056-1

ISBN electrónico

978-3-540-33057-8

Editor responsable

Springer Nature

País de edición

Reino Unido

Fecha de publicación

Información sobre derechos de publicación

© Springer-Verlag Berlin Heidelberg 2006

Tabla de contenidos

Weighted Pushdown Systems and Trust-Management Systems

Somesh Jha; Stefan Schwoon; Hao Wang; Thomas Reps

The authorization problem is to decide whether, according to a security policy, some principal should be allowed access to a resource. In the trust-management system SPKI/SDSI, the security policy is given by a set of certificates, and proofs of authorization take the form of certificate chains. The certificate-chain-discovery problem is to discover a proof of authorization for a given request. Certificate-chain-discovery algorithms for SPKI/SDSI have been investigated by several researchers. We consider a variant of the certificate-chain discovery problem where the certificates are distributed over a number of servers, which then have to cooperate to identify the proof of authorization for a given request. We propose two protocols for this purpose. These protocols are based on distributed model-checking algorithms for weighted pushdown systems (WPDSs). These protocols can also handle cases where certificates are labeled with weights and where multiple certificate chains must be combined to form a proof of authorization. We have implemented these protocols in a prototype and report preliminary results of our evaluation.

- Invited Contributions | Pp. 1-26

Automatic Verification of Parameterized Data Structures

Jyotirmoy V. Deshmukh; E. Allen Emerson; Prateek Gupta

Verifying correctness of programs operating on data structures has become an integral part of software verification. A method is a program that acts on an input data structure (modeled as a graph) and produces an output data structure. The problem for such methods can be defined as follows: Given a method and a property of the input graphs, we wish to verify that for all input graphs, parameterized by their size, the output graphs also satisfy the property. We present an automated approach to verify that a given method a given property for a large class of methods. Examples include reversals of linked lists, insertion, deletion and iterative modification of nodes in directed graphs. Our approach draws on machinery from automata theory and temporal logic. For a useful class of data structures and properties, our solution is polynomial in the size of the method and size of the property specification.

- Parametrization and Slicing | Pp. 27-41

Parameterized Verification of -Calculus Systems

Ping Yang; Samik Basu; C. R. Ramakrishnan

In this paper we present an automatic verification technique for parameterized systems where the subsystem behavior is modeled using the -calculus. At its core, our technique treats each process instance in a system as a property transformer. Given a property that we want to verify of an -process system, we use a partial model checker to infer the property ′ (stated as a formula in a sufficiently rich logic) that must hold of an ( – 1)-process system. If the sequence of formulas ,′,... thus constructed converges, and the limit is satisfied by the deadlocked process, we can conclude that the -process system satisfies . To this end, we develop a partial model checker for the -calculus that uses an expressive value-passing logic as the property language. We also develop a number of optimizations to make the model checker efficient enough for routine use, and a light-weight widening operator to accelerate convergence. We demonstrate the effectiveness of our technique by using it to verify properties of a wide variety of parameterized systems that are beyond the reach of existing techniques.

- Parametrization and Slicing | Pp. 42-57

Easy Parameterized Verification of Biphase Mark and 8N1 Protocols

Geoffrey M. Brown; Lee Pike

The Biphase Mark Protocol (BMP) and 8N1 Protocol are physical layer protocols for data transmission. We present a generic model in which timing and error values are parameterized by linear constraints, and then we use this model to verify these protocols. The verifications are carried out using SRI’s SAL model checker that combines a decision procedure with a bounded model checker for highly-automated induction proofs of safety properties over infinite-state systems. Previously, parameterized formal verification of real-time systems required mechanical theorem-proving or specialized real-time model checkers; we describe a compelling case-study demonstrating a simpler and more general approach. The verification reveals a significant error in the parameter ranges for 8N1 given in a published application note [1].

- Parametrization and Slicing | Pp. 58-72

Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs

Matthew B. Dwyer; John Hatcliff; Matthew Hoosier; Venkatesh Ranganath; Robby; Todd Wallentine

Model checking techniques have proven effective for checking a number of non-trivial concurrent object-oriented software systems. However, due to the high computational and memory costs, a variety of model reduction techniques are needed to overcome current limitations on applicability and scalability. Conventional wisdom holds that static program slicing can be an effective model reduction technique, yet anecdotal evidence is mixed, and there has been no work that has systematically studied the costs/benefits of slicing for model reduction in the context of model checking source code for realistic systems.

In this paper, we present an overview of the sophisticated Indus program slicer that is capable of handling full Java and is readily applicable to interesting off-the-shelf concurrent Java programs. Using the Indus program slicer as part of the next generation of the Bandera model checking framework, we experimentally demonstrate significant benefits from using slicing as a fully automatic model reduction technique. Our experimental results consider a number of Java systems with varying structural properties, the effects of combining slicing with other well-known model reduction techniques such as partial order reductions, and the effects of slicing for different classes of properties. Our conclusions are that slicing concurrent object-oriented source code provides significant reductions that are orthogonal to a number of other reduction techniques, and that slicing should always be applied due to its automation and low computational costs.

- Parametrization and Slicing | Pp. 73-89

New Metrics for Static Variable Ordering in Decision Diagrams

Radu I. Siminiceanu; Gianfranco Ciardo

We investigate a new class of metrics to find good variable orders for decision diagrams in symbolic state-space generation. Most of the previous work on static ordering is centered around the concept of minimum variable span, which can also be found in the literature under several other names. We use a similar concept, but applied to event span, and generalize it to a family of metrics parameterized by a moment, where the metric of moment 0 is the combined event span. Finding a good variable order is then reduced to optimizing one of these metrics, and we design extensive experiments to evaluate them. First, we investigate how the actual optimal order performs in state-space generation, when it can be computed by evaluating all possible permutations. Then, we study the performance of these metrics on selected models and compare their impact on two different state-space generation algorithms: classic breadth-first and our own saturation strategy. We conclude that the new metric of moment 1 is the best choice. In particular, the saturation algorithm seems to benefit the most from using it, as it achieves the better performance in nearly 80% of the cases.

- Symbolic Techniques | Pp. 90-104

Widening ROBDDs with Prime Implicants

Neil Kettle; Andy King; Tadeusz Strzemecki

Despite the ubiquity of ROBDDs in program analysis, and extensive literature on ROBDD minimisation, there is a dearth of work on approximating ROBDDs. The need for approximation arises because many ROBDD operations result in an ROBDD whose size is quadratic in the size of the inputs. Furthermore, if ROBDDs are used in abstract interpretation, the running time of the analysis is related not only to the complexity of the individual ROBDD operations but also the number of operations applied. The number of operations is, in turn, constrained by the number of times a Boolean function can be weakened before stability is achieved. This paper proposes a widening that can be used to both constrain the size of an ROBDD and also ensure that the number of times that it is weakened is bounded by some given constant. The widening can be used to either systematically approximate from above (i.e. derive a weaker function) or below (i.e. infer a stronger function).

- Symbolic Techniques | Pp. 105-119

Efficient Guided Symbolic Reachability Using Reachability Expressions

Dina Thomas; Supratik Chakraborty; Paritosh Pandya

Asynchronous systems consist of a set of transitions which are non-deterministically chosen and executed. We present a theory of guiding symbolic reachability in such systems by scheduling clusters of transitions. A theory of reachability expressions which specify the schedules is presented. This theory allows proving equivalence of different schedules which may have radically different performance in BDD-based search. We present experimental evidence to show that optimized reachability expressions give rise to significant performance advantages. The profiling is carried out in the NuSMV framework using examples from discrete timed automata and circuits with delays. A variant tool called NuSMV-DP has been developed for interpreting reachability expressions to carry out the experiments.

- Symbolic Techniques | Pp. 120-134

: Tight Integration of and Approaches in a Separation Logic Solver

Malay K Ganai; Muralidhar Talupur; Aarti Gupta

Existing Separation Logic () solvers can be broadly classified as or each with its own merits and de-merits. We propose a novel Separation Logic Solver that combines the strengths of both these approaches and provides a robust performance over a wide set of benchmarks. The solver works in two phases: and . In the , it allocates non-uniform ranges for variables appearing in separation predicates. This phase is similar to previous small domain encoding approaches, but uses a novel algorithm with 1-2 orders of magnitude improvement in performance and smaller ranges for variables. Furthermore, the Separation Logic formula is not transformed into an equi-satisfiable Boolean formula in one step, but rather done lazily in the following phase. In the , uses a lazy refinement approach to search for a satisfying model . Thus, any partially DL-theory consistent model can be discarded if it can not be satisfied within the allocated ranges. Note the crucial difference: Moreover, we dynamically refine the allocated ranges and search for a feasible solution within the updated ranges. This combined approach benefits from both the smaller search space (as in eager approaches) and also from the theory-specific graph-based algorithms (characteristic of lazy approaches). Experimental results show that our method is robust and always better than or comparable to state-of-the art solvers.

- Satisfiability | Pp. 135-150

SAT-Based Software Certification

Sagar Chaki

We formalize a notion of witnesses for satisfaction of linear temporal logic specifications by infinite state programs. We show how such witnesses may be constructed via predicate abstraction, and validated by generating verification conditions and proving them. We propose the use of SAT-based theorem provers and resolution proofs in proving these verification conditions. In addition to yielding extremely compact proofs, a SAT-based approach overcomes several limitations of conventional theorem provers when applied to the verification of programs written in real-life programming languages. We also formalize a notion of witnesses of simulation conformance between infinite state programs and finite state machine specifications. We present algorithms to construct simulation witnesses of minimal size by solving pseudo-Boolean constraints. We present experimental results on several non-trivial benchmarks which suggest that a SAT-based approach can yield extremely compact proofs, in some cases by a factor of over 10, when compared to existing non-SAT-based theorem provers.

- Satisfiability | Pp. 151-166