scientific article

zbMath0978.68095MaRDI QIDQ2769578

Henny B. Sipma, Michael A. Colón

Publication date: 5 February 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2031/20310067

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (25)

Termination of Single-Path Polynomial Loop Programs ⋮ Termination of floating-point computations ⋮ The octagon abstract domain ⋮ Recent advances in program verification through computer algebra ⋮ Termination of linear programs with nonlinear constraints ⋮ Generating exact nonlinear ranking functions by symbolic-numeric hybrid method ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ What's decidable about discrete linear dynamical systems? ⋮ Discovering invariants via simple component analysis ⋮ PPLite: zero-overhead encoding of NNC polyhedra ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Property-directed incremental invariant generation ⋮ Ranking function synthesis for bit-vector relations ⋮ A new look at the automatic synthesis of linear ranking functions ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Unnamed Item ⋮ Decision Procedures for Automating Termination Proofs ⋮ Proving Termination of Integer Term Rewriting ⋮ Automata-Based Termination Proofs ⋮ Applications of polyhedral computations to the analysis and verification of hardware and software systems ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ Ranking Functions for Linear-Constraint Loops ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ Algebraic model checking for discrete linear dynamical systems ⋮ Witness to non-termination of linear programs

This page was built for publication: