
   
PUBLICATIONS
The following scientific publications have resulted from the project
work so far.
Books and Edited Volumes
 Luca Aceto and Lars
Birkedal. Special
Issue: Selected papers of the conference on ``Foundations of
Software Science and Computation Structures'': FOSSACS 2012,
Tallinn, Estonia, 2012. Logical Methods in Computer Science,
2013.
 Luca Aceto, Monika Henzinger and Jiri Sgall. Proceedings of
the 38th International Colloquium on Automata, Languages and
Programming (ICALP 2011), Lecture Notes in Computer Science 6755
and 6756, SpringerVerlag, 2011. Part I may be found
here, and part
II here.
 Luca Aceto, Monika Henzinger and Jiri Sgall.
38th
International Colloquium on Automata, Languages and Programming (ICALP
2011), Information and Computation 222, pages 1306, January
2013.

Luca Aceto and MohammadReza
Mousavi. Proceedings
of the First International Workshop on Process Algebra and
Coordination (PACO 2011), volume 60 of Electronic Proceedings in
Theoretical Computer Science, 6 August 2011.
 Luca Aceto and Pawel Sobocinski. Proceedings of the Seventh
Workshop on Structural Operational Semantics, volume 32 of
Electronic Proceedings in Theoretical Computer Science, 11th August
2010.
PhD Theses
 Georgiana Caltais. Coalgebraic
Tools for Bisimilarity and Decorated Trace Semantics. PhD
thesis in Computer Science, Reykjavik University and Radboud
University Nijmegen. Date of defence: 16 December 2013.
 Matteo
Cimini. Contributions to the
Metatheory of Structural Operational Semantics. PhD thesis in
Computer Science, Reykjavik University. Date of defence: 18 November
2011.

EugenIoan Goriac. Axiomatizations from Structural Operational Semantics: Theory and Tools. PhD thesis in Computer Science, Reykjavik
University. Date of defence: 22 August 2013.
MSc Theses
 Oddur Óskar Kjartansson. On the Formal Semantics of Bluespec
System Verilog. MSc thesis in Computer Science, Reykjavik
University. Date of defence: 29 August 2012.
Chapters in Books and Collections

Luca Aceto, Anna
Ingolfsdottir and Jiri Srba.
The Algorithmics of Bisimilarity.
Chapter 3 of
Advanced Topics in Bisimulation and Coinduction (Jan Rutten
and Davide Sangiorgi editors), volume 52 of Cambridge Tracts in
Theoretical Computer Science, pp. 100172, Cambridge University Press.
Journal Papers

Luca Aceto, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and
Michel Reniers.
Rule Formats for Determinism and Idempotence.
Journal
version to appear in a Special Issue of Science of
Computer Programming devoted to FSEN 2009 (Farhad Arbab
and Marjan Sirjani guest editors). Version dated 31
March 2010. The official journal version is
here.

Luca Aceto,
Taolue Chen, Anna
Ingolfsdottir, Bas
Luttik and Jaco
van de
Pol.
On the Axiomatizability of Priority II. Theoretical
Computer Science 412(28):30353044, 2011. The official journal paper
is here.
 Luca Aceto, Matteo Cimini and Anna Ingolfsdottir.
Proving
the validity of equations in GSOS languages using rulematching
bisimilarity. Version dated 18 October 2010. Mathematical
Structures in Computer Science 22(2):291331, Cambridge
University Press, 2012.

Luca Aceto,
Matteo Cimini, Anna
Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers.
SOS Rule Formats for Zero and Unit
Elements. Theoretical
Computer Science 412(28):30453071, 2011. The official journal
paper
is here.

Luca Aceto,
Matteo Cimini, Anna
Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers.
Rule Formats for Distributivity. Theoretical
Computer Science, Elsevier. To appear.
 Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Ali Jafari, Arni
Hermann Reynisson, Steinar Hugi Sigurdarson and Marjan
Sirjani. Modelling
and Simulation of RealTime Systems using Timed
Rebeca. Science of Computer Programming, Elsevier. To
appear.

Luca Aceto, David de Frutos Escrig, Carlos GregorioRodriguez and Anna
Ingolfsdottir.
Complete
and ready simulation semantics are not finitely based over BCCSP,
even with a singleton
alphabet. Information
Processing Letters 111(9):408413, Elsevier, 2011.

Luca Aceto, David de Frutos Escrig,
Carlos GregorioRodriguez and Anna Ingolfsdottir.
Axiomatizing Weak Simulation
Semantics over BCCSP. To appear in the journal
Theoretical
Computer Science..

Luca Aceto, EugenIoan Goriac and Anna
Ingolfsdottir.
SOS Rule Formats for Idempotent Terms and Idempotent Unary
Operators.. Journal of Logic and Algebraic Programming,
Elsevier, 2013. To appear.
 Bonsangue, M.M., Caltais, G., Goriac, E., Lucanu, D., Rutten,
J.J.M.M. and Silva, A.
Automatic
equivalence proofs for nondeterministic coalgebras. To appear in Science of Computer
Programming. Also available as
CWI
report SEN1113, December 2011.
Conference and Workshop Papers

Luca Aceto, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi.
Decompositional Reasoning about the History of Parallel
Processes.
To appear in the Proceedings of IPM International Conference on
Fundamentals of Software Engineering (FSEN 2011), Tehran, Iran,
April 2022, 2011. Lecture Notes in Computer Science,
SpringerVerlag.

Luca Aceto,
Georgiana Caltais, EugenIoan Goriac and Anna
Ingolfsdotti.
PREG Axiomatizer  A Ground Bisimilarity Checker for GSOS with
Predicates..
Version dated 21 April 2011. Proceedings
of CALCO 2011 as a
contribution
to CALCO
Tools, Lecture Notes in Computer Science 6859, pp. 378385,
Springer Verlag 2011. The associated PREG Axiomatizer tool is
available here. PREG
Axiomatizer is a tool for automatically deriving groundcomplete
axiomatizaitons of the bisimilarity over GSOS systems (extended with
predicates). The official version from Springer is
here.
 Luca Aceto, Georgiana Caltais, EugenIoan Goriac and Anna
Ingolfsdottir.
Axiomatizing GSOS with Predicates. Proceedings of SOS 2011, Electronic
Proceedings in Theoretical Computer Science 62, pp. 115, 2011.
 Luca Aceto, Arnaud Carayol, Zoltan Esik and Anna
Ingolfsdottir. Algebraic
Synchronization Trees and Processes. Proceedings of ICALP 2012,
Lecture Notes in Computer Science, Springer, July 2012. To appear.

Luca Aceto,
Matteo Cimini, Anna
Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers.
On Rule Formats for Zero and Unit Elements. Proceedings of
the TwentySixth
Conference on the Mathematical Foundations of Programming
Semantics, University of Ottawa Thursday May 6  Monday May 10,
2010. Electronic Notes in Theoretical Computer Science 256,
pp. 145160, Elsevier.

Luca Aceto,
Matteo Cimini, Anna
Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers.
Rule Formats for Distributivity. Proceedings of LATA 2011, Lecture Notes in
Computer Science 6638, pp. 8091, Springer Verlag, 2011. The official
version from Springer is
here.
 Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Arni Hermann
Reynisson, Steinar Hugi Sigurdarson and Marjan
Sirjani.
Modelling and Simulation of RealTime Systems using Timed
Rebeca.
Version dated 19 February 2011. Proceedings of FOCLASA
2011, Electronic Proceedings in Theoretical Computer Science 58, pp. 119,
2011.
 Luca Aceto, David de Frutos Escrig,
Carlos GregorioRodriguez and Anna Ingolfsdottir.
Axiomatizing Weak Ready Simulation Semantics over BCCSP. Version dated 3 June 2011.
Proceedings of the
8th International
Colloquium on Theoretical Aspects of Computing, ICTAC 2011,
Lecture Notes in Computer Science 6919, pp. 724, SpringerVerlag, 2011.

Luca Aceto, David de Frutos Escrig,
Carlos GregorioRodriguez and Anna Ingolfsdottir.
The
Equational Theory of Weak Complete Simulation Semantics over
BCCSP.
Version dated 26 June 2011.
To appear in the Proceedings of the
38th International Conference on Current
Trends in Theory and Practice of Computer Science (SOFSEM 2012)
(M. Bieliková et al. (Eds.)), Lecture Notes in Computer Science
7147, pages 141152, SpringerVerlag, 2012.

