Verification, Model Checking, and Abstract Interpretation
From MaRDI portal
Publication:5711496
DOI10.1007/b105073zbMath1111.68514OpenAlexW2611288859MaRDI 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
Special problems of linear programming (transportation, multi-index, data envelopment analysis, etc.) (90C08) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Improving the results of program analysis by abstract interpretation beyond the decreasing sequence ⋮ Experimental evaluation of numerical domains for inferring ranges ⋮ On the efficiency of convex polyhedra ⋮ Template-Based Unbounded Time Verification of Affine Hybrid Automata ⋮ Combining Model Checking and Deduction ⋮ Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness ⋮ A minimalistic look at widening operators ⋮ Descending chains and narrowing on template abstract domains ⋮ Symbolic analysis of linear hybrid automata -- 25 years later ⋮ Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT ⋮ Finding Relevant Templates via the Principal Component Analysis ⋮ Sound Bit-Precise Numerical Domains ⋮ 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 ⋮ Linear Absolute Value Relation Analysis ⋮ Generalizing the Template Polyhedral Domain ⋮ Improving Strategies via SMT Solving ⋮ Property-directed incremental invariant generation ⋮ Counterexample-Guided Refinement of Template Polyhedra ⋮ Numerical invariants through convex relaxation and max-strategy iteration ⋮ Reachability computation for polynomial dynamical systems ⋮ 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 ⋮ Pentagons: a weakly relational abstract domain for the efficient validation of array accesses ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ A topological method for finding invariant sets of continuous systems ⋮ Invariant Synthesis for Combined Theories ⋮ Narrowing Operators on Template Abstract Domains ⋮ 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 ⋮ Logahedra: A New Weakly Relational Domain ⋮ Applications of polyhedral computations to the analysis and verification of hardware and software systems ⋮ Template polyhedra and bilinear optimization ⋮ A new abstraction framework for affine transformers ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Certification of real inequalities: templates and sums of squares
Uses Software
