Static Analysis Book

	Static Program Analysis via 3-Valued Logic	1
	Open Modeling in Multi-stakeholder Distributed Systems: Research and Tool Challenges	2
	An Algebraic Approach to the Static Analysis of Concurrent Software	3
	Polynomial Constants Are Decidable	4
	Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi	20
	Nonuniform Alias Analysis of Recursive Data Structures and Arrays	36
	Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes	52
	Automated Verification of Concurrent Linked Lists with Counters	69
	Backward Type Inference Generalises Type Checking	85
	More Precise Yet Efficient Type Inference for Logic Programs	102
	A Few Graph-Based Relational Numerical Abstract Domains	117
	Static Analysis of the Numerical Stability of Loops	133
	On Termination of Logic Programs with Floating Point Computations	151
	Modular Control Flow Analysis for Libraries	165
	An Efficient Inclusion-Based Points-To Analysis for Strictly-Typed Languages	180
	Compactly Representing First-Order Structures for Static Analysis	196
	Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library	213
	Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis	230
	Improving the Precision of Equality-Based Dataflow Analyses	247
	Guaranteed Optimization: Proving Nullspace Properties of Compilers	263
	Representation Analysis for Coercion Placement	278
	Pipeline Modeling for Timing Analysis	294
	Analysing Approximate Confinement under Uniform Attacks	310
	An Improved Constraint-Based System for the Verification of Security Protocols	326
	From Secrecy to Authenticity in Security Protocols	342
	Security Typings by Abstract Interpretation	360
	Static Confidentiality Enforcement for Distributed Programs	376
	Refinement of LTL Formulas for Abstract Model Checking	395
	Making Abstract Model Checking Strongly Preserving	411
	Semantics for Abstract Interpretation-Based Static Analyzes of Temporal Properties	428
	Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation	444
	States vs. Traces in Model Checking by Abstract Interpretation	461
	Reuse of Results in Termination Analysis of Typed Logic Programs	477
	Finiteness Analysis in Polynomial Time	493
	Detecting Optimal Termination Conditions of Logic Programs	509
	Author Index	527