Luca Aceto, EugenIoan Goriac and Anna
Ingolfsdottir.
SOS Rule Formats for Idempotent Terms and Idempotent Unary
Operators.. Proceedings of
SOFSEM 2013: The 39th
International Conference on Current Trends in Theory and Practice of
Computing, Lecture Notes in Computer Science 7741, pp. 108120,
SpringerVerlag, 2013.
 Luca Aceto,
EugenIoan Goriac and Anna
Ingolfsdottir.
Meta SOS  A Maude Based SOS MetaTheory
Framework. Proceeedings of EXPRESS/SOS 2013, Electronic
Proceedings in Theoretical Computer Science, 2013.
 Luca Aceto, EugenIoan Goriac, Anna Ingolfsdottir, MohammadReza
Mousavi and Michel
Reniers. Exploiting
Algebraic Laws to Improve Mechanized Axiomatizations. To
appear in the Proceedings of the 5th
Conference on Algebra and Coalgebra in Computer Science, Warsaw,
Poland, 36 September 2013. SpringerVerlag, 2013.
 Luca Aceto, Anna Ingolfsdottir, MohammadReza Mousavi and
Michel Reniers.
A Rule Format for Unit Elements. Proceedings of SOFSEM 2010:
The 36th International Conference on Current Trends in Theory
and Practice of Computing, Lecture Notes in Computer
Science 5901, pp. 141152, SpringerVerlag, 2010.
 Filippo Bonchi, Marcello Bonsangue, Georgiana Caltais, Jan Rutten
and Alexandra Silva. Final semantics for decorated traces. To
appear in the Proceedings of the
Twentyeighth
Conference on the Mathematical Foundations of Programming
Semantics, Electronic Notes in Theoretical Computer Science,
Elsevier, 2012.
 Marcello Bonsangue, Georgiana Caltais, EugenIoan Goriac, Dorel
Lucanu, Jan Rutten and Alexandra Silva. A
decision procedure for bisimilarity of generalized
regular expressions. Proceedings
of the 13th Brazilian Symposium on Formal Methods
(SBMF'2010), Lecture Notes in Computer Science 6527, pp. 226241, Springer 2011.
 Matteo Cimini, MohammadReza Mousavi, Michel Reniers and Murdoch
Gabbay. Nominal SOS. To appear in the Proceedings of the
Twentyeighth
Conference on the Mathematical Foundations of Programming
Semantics, Electronic Notes in Theoretical Computer Science,
Elsevier, 2012.

Daniel Gebler, EugenIoan Goriac and Mohammad Reza
Mousavi. Algebraic
MetaTheory of Processes with Data. Proceedings of EXPRESS/SOS
2013, volume 120 of Electronic Proceedings in Theoretical Computer
Science, pp. 6377, 2013

E. I. Goriac, D. Lucanu,
G. Roşu. Automating
Coinduction with Case Analysis. Proceedings of ICFEM 2010,
Lecture Notes in Computer Science 6447, pp. 220236, SpringerVerlag.
Unpublished and Submitted Papers
 Luca Aceto,
EugenIoan Goriac and Anna
Ingolfsdottir.
A GroundComplete Axiomatization of Stateless Bisimilarity over
Linda.
Version dated 21 June 2013. Submitted for
publication.
 Filippo Bonchi, Marcello Bonsangue, Georgiana Caltais, Jan Rutten
and Alexandra Silva. Final semantics
for decorated traces, October 2012. Submitted for journal
publication.
Software
 Luca Aceto, Georgiana Caltais, EugenIoan Goriac and Anna
Ingolfsdotti. PREG
Axiomatizer. PREG Axiomatizer is a tool for automatically
deriving groundcomplete axiomatizaitons of the bisimilarity over
GSOS systems (extended with predicates).
 Luca Aceto, Matteo Cimini, Anna Ingolfsdotti, Arni Hermann Reynisson,
Steinar Hugi Sigurdarson and Marjan Sirjani.
Translator
from Timed Rebeca to Erlang.
 Luca Aceto,
EugenIoan Goriac and Anna
Ingolfsdottir.
Meta SOS  A Maude Based SOS MetaTheory
Framework.
