SPIN
2009
Springer
14 years 2 months ago
2009
Springer
This paper introduces a new model checking algorithm that searches for non-progress cycles, used mainly to check for livelocks. The algorithm performs an incremental depth-first s...
SPIN
2009
Springer
14 years 2 months ago
2009
Springer
This paper describes a set of software tools developed for teaching concurrency and model checking. jSpin is an elementary development environment for Spin that formats and filter...
SPIN
2009
Springer
14 years 2 months ago
2009
Springer
SPIN
2009
Springer
14 years 2 months ago
2009
Springer
Abstract. Symbolic reachability analysis provides a basis for the verification of software systems by offering algorithmic support for the exploration of the program state space ...
SPIN
2009
Springer
14 years 2 months ago
2009
Springer
RTA
2009
Springer
14 years 2 months ago
2009
Springer
Abstract. The automated analysis of termination of term rewriting systems (TRSs) has drawn a lot of attention in the scientific community during the last decades and many differe...
RTA
2009
Springer
14 years 2 months ago
2009
Springer
Abstract. We consider the problem of deciding the security of cryptographic protocols for a bounded number of sessions, taking into account some algebraic properties of the securit...
RTA
2009
Springer
14 years 2 months ago
2009
Springer
It is known that the first-order theory with a single predicate → that denotes one-step rewriting reduction on terms is undecidable already for formulae with ∃∀ prefix. Sev...
RTA
2009
Springer
14 years 2 months ago
2009
Springer
We address the problem of cyclic termgraph rewriting. We propose a new framework where rewrite rules are tuples of the form (L, R, τ, σ) such that L and R are termgraphs represen...
RTA
2009
Springer
14 years 2 months ago
2009
Springer
Abstract. Interaction nets are a graphical formalism inspired by Linear Logic proof-nets often used for studying higher order rewriting e.g. β-reduction. Traditional presentations...