RELEASE: Publications

GreenHub farmer: real-world data for Android energy mining.

2019

Matalonga, Hugo and Cabral, Bruno and Castor, Fernando and Couto, Marco and Pereira, Rui and de Sousa, Simão Melo and Fernandes, João Paulo.
Proceedings of the 16th International Conference on Mining Software Repositories, MSR 2019, 26-27 May 2019, Montreal, Canada. Pages 171-175.
DOI: 10.1109/MSR.2019.00034

@inproceedings{conf/msr/MatalongaCC0PSF19,
  author = {Matalonga, Hugo and Cabral, Bruno and Castor, Fernando and Couto, Marco and Pereira, Rui and de Sousa, Simão Melo and Fernandes, João Paulo},
  editor = {Storey, Margaret{-}Anne D. and Adams, Bram and Haiduc, Sonia},
  title = {GreenHub farmer: real-world data for Android energy mining},
  booktitle = {Proceedings of the 16th International Conference on Mining Software
        Repositories, {MSR} 2019, 26-27 May 2019, Montreal, Canada.},
  pages = {171-175},
  publisher = {IEEE / ACM},
  year = {2019},
  url = {https://doi.org/10.1109/MSR.2019.00034},
  doi = {10.1109/MSR.2019.00034},
  pdf = {http://greenlab.di.uminho.pt/wp-content/uploads/2019/04/GreenHubFarmerFinal.pdf}
}

Revisiting concurrent separation logic.

2017

Soares, Pedro and Ravara, António and de Sousa, Simão Melo.
J. Log. Algebr. Meth. Program. 89. Pages 41-66.
DOI: 10.1016/j.jlamp.2017.02.004

@article{journals/jlp/SoaresRS17,
  author = {Soares, Pedro and Ravara, António and de Sousa, Simão Melo},
  title = {Revisiting concurrent separation logic},
  journal = {J. Log. Algebr. Meth. Program.},
  volume = {89},
  pages = {41-66},
  year = {2017},
  url = {https://doi.org/10.1016/j.jlamp.2017.02.004},
  doi = {10.1016/j.jlamp.2017.02.004}
}

Deciding Kleene algebra terms equivalence in Coq.

2015

Moreira, Nelma and Pereira, David and de Sousa, Simão Melo.
J. Log. Algebr. Meth. Program. 84(3). Pages 377-401.
DOI: 10.1016/j.jlamp.2014.12.004

@article{journals/jlp/MoreiraPS15,
  author = {Moreira, Nelma and Pereira, David and de Sousa, Simão Melo},
  title = {Deciding Kleene algebra terms equivalence in Coq},
  journal = {J. Log. Algebr. Meth. Program.},
  volume = {84},
  number = {3},
  pages = {377-401},
  year = {2015},
  url = {https://doi.org/10.1016/j.jlamp.2014.12.004},
  doi = {10.1016/j.jlamp.2014.12.004}
}

Certifying execution time in multicores.

2015

Rodrigues, Vitor and Akesson, Benny and Florido, Mário and de Sousa, Simão Melo and Pedroso, João Pedro and Vasconcelos, Pedro B..
Sci. Comput. Program. 111. Pages 505-534.
DOI: 10.1016/j.scico.2015.06.006

@article{journals/scp/RodriguesAFSPV15,
  author = {Rodrigues, Vitor and Akesson, Benny and Florido, Mário and de Sousa, Simão Melo and Pedroso, João Pedro and Vasconcelos, Pedro B.},
  title = {Certifying execution time in multicores},
  journal = {Sci. Comput. Program.},
  volume = {111},
  pages = {505-534},
  year = {2015},
  url = {https://doi.org/10.1016/j.scico.2015.06.006},
  doi = {10.1016/j.scico.2015.06.006}
}

Revisiting Concurrent Separation Logic and Operational Semantics.

2015

Soares, Pedro and Ravara, António and de Sousa, Simão Melo.
23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015, Turku, Finland, March 4-6, 2015 Pages 484-491.
DOI: 10.1109/PDP.2015.85

@inproceedings{conf/pdp/SoaresRS15,
  author = {Soares, Pedro and Ravara, António and de Sousa, Simão Melo},
  editor = {Daneshtalab, Masoud and Aldinucci, Marco and Lepp{\"{a}}nen, Ville and Lilius, Johan and Brorsson, Mats},
  title = {Revisiting Concurrent Separation Logic and Operational Semantics},
  booktitle = {23rd Euromicro International Conference on Parallel, Distributed,
      and Network-Based Processing, {PDP} 2015, Turku, Finland, March 4-6,
      2015},
  pages = {484-491},
  publisher = {IEEE Computer Society},
  year = {2015},
  url = {https://doi.org/10.1109/PDP.2015.85},
  doi = {10.1109/PDP.2015.85}
}

Complexity checking of ARM programs, by deduction.

2014

Pereira, Mário and de Sousa, Simão Melo.
Symposium on Applied Computing, SAC 2014, Gyeongju, Republic of Korea - March 24 - 28, 2014 Pages 1309-1314.
DOI: 10.1145/2554850.2555012

@inproceedings{conf/sac/PereiraS14,
  author = {Pereira, Mário and de Sousa, Simão Melo},
  editor = {Cho, Yookun and Shin, Sung Y. and Kim, Sang{-}Wook and Hung, Chih{-}Cheng and Hong, Jiman},
  title = {Complexity checking of {ARM} programs, by deduction},
  booktitle = {Symposium on Applied Computing, {SAC} 2014, Gyeongju, Republic of
        Korea - March 24 - 28, 2014},
  pages = {1309-1314},
  publisher = {ACM},
  year = {2014},
  url = {https://doi.org/10.1145/2554850.2555012},
  doi = {10.1145/2554850.2555012}
}

E-Id Authentication and Uniform Access to Cloud Storage Service Providers.

2013

Gouveia, João and Crocker, Paul Andrew and de Sousa, Simão Melo and Azevedo, Ricardo.
IEEE 5th International Conference on Cloud Computing Technology and Science, CloudCom 2013, Bristol, United Kingdom, December 2-5, 2013, Volume 1 Pages 487-492.
DOI: 10.1109/CloudCom.2013.71

@inproceedings{conf/cloudcom/GouveiaCSA13,
  author = {Gouveia, João and Crocker, Paul Andrew and de Sousa, Simão Melo and Azevedo, Ricardo},
  title = {E-Id Authentication and Uniform Access to Cloud Storage Service Providers},
  booktitle = {IEEE 5th International Conference on Cloud Computing Technology
        and Science, CloudCom 2013, Bristol, United Kingdom, December 2-5,
        2013, Volume 1},
  pages = {487-492},
  publisher = {IEEE Computer Society},
  year = {2013},
  url = {https://doi.org/10.1109/CloudCom.2013.71},
  doi = {10.1109/CloudCom.2013.71}
}

A Declarative Compositional Timing Analysis for Multicores Using the Latency-Rate Abstraction.

2013

Rodrigues, Vitor and Akesson, Benny and de Sousa, Simão Melo and Florido, Mário.
Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings 7752. Pages 43-59.
DOI: 10.1007/978-3-642-45284-0_4

@inproceedings{conf/padl/RodriguesASF13,
  author = {Rodrigues, Vitor and Akesson, Benny and de Sousa, Simão Melo and Florido, Mário},
  editor = {Sagonas, Konstantinos},
  title = {A Declarative Compositional Timing Analysis for Multicores Using the
        Latency-Rate Abstraction},
  booktitle = {Practical Aspects of Declarative Languages - 15th International Symposium,
        {PADL} 2013, Rome, Italy, January 21-22, 2013. Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {7752},
  pages = {43-59},
  publisher = {Springer},
  year = {2013},
  url = {https://doi.org/10.1007/978-3-642-45284-0_4},
  doi = {10.1007/978-3-642-45284-0_4}
}

Deciding Regular Expressions (In-)Equivalence in Coq.

2012

Moreira, Nelma and Pereira, David and de Sousa, Simão Melo.
Relational and Algebraic Methods in Computer Science - 13th International Conference, RAMiCS 2012, Cambridge, UK, September 17-20, 2012. Proceedings 7560. Pages 98-113.
DOI: 10.1007/978-3-642-33314-9_7

@inproceedings{conf/RelMiCS/MoreiraPS12,
  author = {Moreira, Nelma and Pereira, David and de Sousa, Simão Melo},
  editor = {Kahl, Wolfram and Griffin, Timothy G.},
  title = {Deciding Regular Expressions (In-)Equivalence in Coq},
  booktitle = {Relational and Algebraic Methods in Computer Science - 13th International
        Conference, RAMiCS 2012, Cambridge, UK, September 17-20, 2012. Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {7560},
  pages = {98-113},
  publisher = {Springer},
  year = {2012},
  url = {https://doi.org/10.1007/978-3-642-33314-9_7},
  doi = {10.1007/978-3-642-33314-9_7}
}

Learning Stochastic Timed Automata from Sample Executions.

2012

de Matos Pedro, André and Crocker, Paul Andrew and de Sousa, Simão Melo.
Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I 7609. Pages 508-523.
DOI: 10.1007/978-3-642-34026-0_38

@inproceedings{conf/isola/PedroCS12,
  author = {de Matos Pedro, André and Crocker, Paul Andrew and de Sousa, Simão Melo},
  editor = {Margaria, Tiziana and Steffen, Bernhard},
  title = {Learning Stochastic Timed Automata from Sample Executions},
  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.
        Technologies for Mastering Change - 5th International Symposium, ISoLA
        2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings,
        Part {I}},
  series = {Lecture Notes in Computer Science},
  volume = {7609},
  pages = {508-523},
  publisher = {Springer},
  year = {2012},
  url = {https://doi.org/10.1007/978-3-642-34026-0_38},
  doi = {10.1007/978-3-642-34026-0_38}
}

Rigorous Software Development - An Introduction to Program Verification.

2011

Almeida, José Bacelar and Frade, Maria João and Pinto, Jorge Sousa and de Sousa, Simão Melo.

DOI: 10.1007/978-0-85729-018-2
ISBN: 978-0-85729-017-5

@book{series/utcs/AlmeidaFPS11,
  author = {Almeida, José Bacelar and Frade, Maria João and Pinto, Jorge Sousa and de Sousa, Simão Melo},
  title = {Rigorous Software Development - An Introduction to Program Verification},
  series = {Undergraduate Topics in Computer Science},
  publisher = {Springer},
  year = {2011},
  url = {https://doi.org/10.1007/978-0-85729-018-2},
  doi = {10.1007/978-0-85729-018-2},
  isbn = {978-0-85729-017-5}
}

Certifying Execution Time.

2011

Rodrigues, Vitor and Pedroso, João Pedro and Florido, Mário and de Sousa, Simão Melo.
Foundational and Practical Aspects of Resource Analysis - Second International Workshop, FOPARA 2011, Madrid, Spain, May 19, 2011, Revised Selected Papers 7177. Pages 108-125.
DOI: 10.1007/978-3-642-32495-6_7

@inproceedings{conf/fopara/RodriguesPFS11,
  author = {Rodrigues, Vitor and Pedroso, João Pedro and Florido, Mário and de Sousa, Simão Melo},
  editor = {Peña, Ricardo and van Eekelen, Marko C. J. D. and Shkaravska, Olha},
  title = {Certifying Execution Time},
  booktitle = {Foundational and Practical Aspects of Resource Analysis - Second International
        Workshop, {FOPARA} 2011, Madrid, Spain, May 19, 2011, Revised Selected
        Papers},
  series = {Lecture Notes in Computer Science},
  volume = {7177},
  pages = {108-125},
  publisher = {Springer},
  year = {2011},
  url = {https://doi.org/10.1007/978-3-642-32495-6_7},
  doi = {10.1007/978-3-642-32495-6_7}
}

A Functional Approach to Worst-Case Execution Time Analysis.

2011

Rodrigues, Vitor and Florido, Mário and de Sousa, Simão Melo.
Functional and Constraint Logic Programming - 20th International Workshop, WFLP 2011, Odense, Denmark, July 19th, Proceedings 6816. Pages 86-103.
DOI: 10.1007/978-3-642-22531-4_6

@inproceedings{conf/wflp/RodriguesFS11,
  author = {Rodrigues, Vitor and Florido, Mário and de Sousa, Simão Melo},
  editor = {Kuchen, Herbert},
  title = {A Functional Approach to Worst-Case Execution Time Analysis},
  booktitle = {Functional and Constraint Logic Programming - 20th International Workshop,
        {WFLP} 2011, Odense, Denmark, July 19th, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {6816},
  pages = {86-103},
  publisher = {Springer},
  year = {2011},
  url = {https://doi.org/10.1007/978-3-642-22531-4_6},
  doi = {10.1007/978-3-642-22531-4_6}
}

Model-Checking Temporal Properties of Real-Time HTL Programs.

2010

Carvalho, André and Carvalho, Joel and Pinto, Jorge Sousa and de Sousa, Simão Melo.
Leveraging Applications of Formal Methods, Verification, and Validation - 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II 6416. Pages 191-205.
DOI: 10.1007/978-3-642-16561-0_22

@inproceedings{conf/isola/CarvalhoCPS10,
  author = {Carvalho, André and Carvalho, Joel and Pinto, Jorge Sousa and de Sousa, Simão Melo},
  editor = {Margaria, Tiziana and Steffen, Bernhard},
  title = {Model-Checking Temporal Properties of Real-Time {HTL} Programs},
  booktitle = {Leveraging Applications of Formal Methods, Verification, and Validation
      - 4th International Symposium on Leveraging Applications, ISoLA 2010,
      Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part {II}},
  series = {Lecture Notes in Computer Science},
  volume = {6416},
  pages = {191-205},
  publisher = {Springer},
  year = {2010},
  url = {https://doi.org/10.1007/978-3-642-16561-0_22},
  doi = {10.1007/978-3-642-16561-0_22}
}

Partial Derivative Automata Formalized in Coq.

2010

Almeida, José Bacelar and Moreira, Nelma and Pereira, David and de Sousa, Simão Melo.
Implementation and Application of Automata - 15th International Conference, CIAA 2010, Winnipeg, MB, Canada, August 12-15, 2010. Revised Selected Papers 6482. Pages 59-68.
DOI: 10.1007/978-3-642-18098-9_7

@inproceedings{conf/wia/AlmeidaMPS10,
  author = {Almeida, José Bacelar and Moreira, Nelma and Pereira, David and de Sousa, Simão Melo},
  editor = {Domaratzki, Michael and Salomaa, Kai},
  title = {Partial Derivative Automata Formalized in Coq},
  booktitle = {Implementation and Application of Automata - 15th International Conference,
        {CIAA} 2010, Winnipeg, MB, Canada, August 12-15, 2010. Revised Selected
        Papers},
  series = {Lecture Notes in Computer Science},
  volume = {6482},
  pages = {59-68},
  publisher = {Springer},
  year = {2010},
  url = {https://doi.org/10.1007/978-3-642-18098-9_7},
  doi = {10.1007/978-3-642-18098-9_7}
}

Guest Editorial.

2008

de Sousa, Simão Melo.
Comput. Sci. Inf. Syst. 5(2).

@article{journals/comsis/Sousa08,
  author = {de Sousa, Simão Melo},
  title = {Guest Editorial},
  journal = {Comput. Sci. Inf. Syst.},
  volume = {5},
  number = {2},
  year = {2008},
  url = {http://www.comsis.org/ComSIS/Vol5No2/EditorialG.htm}
}

Secure Biometric Authentication with Improved Accuracy.

2008

Barbosa, Manuel and Brouard, Thierry and Cauchie, Stéphane and de Sousa, Simão Melo.
Information Security and Privacy, 13th Australasian Conference, ACISP 2008, Wollongong, Australia, July 7-9, 2008, Proceedings 5107. Pages 21-36.
DOI: 10.1007/978-3-540-70500-0_3

@inproceedings{conf/acisp/BarbosaBCS08,
  author = {Barbosa, Manuel and Brouard, Thierry and Cauchie, Stéphane and de Sousa, Simão Melo},
  editor = {Mu, Yi and Susilo, Willy and Seberry, Jennifer},
  title = {Secure Biometric Authentication with Improved Accuracy},
  booktitle = {Information Security and Privacy, 13th Australasian Conference, {ACISP}
        2008, Wollongong, Australia, July 7-9, 2008, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {5107},
  pages = {21-36},
  publisher = {Springer},
  year = {2008},
  url = {https://doi.org/10.1007/978-3-540-70500-0_3},
  doi = {10.1007/978-3-540-70500-0_3}
}

Lissom, a Source Level Proof Carrying Code Platform.

2008

Gomes, João and Martins, Daniel and de Sousa, Simão Melo and Pinto, Jorge Sousa.
CoRR abs/0803.2317.

@article{journals/corr/abs-0803-2317,
  author = {Gomes, João and Martins, Daniel and de Sousa, Simão Melo and Pinto, Jorge Sousa},
  title = {Lissom, a Source Level Proof Carrying Code Platform},
  journal = {CoRR},
  volume = {abs/0803.2317},
  year = {2008},
  url = {http://arxiv.org/abs/0803.2317},
  archiveprefix = {arXiv},
  eprint = {0803.2317}
}

Secure Biometric Authentication With Improved Accuracy.

2008

Barbosa, Manuel and Cauchie, Stéphane and Brouard, Thierry and de Sousa, Simão Melo.
IACR Cryptology ePrint Archive 2008. Pages 302.

@article{journals/iacr/BarbosaCBS08,
  author = {Barbosa, Manuel and Cauchie, Stéphane and Brouard, Thierry and de Sousa, Simão Melo},
  title = {Secure Biometric Authentication With Improved Accuracy},
  journal = {IACR Cryptology ePrint Archive},
  volume = {2008},
  pages = {302},
  year = {2008},
  url = {http://eprint.iacr.org/2008/302}
}

IS 2007 PC Co-chairs’ Message.

2007

Freire, Mário M. and de Sousa, Simão Melo and Santos, Vítor and Park, Jong Hyuk.
On the Move to Meaningful Internet Systems 2007: CoopIS, DOA, ODBASE, GADA, and IS, OTM Confederated International Conferences CoopIS, DOA, ODBASE, GADA, and IS 2007, Vilamoura, Portugal, November 25-30, 2007, Proceedings, Part II 4804. Pages 1527.
DOI: 10.1007/978-3-540-76843-2_28

@inproceedings{conf/otm/FreireSSP07,
  author = {Freire, Mário M. and de Sousa, Simão Melo and Santos, Vítor and Park, Jong Hyuk},
  editor = {Meersman, Robert and Tari, Zahir},
  title = {IS 2007 PC Co-chairs' Message},
  booktitle = {On the Move to Meaningful Internet Systems 2007: CoopIS, DOA, ODBASE,
        GADA, and IS, {OTM} Confederated International Conferences CoopIS,
        DOA, ODBASE, GADA, and {IS} 2007, Vilamoura, Portugal, November 25-30,
        2007, Proceedings, Part {II}},
  series = {Lecture Notes in Computer Science},
  volume = {4804},
  pages = {1527},
  publisher = {Springer},
  year = {2007},
  url = {https://doi.org/10.1007/978-3-540-76843-2_28},
  doi = {10.1007/978-3-540-76843-2_28}
}

IS 2006 PC Co-chairs’ Message.

2006

Freire, Mário M. and de Sousa, Simão Melo and Santos, Vítor.
On the Move to Meaningful Internet Systems 2006: OTM 2006 Workshops, OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, COMINF, IS, KSinBIT, MIOS-CIAO, MONET, OnToContent, ORM, PerSys, OTM Academy Doctoral Consortium, RDDS, SWWS, and SeBGIS 2006, Montpellier, France, October 29 - November 3, 2006. Proceedings, Part I 4277. Pages 311.
DOI: 10.1007/11915034_54

@inproceedings{conf/otm/FreireSS06,
  author = {Freire, Mário M. and de Sousa, Simão Melo and Santos, Vítor},
  editor = {Meersman, Robert and Tari, Zahir and Herrero, Pilar},
  title = {IS 2006 PC Co-chairs' Message},
  booktitle = {On the Move to Meaningful Internet Systems 2006: {OTM} 2006 Workshops,
  {OTM} Confederated International Workshops and Posters, AWeSOMe, CAMS,
  COMINF, IS, KSinBIT, MIOS-CIAO, MONET, OnToContent, ORM, PerSys, {OTM}
  Academy Doctoral Consortium, RDDS, SWWS, and SeBGIS 2006, Montpellier,
  France, October 29 - November 3, 2006. Proceedings, Part {I}},
  series = {Lecture Notes in Computer Science},
  volume = {4277},
  pages = {311},
  publisher = {Springer},
  year = {2006},
  url = {https://doi.org/10.1007/11915034_54},
  doi = {10.1007/11915034_54}
}

Tool-Assisted Specification and Verification of Typed Low-Level Languages.

2005

Barthe, Gilles and Courtieu, Pierre and Dufay, Guillaume and de Sousa, Simão Melo.
J. Autom. Reasoning 35(4). Pages 295-354.
DOI: 10.1007/s10817-005-0084-6

@article{journals/jar/BartheCDS05,
  author = {Barthe, Gilles and Courtieu, Pierre and Dufay, Guillaume and de Sousa, Simão Melo},
  title = {Tool-Assisted Specification and Verification of Typed Low-Level Languages},
  journal = {J. Autom. Reasoning},
  volume = {35},
  number = {4},
  pages = {295-354},
  year = {2005},
  url = {https://doi.org/10.1007/s10817-005-0084-6},
  doi = {10.1007/s10817-005-0084-6}
}

Tool-Assisted Specification and Verification of the JavaCard Platform.

2002

Barthe, Gilles and Courtieu, Pierre and Dufay, Guillaume and de Sousa, Simão Melo.
Algebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings 2422. Pages 41-59.
DOI: 10.1007/3-540-45719-4_4

@inproceedings{conf/amast/BartheCDS02,
  author = {Barthe, Gilles and Courtieu, Pierre and Dufay, Guillaume and de Sousa, Simão Melo},
  editor = {Kirchner, Hélène and Ringeissen, Christophe},
  title = {Tool-Assisted Specification and Verification of the JavaCard Platform},
  booktitle = {Algebraic Methodology and Software Technology, 9th International Conference,
        {AMAST} 2002, Saint-Gilles-les-Bains, Reunion Island, France, September
        9-13, 2002, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {2422},
  pages = {41-59},
  publisher = {Springer},
  year = {2002},
  url = {https://doi.org/10.1007/3-540-45719-4_4},
  doi = {10.1007/3-540-45719-4_4}
}

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.

2002

Barthe, Gilles and Dufay, Guillaume and Jakubiec, Line and de Sousa, Simão Melo.
Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers 2294. Pages 32-45.
DOI: 10.1007/3-540-47813-2_3

@inproceedings{conf/vmcai/BartheDJS02,
  author = {Barthe, Gilles and Dufay, Guillaume and Jakubiec, Line and de Sousa, Simão Melo},
  editor = {Cortesi, Agostino},
  title = {A Formal Correspondence between Offensive and Defensive JavaCard Virtual
        Machines},
  booktitle = {Verification, Model Checking, and Abstract Interpretation, Third International
        Workshop, {VMCAI} 2002, Venice, Italy, January 21-22, 2002, Revised
        Papers},
  series = {Lecture Notes in Computer Science},
  volume = {2294},
  pages = {32-45},
  publisher = {Springer},
  year = {2002},
  url = {https://doi.org/10.1007/3-540-47813-2_3},
  doi = {10.1007/3-540-47813-2_3}
}

Jakarta: A Toolset for Reasoning about JavaCard.

2001

Barthe, Gilles and Dufay, Guillaume and Huisman, Marieke and de Sousa, Simão Melo.
Smart Card Programming and Security, International Conference on Research in Smart Cards, E-smart 2001, Cannes, France, September 19-21, 2001, Proceedings 2140. Pages 2-18.
DOI: 10.1007/3-540-45418-7_2

@inproceedings{conf/esmart/BartheDHS01,
  author = {Barthe, Gilles and Dufay, Guillaume and Huisman, Marieke and de Sousa, Simão Melo},
  editor = {Attali, Isabelle and Jensen, Thomas P.},
  title = {Jakarta: {A} Toolset for Reasoning about JavaCard},
  booktitle = {Smart Card Programming and Security, International Conference on Research
      in Smart Cards, E-smart 2001, Cannes, France, September 19-21, 2001,
      Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {2140},
  pages = {2-18},
  publisher = {Springer},
  year = {2001},
  url = {https://doi.org/10.1007/3-540-45418-7_2},
  doi = {10.1007/3-540-45418-7_2}
}

A Formal Executable Semantics of the JavaCard Platform.

2001

Barthe, Gilles and Dufay, Guillaume and Jakubiec, Line and Serpette, Bernard P. and de Sousa, Simão Melo.
Programming Languages and Systems, 10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings 2028. Pages 302-319.
DOI: 10.1007/3-540-45309-1_20

@inproceedings{conf/esop/BartheDJSS01,
  author = {Barthe, Gilles and Dufay, Guillaume and Jakubiec, Line and Serpette, Bernard P. and de Sousa, Simão Melo},
  editor = {Sands, David},
  title = {A Formal Executable Semantics of the JavaCard Platform},
  booktitle = {Programming Languages and Systems, 10th European Symposium on Programming,
        {ESOP} 2001 Held as Part of the Joint European Conferences on Theory
        and Practice of Software, {ETAPS} 2001 Genova, Italy, April 2-6, 2001,
        Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {2028},
  pages = {302-319},
  publisher = {Springer},
  year = {2001},
  url = {https://doi.org/10.1007/3-540-45309-1_20},
  doi = {10.1007/3-540-45309-1_20}
}

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts.
2020
Reis, João Santos and Crocker, Paul and Melo de Sousa, Simão.
arXiv:2005.11839 [cs]
arXiv: 2005.11839
[abstract]
This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, ow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.
```
@article{reisTezlaIntermediateRepresentation2020,
  title = {Tezla, an {{Intermediate Representation}} for {{Static Analysis}} of {{Michelson Smart Contracts}}},
  author = {Reis, Jo{\~a}o Santos and Crocker, Paul and {Melo de Sousa}, Sim{\~a}o},
  year = {2020},
  month = may,
  archiveprefix = {arXiv},
  eprint = {2005.11839},
  eprinttype = {arxiv},
  file = {C\:\\Users\\joaos\\OneDrive - Universidade da Beira Interior\\Zotero\\storage\\P4UQQKTI\\Reis et al. - 2020 - Tezla, an Intermediate Representation for Static A.pdf;C\:\\Users\\joaos\\OneDrive - Universidade da Beira Interior\\Zotero\\storage\\X7YKYGZG\\2005.html},
  journal = {arXiv:2005.11839 [cs]},
  keywords = {Computer Science - Programming Languages},
  primaryclass = {cs}
}
```

Publications

2019

2017

2015

2015

2015

2014

2013

2013

2012

2012

2011

2011

2011

2010

2010

2008

2008

2008

2008

2007

2006

2005

2002

2002

2001

2001

2020