Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2012 | Buch

Computer-Aided Cryptographic Proofs Kapitel lesen Erstes Kapitel lesen

Static Analysis

19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings

herausgegeben von: Antoine Miné, David Schmidt

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the thoroughly refereed proceedings of the 19th International Symposium on Static Analysis, SAS 2012, held in Deauville, France, in September 2012. The 25 revised full papers presented together with 4 invited talks were selected from 62 submissions. The papers address all aspects of static analysis, including abstract domains, abstract interpretation, abstract testing, bug detection, data flow analysis, model checking, new applications, program transformation, program verification, security analysis, theoretical frameworks, and type checking.

Inhaltsverzeichnis

Frontmatter

Invited Talks

Computer-Aided Cryptographic Proofs
Abstract
Provable security [6] is at the heart of modern cryptography. It advocates a mathematical approach in which the security of new cryptographic constructions is defined rigorously, and provably reduced to one or several assumptions, such as the hardness of a computational problem, or the existence of an ideal functionality. A typical provable security statement is of the form: for all adversary \(\mathcal{A}\) against the cryptographic construction \(\mathcal{S}\), there exists an adversary \(\mathcal{B}\) against a security assumption \(\mathcal{H}\), such that if \(\mathcal{A}\) has a high probability of breaking the scheme \(\mathcal{S}\) in time t, then \(\mathcal{B}\) has a high probability of breaking the assumption \(\mathcal{H}\) in time t′ (defined as a function of t).
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin
A Voyage to the Deep-Heap
Abstract
This talk is the diary of a journey that brought the theoretical advances of Separation Logic all the way to a commercial static analyzer. It reports on some of the key insights which made this journey possible. It reviews the difficulties we have encountered along the way, the present status, and some of the challenges that remain open.
I have shared this journey with Cristiano Calcagno, Peter O’Hearn, and Hongseok Yang.
Dino Distefano
Semantics and Analyses for JavaScript and the Web
Abstract
The Web’s lingua franca, JavaScript, is a large and complex language with an unconventional object model, a highly dynamic semantics, and many nonorthogonal features. We therefore defined λ JS , a core language for JavaScript that presents just a small set of essential constructs. This core language was designed to be friendly to the needs of analysis and proof.
Shriram Krishnamurthi
Efficient May Happen in Parallel Analysis for Async-Finish Parallelism
Abstract
For concurrent and parallel languages, the may-happen-in-parallel (MHP) decision problem asks, given two actions in the program, if there is an execution in which they can execute in parallel. Closely related, the MHP computation problem asks, given a program, which pairs of statements may happen in parallel. MHP analysis is the basis for many program analysis problems, such as data race detection and determinism checking, and researchers have devised MHP analyses for a variety of programming models.
We present algorithms for static MHP analysis of a storeless abstraction of X10-like languages that have async-finish parallelism and procedures. For a program of size n, our first algorithm solves the MHP decision problem in O(n) time, via a reduction to constrained dynamic pushdown networks (CDPNs). Our second algorithm solves the MHP computation problem in O(n · max (n, k)) time, where k is a statically determined upper bound on the number of pairs that may happen in parallel. The second algorithm first runs a type-based analysis that produces a set of candidate pairs, and then it runs the decision procedure on each of those pairs. For programs without recursion, the type-based analysis is exact and gives an output-sensitive algorithm for the MHP computation problem, while for recursive programs, the type-based analysis may produce spurious pairs that the decision procedure will then remove. Our experiments on a large suite of X10 benchmarks suggest that our approach scales well. Our experiments also show that while k is O(n 2) in the worst case, k is often O(n) in practice.
Jonathan K. Lee, Jens Palsberg, Rupak Majumdar, Hong Hong

Contributed Papers

Modular Static Analysis with Zonotopes
Abstract
Being able to analyze programs function by function, or module by module is a key ingredient to scalable static analyses. The main difficulty for modular static analysis is to be able to do so while not losing too much precision. In this paper, we present a new summary-based approach that builds on previous work of the authors, a zonotopic functional abstraction, that is economical both in space and time complexity. This approach has been implemented, and experiments on numerical programs, reported here, show that this approach is very efficient, and that we still obtain precise analyses in realistic cases.
Eric Goubault, Sylvie Putot, Franck Védrine
Polyhedral Analysis Using Parametric Objectives
Abstract
The abstract domain of polyhedra lies at the heart of many program analysis techniques. However, its operations can be expensive, precluding their application to polyhedra that involve many variables. This paper describes a new approach to computing polyhedral domain operations. The core of this approach is an algorithm to calculate variable elimination (projection) based on parametric linear programming. The algorithm enumerates only non-redundant inequalities of the projection space, hence permits anytime approximation of the output.
Jacob M. Howe, Andy King
Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases
Abstract
We propose a static analysis for computing polynomial invariants for imperative programs. The analysis is derived from an abstract interpretation of a backwards semantics, and computes pre-conditions for equalities like g = 0 to hold at the end of execution. A distinguishing feature of the technique is that it computes polynomial loop invariants without resorting to Gröbner base computations. The analysis uses remainder computations over parameterized polynomials in order to handle conditionals and loops efficiently. The algorithm can analyse and find a large majority of loop invariants reported previously in the literature, and executes significantly faster than implementations using Gröbner bases.
David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner
A New Abstract Domain for the Representation of Mathematically Equivalent Expressions
Abstract
Exact computations being in general not tractable for computers, they are approximated by floating-point computations. This is the source of many errors in numerical programs. Because the floating-point arithmetic is not intuitive, these errors are very difficult to detect and to correct by hand and we consider the problem of automatically synthesizing accurate formulas. We consider that a program would return an exact result if the computations were carried out using real numbers. In practice, roundoff errors arise during the execution and these errors are closely related to the way formulas are written. Our approach is based on abstract interpretation. We introduce Abstract Program Equivalence Graphs (APEGs) to represent in polynomial size an exponential number of mathematically equivalent expressions. The concretization of an APEG yields expressions of very different shapes and accuracies. Then, we extract optimized expressions from APEGs by searching the most accurate concrete expressions among the set of represented expressions.
Arnault Ioualalen, Matthieu Martel
An Abstract Domain to Infer Types over Zones in Spreadsheets
Abstract
Spreadsheet languages are very commonly used, by large user bases, yet they are error prone. However, many semantic issues and errors could be avoided by enforcing a stricter type discipline. As declaring and specifying type information would represent a prohibitive amount of work for users, we propose an abstract interpretation based static analysis for spreadsheet programs that infers type constraints over zones of spreadsheets, viewed as two-dimensional arrays. Our abstract domain consists in a cardinal power from a numerical abstraction describing zones in a spreadsheet to an abstraction of cell values, including type properties. We formalize this abstract domain and its operators (transfer functions, join, widening and reduction) as well as a static analysis for a simplified spreadsheet language. Last, we propose a representation for abstract values and present an implementation of our analysis.
Tie Cheng, Xavier Rival
Bilateral Algorithms for Symbolic Abstraction
Abstract
Given a concrete domain \(\mathcal{C}\), a concrete operation \(\tau: \mathcal{C} \to \mathcal{C}\), and an abstract domain \(\mathcal{A}\), a fundamental problem in abstract interpretation is to find the best abstract transformer \(\tau^{\#}: \mathcal{A} \to \mathcal{A}\) that over-approximates τ. This problem, as well as several other operations needed by an abstract interpreter, can be reduced to the problem of symbolic abstraction: the symbolic abstraction of a formula ϕ in logic \(\mathcal{L}\), denoted by \(\widehat{\alpha}(\varphi)\), is the best value in \(\mathcal{A}\) that over-approximates the meaning of ϕ. When the concrete semantics of τ is defined in \(\mathcal{L}\) using a formula ϕ τ that specifies the relation between input and output states, the best abstract transformer τ # can be computed as \(\widehat{\alpha}(\varphi_\tau)\).
In this paper, we present a new framework for performing symbolic abstraction, discuss its properties, and present several instantiations for various logics and abstract domains. The key innovation is to use a bilateral successive-approximation algorithm, which maintains both an over-approximation and an under-approximation of the desired answer.
Aditya Thakur, Matt Elder, Thomas Reps
Making Abstract Interpretation Incomplete: Modeling the Potency of Obfuscation
Abstract
Recent studies on code protection showed that incompleteness, in the abstract interpretation framework, has a key role in understanding program obfuscation. In particular, it is well known that completeness corresponds to exactness of a given analysis for a fixed program semantics, hence incompleteness implies the imprecision of an analysis with respect to the program semantics. In code protection, if the analysis corresponds to attacker capability of understanding a program semantics, then to study incompleteness means to study how to make an attacker harmless. We recently showed that this is possible by transforming the program semantics towards incompleteness, which corresponds to a code obfuscation. In this paper, we show that incompleteness can be induced also by transforming abstract domains. In this way we can associate with each obfuscated program (semantics) the most imprecise, harmless, analysis. We show that, for both the forms of completeness, backward and forward, we can uniquely simplify domains towards incompleteness, while in general it is not possible to uniquely refine domains. Finally, we show some examples of known code protection techniques that can be characterized in the new framework of abstract interpretation incompleteness.
Roberto Giacobazzi, Isabella Mastroeni
Invariant Generation for Parametrized Systems Using Self-reflection
(Extended Version)
Abstract
We examine the problem of inferring invariants for parametrized systems. Parametrized systems are concurrent systems consisting of an a priori unbounded number of process instances running the same program. Such systems are commonly encountered in many situations including device drivers, distributed systems, and robotic swarms. In this paper we describe a technique that enables leveraging off-the-shelf invariant generators designed for sequential programs to infer invariants of parametrized systems. The central challenge in invariant inference for parametrized systems is that naïvely exploding the transition system with all interleavings is not just impractical but impossible. In our approach, the key enabler is the notion of a reflective abstraction that we prove has an important correspondence with inductive invariants. This correspondence naturally gives rise to an iterative invariant generation procedure that alternates between computing candidate invariants and creating reflective abstractions.
Alejandro Sanchez, Sriram Sankaranarayanan, César Sánchez, Bor-Yuh Evan Chang
Automatic Fence Insertion in Integer Programs via Predicate Abstraction
Abstract
We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous approaches to this problem, which allow only variables of finite domain, we target programs with (unbounded) integer variables. The problem is difficult because it has two different sources of infiniteness: unbounded store buffers and unbounded integer variables. Our framework consists of three main components: (1) a finite abstraction technique for the store buffers, (2) a finite abstraction technique for the integer variables, and (3) a counterexample guided abstraction refinement loop of the model obtained from the combination of the two abstraction techniques. We have implemented a prototype based on the framework and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing methods.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine
Control Flow Analysis for the Join Calculus
Abstract
Since first being described, the Join Calculus has been incorporated into a variety of languages as an alternative concurrency primitive. While there has been some work on efficient library implementation of the calculus, there has been little on statically analysing and transforming it. This work explores adapting conventional analysis techniques to the Join Calculus. In particular, we present three variations of control flow analysis for a flattened version, and consider two important optimisations: inlining and queue bounding.
Peter Calvert, Alan Mycroft
When the Decreasing Sequence Fails
Abstract
The classical method for program analysis by abstract interpretation consists in computing a increasing sequence with widening, which converges towards a correct solution, then computing a decreasing sequence of correct solutions without widening. It is generally admitted that, when the decreasing sequence reaches a fixpoint, it cannot be improved further. As a consequence, all efforts for improving the precision of an analysis have been devoted to improving the limit of the increasing sequence. In this paper, we propose a method to improve a fixpoint after its computation. The method consists in projecting the solution onto well-chosen components and to start again increasing and decreasing sequences from the result of the projection.
Nicolas Halbwachs, Julien Henry
Loop Leaping with Closures
Abstract
Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops starting from the innermost loop and proceeding in a bottom-up fashion considering one more loop at a time. Loop leaping contrasts with classical approaches to finding loop invariants that are iterative; loop leaping is compositional requiring each stratum in the nest of loops to be considered exactly once. The approach is attractive in predicate abstraction where disjunctive domains are increasingly used that present long ascending chains. This paper proposes a simple and an efficient approach for loop leaping for these domains based on viewing loops as closure operators.
Sebastian Biallas, Jörg Brauer, Andy King, Stefan Kowalewski
Path-Sensitive Backward Slicing
Abstract
Backward slicers are typically path-insensitive (i.e., they ignore the evaluation of predicates at conditional branches) often producing too big slices. Though the effect of path-sensitivity is always desirable, the major challenge is that there are, in general, an exponential number of predicates to be considered. We present a path-sensitive backward slicer and demonstrate its practicality with real C programs. The crux of our method is a symbolic execution-based algorithm that excludes spurious dependencies lying on infeasible paths and avoids imprecise joins at merging points while reusing dependencies already computed by other paths, thus pruning the search space significantly.
Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa
Symbolic Learning of Component Interfaces
Abstract
Given a white-box component https://static-content.springer.com/image/chp%3A10.1007%2F978-3-642-33125-1_18/978-3-642-33125-1_18_IEq1_HTML.gif with specified unsafe states, we address the problem of automatically generating an interface that captures safe orderings of invocations of https://static-content.springer.com/image/chp%3A10.1007%2F978-3-642-33125-1_18/978-3-642-33125-1_18_IEq2_HTML.gif ’s public methods. Method calls in the generated interface are guarded by constraints on their parameters. Unlike previous work, these constraints are generated automatically through an iterative refinement process. Our technique, named Psyco (Predicate-based SYmbolic COmpositional reasoning), employs a novel combination of the L* automata learning algorithm with symbolic execution. The generated interfaces are three-valued, capturing whether a sequence of method invocations is safe, unsafe, or its effect on the component state is unresolved by the symbolic execution engine. We have implemented Psyco as a new prototype tool in the JPF open-source software model checking platform, and we have successfully applied it to several examples.
Dimitra Giannakopoulou, Zvonimir Rakamarić, Vishwanath Raman
Liveness-Based Pointer Analysis
Abstract
Precise flow- and context-sensitive pointer analysis (FCPA) is generally considered prohibitively expensive for large programs; most tools relax one or both of the requirements for scalability. We argue that precise FCPA has been over-harshly judged—the vast majority of points-to pairs calculated by existing algorithms are never used by any client analysis or transformation because they involve dead variables. We therefore formulate a FCPA in terms of a joint points-to and liveness analysis which we call L-FCPA. We implemented a naive L-FCPA in GCC-4.6.0 using linked lists. Evaluation on SPEC2006 showed significant increase in the precision of points-to pairs compared to GCC’s analysis. Interestingly, our naive implementation turned out to be faster than GCC’s analysis for all programs under 30kLoC. Further, L-FCPA showed that fewer than 4% of basic blocks had more than 8 points-to pairs. We conclude that the usable points-to information and the required context information is small and sparse and argue that approximations (e.g. weakening flow or context sensitivity) are not only undesirable but also unnecessary for performance.
Uday P. Khedker, Alan Mycroft, Prashant Singh Rawat
Succinct Representations for Abstract Interpretation
Combined Analysis Algorithms and Experimental Evaluation
Abstract
Abstract interpretation techniques can be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. SMT-solving techniques and sparse representations of paths and sets of paths avoid this pitfall.
We improve previously proposed techniques for guided static analysis and the generation of disjunctive invariants by combining them with techniques for succinct representations of paths and symbolic representations for transitions based on static single assignment.
Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages.
Julien Henry, David Monniaux, Matthieu Moy
Craig Interpretation
Abstract
Abstract interpretation (AI) is one of the most scalable automated approaches to program verification available today. To achieve efficiency, many steps of the analysis, e.g., joins and widening, lose precision. As a result, AI often produces false alarms, coming from the inability to find a safe inductive invariant even when it exists in a chosen abstract domain.
To tackle this problem, we present Vinta, an iterative algorithm that uses Craig interpolants to refine and guide AI away from false alarms. Vinta is based on a novel refinement strategy that capitalizes on recent advances in SMT and interpolation-based verification to (a) find counterexamples to justify alarms produced by AI, and (b) to strengthen an invariant to exclude alarms that cannot be justified. The refinement process continues until either a safe inductive invariant is computed, a counterexample is found, or resources are exhausted. This strategy allows Vinta to recover precision lost in many AI steps, and even to compute inductive invariants that are inexpressible in the chosen abstract domain (e.g., by adding disjunctions and new terms).
We have implemented Vinta and compared it against top verification tools from the recent software verification competition. Our results show that Vinta outperforms state-of-the-art verification tools.
Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik
Satisfiability Solvers Are Static Analysers
Abstract
This paper shows that several propositional satisfiability algorithms compute approximations of fixed points using lattice-based abstractions. The Boolean Constraint Propagation algorithm (bcp) is a greatest fixed point computation over a lattice of partial assignments. The original algorithm of Davis, Logemann and Loveland refines bcp by computing a set of greatest fixed points. The Conflict Driven Clause Learning algorithm alternates between overapproximate deduction with bcp, and underapproximate abduction, with conflict analysis. Thus, in a precise sense, satisfiability solvers are abstract interpreters. Our work is the first step towards a uniform framework for the design and implementation of satisfiability algorithms, static analysers and their combination.
Vijay D’Silva, Leopold Haller, Daniel Kroening
A Generalization of Stålmarck’s Method
Abstract
This paper gives an account of Stålmarck’s method for validity checking of propositional-logic formulas, and explains each of the key components in terms of concepts from the field of abstract interpretation. We then use these insights to present a framework for propositional-logic validity-checking algorithms that is parametrized by an abstract domain and operations on that domain. Stålmarck’s method is one instantiation of the framework; other instantiations lead to new decision procedures for propositional logic.
Aditya Thakur, Thomas Reps
A Structural Soundness Proof for Shivers’s Escape Technique
A Case for Galois Connections
Abstract
Shivers’s escape technique enables one to analyse the control flow of higher-order program fragments. It is widely used, but its soundness has never been proven. In this paper, we present the first soundness proof for the technique. Our proof is structured as a composition of Galois connections and thus rests on the foundations of abstract interpretation.
Jan Midtgaard, Michael D. Adams, Matthew Might
Modular Heap Analysis for Higher-Order Programs
Abstract
We consider the problem of computing summaries for procedures that soundly capture the effect of calling a procedure on program state that includes a mutable heap. Such summaries are the basis for a compositional program analysis and key to scalability. Higher order procedures contain callbacks (indirect calls to procedures specified by callers). The use of such callbacks and higher-order features are becoming increasingly widespread and commonplace even in mainstream imperative languages such as C # and Java. Such callbacks complicate compositional analysis and the construction of procedure summaries. We present an abstract-interpretation based approach to computing summaries (of a procedure’s effect on a mutable heap) in the presence of callbacks in a simple imperative language. We present an empirical evaluation of our approach.
Ravichandhran Madhavan, G. Ramalingam, Kapil Vaswani
Binary Reachability Analysis of Higher Order Functional Programs
Abstract
A number of recent approaches for proving program termination rely on transition invariants - a termination argument that can be constructed incrementally using abstract interpretation. These approaches use binary reachability analysis to check if a candidate transition invariant holds for a given program. For imperative programs, its efficient implementation can be obtained by a reduction to reachability analysis, for which practical tools are available. In this paper, we show how a binary reachability analysis can be put to work for proving termination of higher order functional programs.
Ruslán Ledesma-Garza, Andrey Rybalchenko
On the Limits of the Classical Approach to Cost Analysis
Abstract
The classical approach to static cost analysis is based on transforming a given program into cost relations and solving them into closed-form upper-bounds. It is known that for some programs, this approach infers upper-bounds that are asymptotically less precise than the actual cost. As yet, it was assumed that this imprecision is due to the way cost relations are solved into upper-bounds. In this paper: (1) we show that this assumption is partially true, and identify the reason due to which cost relations cannot precisely model the cost of such programs; and (2) to overcome this imprecision, we develop a new approach to cost analysis, based on SMT and quantifier elimination. Interestingly, we find a strong relation between our approach and amortised cost analysis.
Diego Esteban Alonso-Blas, Samir Genaim
Termination Proofs for Linear Simple Loops
Abstract
Analysis of termination and other liveness properties of an imperative program can be reduced to termination proof synthesis for simple loops, i.e., loops with only variable updates in the loop body. Among simple loops, the subset of Linear Simple Loops (LSLs) is particular interesting because it is common in practice and expressive in theory. Existing techniques can successfully synthesize a linear ranking function for an LSL if there exists one. However, when a terminating LSL does not have a linear ranking function, these techniques fail. In this paper we describe an automatic method that generates proofs of universal termination for LSLs based on the synthesis of disjunctive ranking relations. The method repeatedly finds linear ranking functions on parts of the state space and checks whether the transitive closure of the transition relation is included in the union of the ranking relations. Our method extends the work of Podelski and Rybalchenko [27]. We have implemented a prototype of the method and have shown experimental evidence of the effectiveness of our method.
Hong Yi Chen, Shaked Flur, Supratik Mukhopadhyay
Finding Non-terminating Executions in Distributed Asynchronous Programs
Abstract
Programming distributed and reactive asynchronous systems is complex due to the lack of synchronization between concurrently executing tasks, and arbitrary delay of message-based communication. As even simple programming mistakes have the capability to introduce divergent behavior, a key liveness property is eventual quiescence: for any finite number of external stimuli (e.g., client-generated events), only a finite number of internal messages are ever created.
In this work we propose a practical three-step reduction-based approach for detecting divergent executions in asynchronous programs. As a first step, we give a code-to-code translation reducing divergence of an asynchronous program P to completed state-reachability—i.e., reachability to a given state with no pending asynchronous tasks—of a polynomially-sized asynchronous program P′. In the second step, we give a code-to-code translation under-approximating completed state-reachability of P′ by state-reachability of a polynomially-sized recursive sequential program P′′(K), for the given analysis parameter K ∈ ℕ. Following [8]’s delay-bounding approach, P′′(K) encodes a subset of P′’s, and thus of P’s, behaviors by limiting scheduling nondeterminism. As K is increased, more possibly divergent behaviors of P are considered, and in the limit as K approaches infinity, our reduction is complete for programs with finite data domains. As the final step we give the resulting state-reachability query to an off-the-shelf SMT-based sequential program verification tool.
We demonstrate the feasibility of our approach by implementing a prototype analysis tool called Alive, which detects divergent executions in several hand-coded variations of textbook distributed algorithms. As far as we are aware, our easy-to-implement prototype is the first tool which automatically detects divergence for distributed and reactive asynchronous programs.
Michael Emmi, Akash Lal
Backmatter
Metadaten
Titel
Static Analysis
herausgegeben von
Antoine Miné
David Schmidt
Copyright-Jahr
2012
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-33125-1
Print ISBN
978-3-642-33124-4
DOI
https://doi.org/10.1007/978-3-642-33125-1

Premium Partner

    Bildnachweise