Luca Ferro – Curriculum Vitae
Italian citizenship, born 1982.
- 2008-11: Ph.D. "Verification of temporal properties for SystemC TLM specifications". 3 years and 8 months. TIMA Research Lab, Grenoble, France
- Developed a mechanism to monitor functional requirements during the simulation of timed/untimed SystemC Transaction Level Models (Loosely Timed, Approximately Timed, Cycle Accurate/Bit Accurate...) [1]
- Implemented a framework for the dynamic verification of functional requirements during system-level simulation: the ISIS tool [2] [4] [6] [9]
- Main technologies: Java, C++, JFlex/CUP, XML, Bash, GNU Make, SVN, NetBeans
- Proposed a formal operational semantics of PSL (IEEE 1850 Property Specification Language) extended with the notion of global and local variables [7] [8]
- Involved in the SoCKET Project [9]
- Cooperation with Astrium, STMicroelectronics, Airbus
- Involved in the SFINCS Project
- Cooperation with Thales, Dolphin Integration
- 2008-10: Teaching Associate (moniteur de l'enseignement supérieur) in Computer Science. 3 years, ~200 hours. Université de Grenoble (UJF), France
- Object-oriented modeling of Information Systems with UML
- Databases and Information Systems, Database Management Systems (Oracle), SQL
- Middleware (Java)
- 2007: Internship "Checkers generation for SystemC TLM designs". 6 months. TIMA Research Lab, Grenoble, France
- Adapted an existing technique, initially suited to VHDL RTL, to the construction of SystemC TLM-oriented verification modules
- Main technologies: C, C++, VHDL, Flex/Bison, GNU Make, MPI/MPICH
- 2006: Project "Formalization of the neuro-biological models for spike neurons". ~12 weeks, undergraduate research project. Université de Nice-Sophia Antipolis, France
- Analyzed and evaluated a set of techniques and tools for the validation and for the processing of a large amount of XML data
- Technologies: XML, DTD, W3C XML Schema, Relax NG, Schematron, XSLT, CDuce
- Contributed to the FACETS project and submitted an INRIA Technical Report
- 2011: Ph.D. in Micro and Nano Electronics, Université de Grenoble (Grenoble INP), France. Advisor: Professor Laurence Pierre
- 2007: Master's Degree (French Bac+5, equivalent to a Master thesis) in Computer Science - Embedded Systems, Université de Nice-Sophia Antipolis, France
- 2005: French License (French undergraduate diploma) in Computer Science, Université de Nice-Sophia Antipolis, France
- 2001: High school diploma in modern languages, Liceo G.D. Cassini, Sanremo, Italy
- Methods and concepts: object-oriented and functional paradigms, parsing techniques, Assertion-Based Verification, specification languages (PSL, SVA, temporal logics), UML (Unified Modeling Language), aspect-oriented paradigm (notions)
- Programming, scripting, data manipulation: C, C++, Java, Lisp/Scheme, Caml, Bash, XML, SQL, Lex/Yacc, assembly languages (notions)
- Development environments and tools: Build systems (GNU Make...), Source Control Management (Subversion, CVS...), Integrated Devlopment Environments (NetBeans, Eclipse, Objecteering...)
- Operating systems: Linux/Unix (with notions of kernel modules development), Windows, Solaris
- Hardware-related: SystemC and TLM libraries, VHDL, IP-XACT, IBM FoCs, Mentor Graphics ModelSim/Questa
- Text processing: LaTeX, Microsoft Office and OpenOffice
- Italian: mother tongue
- French: fluent
- English: fluent
- German: notions
Publications and Contributions
- L.Pierre, L.Ferro
"A Tractable and Fast Method for Monitoring SystemC TLM Specifications"
IEEE Transactions on Computers, Vol. 57(10), October 2008 (Special Section on Programming Models and Architectures for Embedded Systems) - L.Ferro, L.Pierre, Y.Ledru, L.Du Bousquet
"Generation of Test Programs for the Assertion-Based Verification of TLM Models"
Proc. IEEE International Design and Test Workshop (IDT'08), Monastir (Tunisia), December 2008 - Presentation "A Tool for Assertion-Based Verification of TLM Platforms"
11th North American SystemC User's Group (NASCUG), San Francisco (CA), July 2009 - L.Ferro, L.Pierre
"ISIS: Runtime Verification of TLM Platforms"
Proc. Forum on Specification and Design Languages (FDL'09), Sophia-Antipolis (France), September 2009
(Best Paper Award) - Presentation "Using Temporal Assertions for Evaluating the Correctness and Safety of Embedded Systems"
Workshop on Simulation Based Development of Certified Embedded Systems (SBDCES), Awaji Yumebutai International Conference Center (Japan), October 2009 - L.Ferro, L.Pierre
"ISIS: Runtime Verification of TLM Platforms"
Advances in Design Methods from Modeling Languages for Embedded Systems and SoC's (Selected Contributions from FDL'09), Lecture Notes in Electrical Engineering (vol. 63), Springer, 2010 - L.Ferro, L.Pierre
"Formal Semantics for PSL Modeling Layer and Application to the Verification of Transactional Models"
Proc. Design, Automation and Test in Europe Conference and Exhibition (DATE'10), Dresden (Germany), March 2010 - L.Pierre, L.Ferro
"Enhancing the Assertion-Based Verification of TLM Designs with Reentrancy"
Proc. 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'10), Grenoble (France), July 2010 - L.Ferro, L.Pierre, Z.Bel Hadj Amor, J.Lachaize, V.Lefftz
"Runtime Verification of Typical Requirements for a Space Critical SoC Platform"
To appear in Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'2011), Trento (Italy), August 2011, Springer - L.Pierre, L.Ferro
"Dynamic Verification of SystemC Transactional Models"
To appear in "Model-Based Testing for Embedded Systems" (Series "Computational Analysis, Synthesis, and Design of Dynamic Systems"), Chapter 22, CRC Press