Simpósio Brasileiro de Linguagens de Programação
When re-boot unfreezes a computer
A computer may block or freeze due to a wide variety of hardware or software problems. If rebooting the machine unfreezes it, most possibly the machine ran out of memory. This talk looks at the evolution of dynamic memory management and provides advice to avoid computer freezing.
Rafael Dueire Lins holds a B.Sc. degree in Electrical Engineering (Electronics) from the Federal University of Pernambuco, Brazil (1982) and a Ph.D. degree in Computing from the University of Kent at Canterbury, UK (1986). Lins published several books, amongst them the best-seller `Garbage Collection: Algorithms for Dynamic Memory Management`, (John Wiley Sons , UK,1996) translated into Chinese (Mandarin) and published by ChinaPub in 2004. His pioneering contributions encompass the creation of the Lambda-Calculus with explicit substitutions, the first general and efficient solution to cyclic reference counting in sequential, parallel and distributed architectures. Lins is the pioneer researcher in document engineering and digital libraries in Latin America. Lins is a founding member of the doctoral programme in Computer Science (1990) and in Electrical Engineering (2000) both at Federal University of Pernambuco, Brazil. Lins is currently Senior Researcher of CNPq (Brazil) and Associate Editor of Springer Nature in Computer Science. Further information may be found at Google Scholar
From operational semantics to verified compilation: mechanized reasoning on realistic languages in the CompCert compiler
A formally verified compiler ensures that compilation does not introduce any bugs in programs. In the CompCert C compiler, this correctness property requires reasoning about realistic languages by using a semantic framework. This talk explains how this framework has been effectively used to turn CompCert from a prototype in a lab into a real-world compiler. More generally, this approach opens the way to the verification of software tools involved in the production and verification of software.
Sandrine Blazy is professor at the University of Rennes and deputy director of the IRISA CNRS laboratory. Her research interests include verified compilation with the CompCert C compiler, formal semantics, deductive verification, static analysis and software security. CompCert has won several awards, including the ACM software system award (2021), the ACM SIGPLAN Programming Languages Software Award (2022). Sandrine Blazy received in 2023 the CNRS silver medal.