scientific article; zbMATH DE number 1701751
From MaRDI portal
zbMATH Open0978.68095MaRDI QIDQ2769578FDOQ2769578
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 of this publication is not available (Why is that?)
Cited In (31)
- Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
- Title not available (Why is that?)
- Time-bounded termination analysis for probabilistic programs with delays
- Algebraic model checking for discrete linear dynamical systems
- Decision Procedures for Automating Termination Proofs
- Property-directed incremental invariant generation
- Discovering non-terminating inputs for multi-path polynomial programs
- Termination of floating-point computations
- Automata-Based Termination Proofs
- A new look at the automatic synthesis of linear ranking functions
- Witness to non-termination of linear programs
- Discovering invariants via simple component analysis
- Applications of polyhedral computations to the analysis and verification of hardware and software systems
- PPLite: zero-overhead encoding of NNC polyhedra
- On lexicographic proof rules for probabilistic termination
- Termination of Single-Path Polynomial Loop Programs
- Ranking function synthesis for bit-vector relations
- Termination analysis of programs with multiphase control-flow
- Recent advances in program verification through computer algebra
- Proving Termination of Integer Term Rewriting
- The octagon abstract domain
- Termination of linear programs with nonlinear constraints
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- What's decidable about discrete linear dynamical systems?
- MDPs as distribution transformers: affine invariant synthesis for safety objectives
- Multiphase-linear ranking functions and their relation to recurrent sets
- Synthesizing ranking functions for loop programs via SVM
- Title not available (Why is that?)
- Ranking Templates for Linear Loops
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- Ranking Functions for Linear-Constraint Loops
Recommendations
- Verification, Model Checking, and Abstract Interpretation π π
- Ranking Function Synthesis for Bit-Vector Relations π π
- Computer Aided Verification π π
- A linear functional strategy for regularized ranking π π
- On multiphase-linear ranking functions π π
- A new look at the automatic synthesis of linear ranking functions π π
- Ranking functions and axioms for linear orders π π
- Ranking function synthesis for bit-vector relations π π
- Title not available (Why is that?) π π
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2769578)