3 Search Results for "Santos, Frederico"

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.24
Toward Tool-Independent Summaries for Symbolic Execution

Authors: Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
We introduce a new symbolic reflection API for implementing tool-independent summaries for the symbolic execution of C programs. We formalise the proposed API as a symbolic semantics and extend two state-of-the-art symbolic execution tools with support for it. Using the proposed API, we implement 67 tool-independent symbolic summaries for a total of 26 libc functions. Furthermore, we present SumBoundVerify, a fully automatic summary validation tool for checking the bounded correctness of the symbolic summaries written using our symbolic reflection API. We use SumBoundVerify to validate 37 symbolic summaries taken from 3 state-of-the-art symbolic execution tools, angr, Binsec and Manticore, detecting a total of 24 buggy summaries.
Cite as

Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos. Toward Tool-Independent Summaries for Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ramos_et_al:LIPIcs.ECOOP.2023.24,
  author =	{Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
  title =	{{Toward Tool-Independent Summaries for Symbolic Execution}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{24:1--24:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.24},
  URN =		{urn:nbn:de:0030-drops-182171},
  doi =		{10.4230/LIPIcs.ECOOP.2023.24},
  annote =	{Keywords: Symbolic Execution, Runtime Modelling, Symbolic Summaries}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.7
Toward Tool-Independent Summaries for Symbolic Execution (Artifact)

Authors: Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
The artifact contains the extended versions of the tools angr and AVD with support for the symbolic reflection API proposed in the paper. Additionally, the artifact contains the source code of SumBoundVerify, our novel tool for the bounded-verification of symbolic summaries for the C programming language. The artifact contains all the scripts and datasets required to obtain the results presented in the paper, including: a library of 67 symbolic summaries implemented using the proposed symbolic reflection API; two symbolic test suites designed to test two open source C libraries; and the source code of the third-party summaries that were validated checked with SumBoundVerify.
Cite as

Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos. Toward Tool-Independent Summaries for Symbolic Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 7:1-7:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{ramos_et_al:DARTS.9.2.7,
  author =	{Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
  title =	{{Toward Tool-Independent Summaries for Symbolic Execution (Artifact)}},
  pages =	{7:1--7:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.9.2.7},
  URN =		{urn:nbn:de:0030-drops-182478},
  doi =		{10.4230/DARTS.9.2.7},
  annote =	{Keywords: Symbolic Execution, Runtime Modelling, Symbolic Summaries}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.2
Challenges and Solutions from an Embedded Programming Bootcamp

Authors: J. Pedro Amaro, Jorge Barreiros, Fernanda Coutinho, João Durães, Frederico Santos, Ana Alves, Marco Silva, and João Cunha

Published in: OASIcs, Volume 81, First International Computer Programming Education Conference (ICPEC 2020)

Abstract
Due to the proliferation of IT companies developing web and mobile applications, computer programmers are in such high demand that universities can’t satisfy it with newly graduated students. In response, some organisations started to create coding bootcamps, providing intensive full-time courses focused on unemployed people or individuals seeking for a career change. There is, however, a different set of skills that is becoming increasingly required, but is not addressed by those courses: embedded programming. In fact, the Internet of Things is connecting every device to the internet, thus making knowledge on hardware and C/C++ programming very relevant skills. A group of computer science and electrical engineering university teachers, in collaboration with several industry stakeholders, have promoted an embedded systems programming course in C and C++. This course is based on an intensive project-based approach comprising 6 months of daylong classes followed by 9 months of paid internships. After two editions, thirty embedded programmers, with no relevant previous programming experience, have been placed with the partners’ working force. In this paper, the course organisation and pedagogical methodologies are described. Problems, challenges and adopted solutions are presented and analysed. We conclude that in spite of the intense rhythm and demanding nature of the subject matter, it is possible to find the structure and solutions that keep students engaged and motivated throughout the course, allowing them to gain the required competences and successfully transition into a new career path.
Cite as

J. Pedro Amaro, Jorge Barreiros, Fernanda Coutinho, João Durães, Frederico Santos, Ana Alves, Marco Silva, and João Cunha. Challenges and Solutions from an Embedded Programming Bootcamp. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{amaro_et_al:OASIcs.ICPEC.2020.2,
  author =	{Amaro, J. Pedro and Barreiros, Jorge and Coutinho, Fernanda and Dur\~{a}es, Jo\~{a}o and Santos, Frederico and Alves, Ana and Silva, Marco and Cunha, Jo\~{a}o},
  title =	{{Challenges and Solutions from an Embedded Programming Bootcamp}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{2:1--2:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-153-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{81},
  editor =	{Queir\'{o}s, Ricardo and Portela, Filipe and Pinto, M\'{a}rio and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2020.2},
  URN =		{urn:nbn:de:0030-drops-122896},
  doi =		{10.4230/OASIcs.ICPEC.2020.2},
  annote =	{Keywords: Coding Bootcamp, Embedded Programming, Career Change}
}
  • Refine by Author
  • 2 Adão, Pedro
  • 2 Fragoso Santos, José
  • 2 Naumann, David A.
  • 2 Ramos, Frederico
  • 2 Sabino, Nuno
  • Show More...

  • Refine by Classification
  • 2 Security and privacy → Formal methods and theory of security
  • 2 Software and its engineering → Software verification and validation
  • 1 Social and professional topics → Computing education

  • Refine by Keyword
  • 2 Runtime Modelling
  • 2 Symbolic Execution
  • 2 Symbolic Summaries
  • 1 Career Change
  • 1 Coding Bootcamp
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2023
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact