Dissertation

Symbolic Reachability Analysis for Rewrite Theories.

Camilo Rocha, Ph.D. Dissertation. Urbana, October, 2012.
    
Related downloads:

Journals

Rewriting Modulo SMT and Open System Analysis.

Camilo Rocha, José Meseguer, and César Muñoz. Journal of Logical and Algebraic Methods in Programming (JLAMP), 86(1), January 2017.
    https://docs.google.com/document/d/1zfkHl8Ys5kbCQT0VTdGawk7Ou9yDM2dQGuUe5qrB108/edit?usp=sharing

Double-spend Attack Models with Time Advantage for Bitcoin.

Carlos Pinzón and Camilo Rocha. Electronic Notes in Theoretical Computer Science (ENTCS), 329C, December 2016.
http://www.sciencedirect.com/science/article/pii/S157106611630113X    https://docs.google.com/document/d/1tyjHedvlkAKbfYukpGLjo0CYb4hUaO7UqaDLFt6R4Wo/edit?usp=sharing

Order-sorted Equality Enrichments Modulo Axioms.

Raúl Gutiérrez, José Meseguer, and Camilo Rocha. Science of Computer Programming (SCP), 99(1), March 2015.
    

Synchronous Set Relations in Rewriting Logic.

Camilo Rocha and César Muñoz. Science of Computer Programming (SCP), 92(B), October 2014.
    

Automatic Proof-Search Heuristics in the Maude Invariant Analyzer Tool.

Camilo Rocha. Revista Colombiana de Computación (RCC), 14(2), December 2013.

   

A Formal Library of Set Relations and its Application to Synchronous Languages.

Camilo Rocha, César Muñoz, and Gilles Dowek. Theoretical Computer Science (TCS), 412(37), August 2011.
    

A Rewriting Decision Procedure for Dijkstra-Scholten’s Syllogistic Logic with Complements.

Camilo Rocha and José Meseguer. Revista Colombiana de Computación (RCC), 8(2), December 2007.
    

Conferences and Workshops (Refereed)

Double-spend Attack Models with Time Advantage for Bitcoin.

Carlos Pinzón and Camilo Rocha. Latin American Symposium on Theory of Computation (in Latin American Informatics Conference) (CLEI XLII). Valparaíso, September 2016.
http://www.sciencedirect.com/science/article/pii/S157106611630113X  https://drive.google.com/file/d/0B-Bk1ixpbgwJTldJZEhTMHBDc3M/view?usp=sharing  https://docs.google.com/document/d/1tyjHedvlkAKbfYukpGLjo0CYb4hUaO7UqaDLFt6R4Wo/edit?usp=sharing  https://drive.google.com/file/d/0B-Bk1ixpbgwJVXhkU0ZKU1NHZm8/view?usp=sharing

Library Management for PVS.

Miguel Romero and Camilo Rocha. Computing Colombian Conference (11CCC). Popayán, September 2016.
https://drive.google.com/file/d/0B-Bk1ixpbgwJUU5QWWR4NmJIZFk/view?usp=sharing  https://drive.google.com/file/d/0B-Bk1ixpbgwJY2t4WkJIeVRRV2M/view?usp=sharing  http://migueleci.github.io/pvslm/  https://drive.google.com/file/d/0B-Bk1ixpbgwJNlRFNDV2OU1uRzA/view?usp=sharing

Formal Verification of Safety Properties for a Cache Coherence Protocol.

Sergio Ramírez and Camilo Rocha. Computing Colombian Conference (10CCC). Bogotá, September 2015.
http://dx.doi.org/10.1109/ColumbianCC.2015.7333399     

Executable Calculational Specifications.

Francisco Cháves and Camilo Rocha. Computing Colombian Conference (10CCC). Bogotá, September 2015.
http://dx.doi.org/10.1109/ColumbianCC.2015.7333398    https://docs.google.com/document/d/1OzT09aeq_g8rqVfF97Q0jpEEx4BJlvaH1Qdddm2XRvI/edit?usp=sharing   

The Formal System of Dijkstra and Scholten.

