Differences

This shows you the differences between two versions of the page.

--- work:semana_25_de_2021 [2021/06/21 19:53] – [Research] magsilva
+++ work:semana_25_de_2021 [2021/09/14 14:55] (current) – ↷ Links adapted because of a move operation 65.21.179.252
@@ Line 2: / Line 2: @@
 ==== Research ====
-  * Request funding for [[Yuri Rafael Grajefe Feitosa]]: Processes SEI 23064.026359/2021-09 (EduComp 2021) and 23064.026367/2021-47 (WEI 2021).
+  * Request funding for [[.students: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 [[http://theory.stanford.edu/~nikolaj/programmingz3.html | 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 [[https://github.com/AbsInt/CompCert | CompCert]], a certified (correctness verified) C compiler. It will be nice to compare test results for applications compiled with C and CompCert.
+  * After analyzing the rebuttal of SBES's papers, I found some interesting static analysis tools:
+    * [[https://clang-analyzer.llvm.org/available_checks.html]] clang-analyzer
+    * [[https://lgtm.com/ | Semmle LGTM]] (engine -- CodeQL) is open source, but not the queries/rules.
+    * [[https://github.com/scovetta/yasca | Yasca]]
+    * [[https://github.com/tsantalis/JDeodorant | JDeodorant]]: detecção de code smells.
+    * [[https://github.com/hcvazquez/JSpIRIT | JSpIRIT]]: detecção de code smells.
+  * [[https://github.com/github/codeql | 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 [[.students:bruno_henrique_pachulski_camara]]: results with test smells, SAS 2021.
+  * Talk to [[.students:allison_alfredo_de_oliveira_sampaio]]: plan implementation of the approach.
+  * Watch talk about surveys: https://www.youtube.com/watch?v=aVFQSuXCHbg. Quite interesting, indeed. I will ask [[.students:leandro_césar_da_cruz]] to watch it too.