-
Article
Open AccessCausal analysis of positive Reaction Systems
Cause/effect analysis of complex systems is instrumental in better understanding many natural phenomena. Moreover, formal analysis requires the availability of suitable abstract computational models that someh...
-
Chapter and Conference Paper
Exploiting Adjoints in Property Directed Reachability Analysis
We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-...
-
Chapter and Conference Paper
First-Order Dynamic Logic for Compensable Processes
Compensable programs offer a convenient paradigm to deal with long-running transactions, because they offer a structured and modular approach to the composition of distributed transactional activities, like se...
-
Chapter and Conference Paper
Sessions and Pipelines for Structured Service Programming
Service-oriented computing is calling for novel computational models and languages with primitives for client-server interaction, orchestration and unexpected events handling. We present CaSPiS, a process calculu...
-
Chapter and Conference Paper
Executable Tile Specifications for Process Calculi
Tile logic extends rewriting logic by taking into account side-effects and rewriting synchronization. These aspects are very important when we model process calculi, because they allow us to expr...