Camilo Rocha. Logic, Rewriting, and Concurrency; Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday (LRC2015). Urbana, September 2015.
http://link.springer.com/chapter/10.1007%2F978-3-642-54624-2_30    https://docs.google.com/a/camilorocha.info/document/d/1BmVu7U-BWC7Yna70xopGF3Kz8rnC9sWTLnQHU6uLxYs/edit?usp=sharing  https://drive.google.com/file/d/0B-Bk1ixpbgwJc0dXZ3FtbTZPbXc/view?usp=sharing

Mechanical Analysis of Reliable Communication Using the Maude Invariant Analyzer Tool in the Alternating Bit Protocol.

Camilo Rocha and José Meseguer. Specification, Algebra, and Software; A Festschrift Symposium in Honor of Kokichi Futatsugi (SAS2014). Kanazawa, April 2014.
http://link.springer.com/chapter/10.1007%2F978-3-642-54624-2_30    https://docs.google.com/a/camilorocha.info/document/d/1BmVu7U-BWC7Yna70xopGF3Kz8rnC9sWTLnQHU6uLxYs/edit?usp=sharing    https://drive.google.com/a/camilorocha.info/file/d/0B-Bk1ixpbgwJRmNMbGtNR1VhaEE/edit?usp=sharing

Rewriting Modulo SMT and Open System Analysis.

Camilo Rocha, José Meseguer, and César Muñoz. 10th International Workshop on Rewriting Techniques and Applications (WRLA2014). Grennoble, April 2014.
    https://docs.google.com/a/camilorocha.info/document/d/1BmVu7U-BWC7Yna70xopGF3Kz8rnC9sWTLnQHU6uLxYs/edit?usp=sharing    https://drive.google.com/a/camilorocha.info/file/d/0B-Bk1ixpbgwJRmNMbGtNR1VhaEE/edit?usp=sharing

Automatic Proof-Search Heuristics in the Maude Invariant Analyzer Tool.

Camilo Rocha. Computing Colombian Conference (8CCC). Armenia, August 2013.
       

A Formal Interactive Verification Environment for the Plan Execution Interchange Language.

Camilo Rocha, Héctor Cadavid, César Muñoz, and Radu Siminiceanu. 9th International Conference on Integrated Formal Methods (iFM2012). Pisa, June 2012.
      

Order-Sorted Equality Enrichments Modulo Axioms.

Raúl Gutiérrez, José Meseguer, and Camilo Rocha. 9th International Workshop on Rewriting Logic and its Applications (WRLA12). Tallinn, March 2012.

        

Towards a Maude Formal Environment.

Francisco Durán, Camilo Rocha, and José M. Álvarez. Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday (FCT). Menlo Park, November 2011.

        

Simulation and Verification of Synchronous Set Relations in Rewriting Logic.

Camilo Rocha and César Muñoz. 14th Brazilian Symposium on Formal Methods (SBMF2011). São Paulo, September 2011.
      http://camilorocha.info/software  

Proving Safety Properties of Rewrite Theories.

Camilo Rocha and José Meseguer. 4th Conference on Algebra and Coalgebra in Computer Science (CALCO2011). Winchester, August 2011.
        

Tool Interoperability in the Maude Formal Environment.

Francisco Durán, Camilo Rocha, and José M. Álvarez. 4th Conference on Algebra and Coalgebra in Computer Science (CALCO-Tools2011). Winchester, August 2011.
        

Constructors, Sufficient Completeness and Deadlock Freedom of Rewrite Theories.

Camilo Rocha and José Meseguer. 17th International Conference on Logic Programming, Artificial Intelligence and Reasoning (LPAR17). Yogyakarta, October 2010.
        

Rewriting Logic Semantics of a Plan Execution Language.

Gilles Dowek, César Muñoz and Camilo Rocha. 6th Workshop on Structural Operational Semantics (SOS09). Bologna, August 2009.
        

A Graphical Environment for the Semantic Validation of a Plan Execution Language.

Camilo Rocha, César Muñoz and Héctor Cadavid. 3rd International Conference on Space Mission Challenges for Information Technology (SMC-IT). Pasadena, July 2009.
      

