Abstract is missing.
- Time of TimeE. Allen Emerson. 1 [doi]
- Static Verification for Code ContractsManuel Fähndrich. 2-5 [doi]
- Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework - In Memory of Amir PnueliBenjamin Goldberg. 6-21 [doi]
- Size-Change Termination and Transition InvariantsMatthias Heizmann, Neil D. Jones, Andreas Podelski. 22-50 [doi]
- Using Static Analysis in Space: Why Doing so?David Lesens. 51-70 [doi]
- Statically Inferring Complex Heap, Array, and Numeric InvariantsBill McCloskey, Thomas W. Reps, Mooly Sagiv. 71-99 [doi]
- From Object Fields to Local Variables: A Practical Approach to Field-Sensitive AnalysisElvira Albert, Puri Arenas, Samir Genaim, German Puebla, Diana V. Ramírez-Deantes. 100-116 [doi]
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart ProgramsChristophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord. 117-133 [doi]
- Deriving Numerical Abstract Domains via Principal Component AnalysisGianluca Amato, Maurizio Parton, Francesca Scozzari. 134-150 [doi]
- Concurrent Separation Logic for Pipelined ParallelizationChristian J. Bell, Andrew W. Appel, David Walker. 151-166 [doi]
- Automatic Abstraction for Intervals Using Boolean FormulaeJörg Brauer, Andy King. 167-183 [doi]
- Interval Slopes as a Numerical Abstract Domain for Floating-Point VariablesAlexandre Chapoutot. 184-200 [doi]
- A Shape Analysis for Non-linear Data StructuresRenato Cherini, Lucas Rearte, Javier O. Blanco. 201-217 [doi]
- Modelling Metamorphism by Abstract InterpretationMila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray, Kevin Coogan, Gregg M. Townsend. 218-235 [doi]
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static AnalysisIsil Dillig, Thomas Dillig, Alex Aiken. 236-252 [doi]
- Compositional Bitvector Analysis for Concurrent Programs with Nested LocksAzadeh Farzan, Zachary Kincaid. 253-270 [doi]
- Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones PreciselyThomas Martin Gawlitza, Helmut Seidl. 271-286 [doi]
- Boxes: A Symbolic Abstract Domain of BoxesArie Gurfinkel, Sagar Chaki. 287-303 [doi]
- Alternation for TerminationWilliam R. Harris, Akash Lal, Aditya V. Nori, Sriram K. Rajamani. 304-319 [doi]
- Interprocedural Analysis with Lazy PropagationSimon Holm Jensen, Anders Møller, Peter Thiemann. 320-339 [doi]
- Verifying a Local Generic Solver in CoqMartin Hofmann, Aleksandr Karbyshev, Helmut Seidl. 340-355 [doi]
- Thread-Modular Counterexample-Guided Abstraction RefinementAlexander Malkis, Andreas Podelski, Andrey Rybalchenko. 356-372 [doi]
- Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic MethodsNadir Matringe, Arnaldo Vieira Moura, Rachid Rebiha. 373-389 [doi]
- Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based MethodsJoost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, Carroll C. Morgan. 390-406 [doi]
- Abstract Interpreters for FreeMatthew Might. 407-421 [doi]
- Points-to Analysis as a System of Linear EquationsRupesh Nasre, Ramaswamy Govindarajan. 422-438 [doi]
- Strictness Meets Data FlowTom Schrijvers, Alan Mycroft. 439-454 [doi]
- Automatic Verification of Determinism for Structured Parallel ProgramsMartin T. Vechev, Eran Yahav, Raghavan Raman, Vivek Sarkar. 455-471 [doi]