TACAS
2009
Springer
14 years 4 months ago
2009
Springer
Abstract. We present a method which computes optimized representations for non-convex polyhedra. Our method detects so-called redundant linear constraints in these representations ...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
Abstract. We propose a static analysis framework for concurrent programs based on reduction of thread interleavings using sound invariants on the top of partial order techniques. S...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
We introduce the All-Termination(T) problem: given a termination solver, T, and a program (a set of functions), find every set of formal arguments whose consideration is sufficie...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
Abstract. Role-Based Access Control (RBAC) has been widely used for expressing access control policies. Administrative Role-Based Access Control (ARBAC) specifies how an RBAC poli...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
CEDAR (Counter Example Driven Antichain Refinement) is a new symbolic algorithm for computing weakest strategies for safety games of imperfect information. The algorithm computes ...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
The ITPN-PerfBound is a tool for the modeling and analysis of Interval Time Petri Nets (ITPN), that is Petri Nets in which firing time intervals, and possibly firing frequency in...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
We describe the design and implementation of an automatic invariant generator for imperative programs. While automatic invariant generation through constraint solving has been exte...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
We discuss the problem of path feasibility for programs manipulating strings using a collection of standard string library functions. We prove results on the complexity of this pro...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis...