SAS
2004
Springer
14 years 5 months ago
2004
Springer
hedron Abstract Domain Robert Claris´o and Jordi Cortadella Universitat Polit`ecnica de Catalunya Barcelona, Spain Abstract. An interesting area in static analysis is the study of...
SAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We specify an information flow analysis for a simple imperative language, using a Hoare-like logic. The logic facilitates static checking of a larger class of programs t...
SAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. In this paper we investigate the existence of a deductive veri cation method based on a logic that describes pointer aliasing. The main idea of such a method is that the ...
ITRUST
2004
Springer
14 years 5 months ago
2004
Springer
Security and trust are two properties of modern computing systems that are the focus of much recent interest. They play an increasingly significant role in the requirements for mo...
ESORICS
2004
Springer
14 years 5 months ago
2004
Springer
The use of formal methods to verify security protocols with respect to secrecy and authentication has become standard practice. In contrast, the formalization of other security goa...
CAV
2004
Springer
14 years 5 months ago
2004
Springer
—We introduce a new BDD-like data structure called Hybrid-Restriction Diagrams (HRDs) for the representation and manipulation of linear hybrid automata (LHA) state-spaces and pre...
CAV
2004
Springer
14 years 5 months ago
2004
Springer
We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is...
CAV
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. Separation Logic consists of a Boolean combination of predicates of the form vi ≥ vj +c where c is a constant and vi, vj are variables of some ordered infinite type li...
CAV
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numeri...
CAV
2004
Springer
14 years 5 months ago
2004
Springer
Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary ...