Publication:2769578
From MaRDI portal
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
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs, Ranking Functions for Linear-Constraint Loops, Recent advances in program verification through computer algebra, Generating exact nonlinear ranking functions by symbolic-numeric hybrid method, Discovering invariants via simple component analysis, Termination of linear programs with nonlinear constraints, A new look at the automatic synthesis of linear ranking functions, Termination of floating-point computations, The octagon abstract domain, Property-directed incremental invariant generation, Applications of polyhedral computations to the analysis and verification of hardware and software systems, Ranking function synthesis for bit-vector relations, Discovering non-terminating inputs for multi-path polynomial programs, Witness to non-termination of linear programs, Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods, Decision Procedures for Automating Termination Proofs, Termination of Single-Path Polynomial Loop Programs, Proving Termination of Integer Term Rewriting, Automata-Based Termination Proofs