Title
Executable rewriting logic semantics of Orc and formal analysis of Orc programs.
Abstract
The Orc calculus is a simple, yet powerful theory of concurrent computations with great versatility and practical applicability to a very wide range of applications, as it has been amply demonstrated by the Orc language, which extends the Orc calculus with powerful programming constructs that can be desugared into the underlying formal calculus. This means that for: (i) theoretical, (ii) program verification, and (iii) language implementation reasons, the formal semantics of Orc is of great importance. Furthermore, having a semantics of Orc that is executable is essential to provide: (i) a formally-defined interpreter against which language implementations can be validated, and (ii) a (semi-)automatic way of generating a wide range of semantics-based program verification tools, including model checkers and theorem provers.
Year
DOI
Venue
2015
10.1016/j.jlamp.2015.03.003
Journal of Logical and Algebraic Methods in Programming
Keywords
Field
DocType
Rewriting logic,Orc,Executable semantics,Maude,Formal analysis,Service orchestration
Operational semantics,Model checking,Programming language,Computer science,Correctness,Theoretical computer science,Rewriting,Bisimulation,Semantics,Formal verification,Executable
Journal
Volume
Issue
ISSN
84
4
2352-2208
Citations 
PageRank 
References 
1
0.36
59
Authors
2
Name
Order
Citations
PageRank
Musab AlTurki11049.80
José Meseguer29533805.39