Sciweavers

VMCAI
2005
Springer
14 years 4 months ago
Termination of Polynomial Programs
We present a technique to prove termination of multipath polynomial programs, an expressive class of loops that enables practical traction and analysis. The technique is based on ļ...
Aaron R. Bradley, Zohar Manna, Henny B. Sipma
VMCAI
2005
Springer
14 years 4 months ago
Checking Herbrand Equalities and Beyond
A Herbrand equality between expressions in a program is an equality which holds relative to the Herbrand interpretation of operators. We show that the problem of checking validity ...
Markus Müller-Olm, Oliver Rüthing, Helmu...
VMCAI
2005
Springer
14 years 4 months ago
An Overview of Semantics for the Validation of Numerical Programs
Interval computations, stochastic arithmetic, automatic diļ¬€erentiation, etc.: much work is currently done to estimate and to improve the numerical accuracy of programs but few c...
Matthieu Martel
VMCAI
2005
Springer
14 years 4 months ago
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists
Roman Manevich, Eran Yahav, Ganesan Ramalingam, Sh...
VMCAI
2005
Springer
14 years 4 months ago
Optimizing Bounded Model Checking for Linear Hybrid Systems
Bounded model checking (BMC) is an automatic veriļ¬cation method that is based on a ļ¬nite unfolding of the systemā€™s transition relation. BMC has been successfully applied, in ...
Erika Ábrahám, Bernd Becker, Felix K...