Abstract. Up to now, research on speed-up techniques for DIJKSTRA’s algorithm focused on single-criteria scenarios. The goal was to find the quickest route within a transportati...
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...
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...
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...
Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yin...
CEDAR (Counter Example Driven Antichain Refinement) is a new symbolic algorithm for computing weakest strategies for safety games of imperfect information. The algorithm computes ...
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...
Elina Pacini Naumovich, Simona Bernardi, Marco Gri...
We describe the design and implementation of an automatic invariant generator for imperative programs. While automatic invariant generation through constraint solving has been exte...
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...
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...