Verification, Model Checking, and Abstract Interpretation
From MaRDI portal
Publication:5711496
DOI10.1007/b105073zbMath1111.68514MaRDI QIDQ5711496
Zohar Manna, Henny B. Sipma, Sriram Sankaranarayanan
Publication date: 6 December 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b105073
90C08: Special problems of linear programming (transportation, multi-index, data envelopment analysis, etc.)
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
The Abstract Domain of Parallelotopes, TreeKs: A Functor to Make Numerical Abstract Domains Scalable, An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations, Proving Termination by Policy Iteration, Complexity and Algorithms for Monomial and Clausal Predicate Abstraction, Narrowing Operators on Template Abstract Domains, Invariant Synthesis for Combined Theories, Validating numerical semidefinite programming solvers for polynomial invariants, A topological method for finding invariant sets of continuous systems, Symbolic analysis of linear hybrid automata -- 25 years later, Abstract interpretation meets convex optimization, Tropical linear-fractional programming and parametric mean payoff games, Acceleration of the abstract fixpoint computation in numerical program analysis, Discovering invariants via simple component analysis, Reachability computation for polynomial dynamical systems, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness, A minimalistic look at widening operators, Property-directed incremental invariant generation, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, Applications of polyhedral computations to the analysis and verification of hardware and software systems, Improving the results of program analysis by abstract interpretation beyond the decreasing sequence, Descending chains and narrowing on template abstract domains, Experimental evaluation of numerical domains for inferring ranges, On the efficiency of convex polyhedra, Numerical invariants through convex relaxation and max-strategy iteration, Template polyhedra and bilinear optimization, A new abstraction framework for affine transformers, Certification of real inequalities: templates and sums of squares, Policy iteration in finite templates domain, Abstract Fixpoint Computations with Numerical Acceleration Methods, View-Augmented Abstractions, Static Analysis by Abstract Interpretation: A Mathematical Programming Approach, A Note on the Inversion Join for Polyhedral Analysis, Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants, Template-Based Unbounded Time Verification of Affine Hybrid Automata, Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT, Finding Relevant Templates via the Principal Component Analysis, Sound Bit-Precise Numerical Domains, Linear Absolute Value Relation Analysis, Generalizing the Template Polyhedral Domain, Improving Strategies via SMT Solving, Combining Model Checking and Deduction, Counterexample-Guided Refinement of Template Polyhedra, Logahedra: A New Weakly Relational Domain
Uses Software
