Monday, 21th of June 2021

Request funding for Yuri Rafael Grajefe Feitosa: Processes SEI 23064.026359/2021-09 (EduComp 2021) and 23064.026367/2021-47 (WEI 2021).

Read “The Role of Formalism in System Requirements”. It is a pretty general paper on requirements (requirement documents/specifications) and the languages you can use to write them (from natural language to formal languages). I got a great link about i* though: https://github.com/jhcp/piStar. It is a i* tool, supporting the i* 2.0 specification. It is easy to install and run it: simply download the files (clone the repository) and load the index.html. That is, quite simple! Another cool site I've found is https://www.capterra.com/requirements-management-software/, a directory on requirements engineering tools. I used that directory to update my course with links to several tools (and tutorials).

Read July issue of Communications of the ACM. There are several papers on software verification and, more specifically, on program proofing. Read them all. While doing that, I stumbled across Z3. I already heard about it when lecturing formal languages and addressing SAT. Z3, as Isabelle and H4, are theorem provers. Z3 relies on SAT and SMT. At is tutorial page there is a nice example on using Z3 to solve a SAT problem. That will be useful for next year (or 2023)!

Another interesting stuff I have found is CompCert, a certified (correctness verified) C compiler. It will be nice to compare test results for applications compiled with C and CompCert.

Semmle CodeQL is used by LGTM. CodeQL indexes the source code of projects, allowing you to run queries (considering features of the programming language). More information about it is available at https://codeql.github.com/docs/. Some sample queries for security analysis are available at https://github.com/github/securitylab

Talk to Bruno Henrique Pachulski Camara.