Theorem Proving Based on Boolean Equational Procedures.

Camilo Rocha and José Meseguer. 10th International Conference on Relational Methods in Computer Science/Fifth International Conference on Applications of Kleene Algebra (RelMiCS10/AKA5). Frauenwörth, April 2008.
    

Assisted Calculational Proofs and Proof Checking Based on Partial Orders.

Jaime Bohórquez and Camilo Rocha. Formal Methods in Computer Science Education 2008 (FORMED). Budapest, March 2008.

A Rewriting Decision Procedure for Dijkstra-Scholten’s Syllogistic Logic with Complements.

Camilo Rocha and José Meseguer. 2do Congreso Colombiano de Computación (2CCC). Bogotá, April 2007.
    

Una Semántica de Ensamblaje y Composición de Servicios y Componentes.

Camilo Rocha, Rafael García and Rubby Casallas. 9a Conferencia Iberoamericana de Software Engineering (CIbSE 2006) La Plata, April 2006.
    

Towards the Effective Use of Formal Logic in the Teaching of Discrete Mathematics.

Jaime Bohórquez and Camilo Rocha. Sixth International Conference on Information Technology Based Higher Education and Training (ITHET). Santo Domingo, July 2005.
    

Technical Reports

Double-spend Attack Models with Time Advantage for Bitcoin.

Carlos Pinzón and Camilo Rocha. Technical Report, Escuela Colombiana de Ingeniería 001/484. Bogotá, December 2016.
  https://drive.google.com/file/d/0B-Bk1ixpbgwJUU5QWWR4NmJIZFk/view?usp=sharing  https://drive.google.com/file/d/0B-Bk1ixpbgwJY2t4WkJIeVRRV2M/view?usp=sharing

Library Management for PVS.

Miguel Romero and Camilo Rocha. Technical Report, Escuela Colombiana de Ingeniería 001/464. Bogotá, October 2016.
  https://drive.google.com/file/d/0B-Bk1ixpbgwJUU5QWWR4NmJIZFk/view?usp=sharing  https://drive.google.com/file/d/0B-Bk1ixpbgwJY2t4WkJIeVRRV2M/view?usp=sharing  http://migueleci.github.io/pvslm/

Rewriting Modulo SMT and Open System Analysis.

Camilo Rocha, José Meseguer, and César Muñoz. Technical Report, University of Illinois at Urbana-Champaign. Urbana, October 2016.
    

Executable Calculational Expressions.

Francisco Cháves and Camilo Rocha. Technical Report, Escuela Colombiana de Ingeniería 001/301. Bogotá, August 2015.
     

Rewriting Modulo SMT.

Camilo Rocha, José Meseguer, and César Muñoz. Technical Memorandum, NASA TM-2013-218033. Langley, August 2013.
    

Order-sorted Equality Enrichments Modulo Axioms.

Raúl Gutiérrez, José Meseguer, and Camilo Rocha. Technical Report, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, December 2011.
    

Proving Safety Properties of Rewrite Theories.

Camilo Rocha and José Meseguer. Technical Report, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, November 2010.
      

Constructors, Sufficient Completeness and Deadlock Freedom of Generalized Rewrite Theories.

Camilo Rocha and José Meseguer. Technical Report, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, May 2010.
      

Rewriting Logic Semantics of a Plan Execution Language.

Gilles Dowek, César Muñoz and Camilo Rocha. Technical Memorandum, NASA TM-2009-215770. Langley, June 2009.
      

Theorem Proving Modulo Based on Boolean Procedures.

Camilo Rocha and José Meseguer. Technical Report TR-2007-2922, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, December 2007.
    

A Rewriting Decision Procedure for Dijkstra-Scholten’s Syllogistic Logic with Complements.

Camilo Rocha and José Meseguer. Technical Report TR-2007-2921, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, December 2007.
    

Five Isomorphic Boolean Theories and Four Decision Procedures.

Camilo Rocha and José Meseguer. Technical Report TR-2007-2818, Department of Computer Science in the University of Illinois at Urbana-Champaign. Urbana, March 2007.