Publications
“Semantics for Interactive Sequential Systems and Non-Interference Properties”, CLEI Electron. J., vol. 14, no. 3, 2011.
paper-8.pdf (231.62 KB)
, 
“Unprovability of the logical characterization of bisimulation”, Information and Computation, vol. 209, pp. 1048-1056, 2011.
, “Assume-guarantee Reasoning with ioco Testing Relation”, in Proceedings of the 22nd IFIP International Conference on Testing Software and Systems: Short Papers, 2010, pp. 103-107.
paper-182.pdf (562.12 KB)
, 
“Automatic Probabilistic Program Verification through Random Variable Abstraction”, in Proceedings Eighth Workshop on Quantitative Aspects of Programming Languages, QAPL 2010, 2010, vol. EPTCS 28, pp. 34-47.
paper-24.pdf (404.61 KB)
, 
“On the automatic verification of Distributed Probabilistic Automata with Partial Information”, Universidad Nacional de Córdoba, Córdoba, 2010.
paper-176.pdf (1.79 MB)
, 
“Describing Secure Interfaces with Interface Automata”, Electr. Notes Theor. Comput. Sci., vol. 264, no. 1, pp. 107-123, 2010.
paper-12.pdf (474.34 KB)
, 
“A Refinement Based Notion of Non-interference for Interface Automata: Compositionality, Decidability and Synthesis”, in SCCC 2010, Proceedings of the XXIX International Conference of the Chilean Computer Science Society, 2010, pp. 280-289.
paper-10.pdf (320.38 KB)
, 
“Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains”, in Model Checking Software - 17th International SPIN Workshop, 2010, vol. LNCS 6349, pp. 193-211.
paper-11.pdf (315.45 KB)
, 
“Cryptographic Protocol Synthesis and Verification for Multiparty Sessions”, in Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009, 2009, pp. 124-140.
paper-188.pdf (512.93 KB)
, 
“On the Expressive Power of Schedulers in Distributed Probabilistic Systems”, Electr. Notes Theor. Comput. Sci., vol. 253, no. 3, pp. 45-71, 2009.
paper-18.pdf (525.34 KB)
, 
“Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization”, in QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, 2009, pp. 11-20.
paper-16.pdf (525.46 KB)
, 
“Optimizing Probabilities of Real-Time Test Case Execution”, in ICST 2009, Second International Conference on Software Testing Verification and Validation, 2009, pp. 446-455.
, “Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers”, in CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009, vol. LNCS 5710, pp. 338-353.
paper-14.pdf (469.3 KB)
, 
“Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications”, QFM, vol. 13. 2009.
, “Secure Enforcement for Global Process Specifications”, in CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, 2009, pp. 511-526.
, “Undecidability Results for Distributed Probabilistic Systems”, in Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, 2009, vol. LNCS 5902, pp. 220-235.
, “Varieties with Definable Factor Congruences”, Trans. Amer. Math. Soc., vol. 361, pp. 5061–5088, 2009.
, “On the verification of probabilistic I/O automata with unspecified rates”, in Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009, pp. 582-586.
paper-17.pdf (312.21 KB)
, 
Calculo de programas. Córdoba: Universidad Nacional de Cordoba, 2008.
, “Directly Indecomposables in Semidegenerate Varieties of Connected po-Groupoids”, Order, vol. 25, pp. 377-386, 2008.
, “Significant Diagnostic Counterexamples in Probabilistic Model Checking”, in Hardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008, 2008, vol. LNCS 5394, pp. 129-148.
paper-19.pdf (363.58 KB)
, 
“Automatic Refinement of Split Binary Semaphore”, in Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings, 2007, vol. 4711, pp. 64-78.
, “Quantitative Model Checking Revisited: Neither Decidable Nor Approximable”, in Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, 2007, vol. LNCS 4763, pp. 179-194.
paper-20.pdf (414.71 KB)
, 
“Verification of clock synchronization algorithms: experiments on a combination of deductive tools”, Formal Asp. Comput., vol. 19, pp. 321-341, 2007.
, “A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes”, in Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, 2006, vol. LNCS 4202, pp. 352-367.
,