Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by Alexandra Silva

2017

Learning nominal automata

Authors
Moerman, Joshua; Sammartino, Matteo; Silva, Alexandra; Klin, Bartek; Szynwelski, Michal;

Publication
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017

Abstract

2013

On Moessner's Theorem

Authors
Kozen, D; Silva, A;

Publication
The American Mathematical Monthly

Abstract

2015

IMCReo: interactive Markov chains for Stochastic Reo

Authors
Oliveira, Nuno; Silva, Alexandra; Barbosa, LuisSoares;

Publication
J. Internet Serv. Inf. Secur.

Abstract

2016

Coalgebraic Learning

Authors
Silva, A;

Publication
25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France

Abstract

2013

Sound and Complete Axiomatizations of Coalgebraic Language Equivalence

Authors
Bonsangue, MM; Milius, S; Silva, A;

Publication
ACM Trans. Comput. Log.

Abstract

2013

Automatic equivalence proofs for non-deterministic coalgebras

Authors
Bonsangue, M; Caltais, G; Goriac, EI; Lucanu, D; Rutten, J; Silva, A;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analog of Kleene's theorem and Kleene algebra, were recently proposed by a subset of the authors of this paper. Examples of the systems covered include infinite streams, deterministic automata, Mealy machines and labeled transition systems. In this paper, we present a novel algorithm to decide whether two expressions are bisimilar or not. The procedure is implemented in the automatic theorem prover CIRC, by reducing coinduction to an entailment relation between an algebraic specification and an appropriate set of equations. We illustrate the generality of the tool with three examples: infinite streams of real numbers, Mealy machines and labeled transition systems.

  • 2
  • 13