We propose a framework to prove almost sure termination for probabilistic programs with
real valued variables. It is based on ranking supermartingales, a notion analogous to …

Probabilistic programs extend classical imperative programs with real-valued random
variables and random branching. The most basic liveness property for such programs is the …

Program termination is a classic non-safety property whose falsification cannot in general be
witnessed by a finite trace. This makes testing for non-termination challenging, and also a …

We present a novel approach to termination analysis. In a first step, the analysis uses a
program as a black-box which exhibits only a finite set of sample traces. Each sample trace …

We present the open-source tool T2, the first public release from the TERMINATOR project
[9]. T2 has been extended over the past decade to support automatic temporal-logic proving …

This report describes the 3rd International Competition on Software Verification (SV-COMP
2014), which is the third edition of a thorough comparative evaluation of fully automatic …

Until recently, model checking and data-flow analysis—two traditional approaches to
software verification—were used independently and in isolation for solving similar problems …

Termination proving has traditionally been based on the search for (possibly lexicographic)
ranking functions. In recent years, however, the discovery of termination proof techniques …

We present a new method for the constraint-based synthesis of termination arguments for
linear loop programs based on linear ranking templates. Linear ranking templates are …

While model checking safety of infinite-state systems by inferring state invariants has
steadily improved recently, most verification tools still rely on a technique based on bounded …