VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
Abstract. We present a multi-pass interprocedural analysis and transformation for the functional aggregate update problem. Our solution handles untyped programs, including unrestri...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
Abstract. Symmetry reduction is a technique to alleviate state explosion in model checking by replacing a model of replicated processes with a bisimilar quotient model. The size of...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
Abstract. We introduce Subpolyhedra (SubPoly) a new numerical abstract domain to infer and propagate linear inequalities. SubPoly is as expressive as Polyhedra, but it drops some o...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
lue Abstraction for Verifying Linearizability Viktor Vafeiadis Microsoft Research, Cambridge, UK This paper presents a novel abstraction for heap-allocated data structures that kee...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
The Rely-Guarantee approach is a well-known compositional method for proving Hoare logic properties of concurrent programs. In this approach, predicates in the proof must be proved...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
Given a 3-valued abstraction of a program (possibly generated using rogram analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
Vectors and bags are basic collection data structures, which are used frequently in programs and specifications. Reasoning about these data structures is supported by established ...
VMCAI
2009
Springer
13 years 11 months ago
2009
Springer
A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a give...