Proving Conditional Termination

13 years 6 months ago

Download www.cs.tau.ac.il

Abstract. We describe a method for synthesizing reasonable underapproximations to weakest preconditions for termination--a long-standing open problem. The paper provides experimental evidence to demonstrate the usefulness of the new procedure.

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Ryb

Real-time Traffic

CAV 2008 | Hardware | Long-standing Open Problem | Reasonable Underapproximations |

claim paper

» Proving Termination by Divergence

» Applying Static Analysis Techniques for Inferring Termination Conditions of Logic Programs

» Proving operational termination of membership equational programs

» Proving termination of membership equational programs

» Proving Liveness with Fairness Using Rewriting

» Constraint Propagation for Soft Constraints Generalization and Termination Conditions

» Termination of Innermost ContextSensitive Rewriting Using Dependency Pairs

» Reducing RightHand Sides for Termination

Post Info
More Details (n/a)

Added	12 Oct 2010
Updated	12 Oct 2010
Type	Conference
Year	2008
Where	CAV
Authors	Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv

Comments (0)

Sciweavers

Proving Conditional Termination

CAV 2008 | Hardware | Long-standing Open Problem | Reasonable Underapproximations |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers