Sciweavers

Share
VMCAI
2009
Springer
9 years 4 months ago
The Higher-Order Aggregate Update Problem
Abstract. We present a multi-pass interprocedural analysis and transformation for the functional aggregate update problem. Our solution handles untyped programs, including unrestri...
Christos Dimoulas, Mitchell Wand
VMCAI
2009
Springer
9 years 4 months ago
Extending Symmetry Reduction by Exploiting System Architecture
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...
Richard J. Trefler, Thomas Wahl
VMCAI
2009
Springer
9 years 4 months ago
SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
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...
Vincent Laviron, Francesco Logozzo
VMCAI
2009
Springer
9 years 4 months ago
Constraint-Based Invariant Inference over Predicate Abstraction
Sumit Gulwani, Saurabh Srivastava, Ramarathnam Ven...
VMCAI
2009
Springer
9 years 4 months ago
Query-Driven Program Testing
Andreas Holzer, Christian Schallhart, Michael Taut...
VMCAI
2009
Springer
9 years 4 months ago
Shape-Value Abstraction for Verifying Linearizability
lue Abstraction for Verifying Linearizability Viktor Vafeiadis Microsoft Research, Cambridge, UK This paper presents a novel abstraction for heap-allocated data structures that kee...
Viktor Vafeiadis
VMCAI
2009
Springer
9 years 4 months ago
Towards Automatic Stability Analysis for Rely-Guarantee Proofs
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...
Hasan Amjad, Richard Bornat
VMCAI
2009
Springer
9 years 4 months ago
LTL Generalized Model Checking Revisited
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...
Patrice Godefroid, Nir Piterman
VMCAI
2009
Springer
9 years 4 months ago
Deciding Extensions of the Theories of Vectors and Bags
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 ...
Patrick Maier
VMCAI
2009
Springer
9 years 4 months ago
Synthesizing Switching Logic Using Constraint Solving
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...
Ankur Taly, Sumit Gulwani, Ashish Tiwari
books