Software Engineer, Researcher
+39 349 29 19 325
Software and lectures on Github
A printable CV (Europass format)
Engineering Manager, for multiple internal projects.
Engineering Team leader, for multiple internal projects.
Development of Nozomi's SCADAGuardian flagship software.
Analysis and Development of advanced algorithms inside Axel’s LogicLab product for applications to Industrial Automation (PLC).
Customization for specific customer requests. Close interaction with the customer’s representatives.
Interaction with the rest of the team on all aspects of software development: planning and scheduling of activities, development, debugging, and test.
Research and Development of formal methods techniques for Embedded Systems using Model Checking, SAT, SMT, BDDs, for Requirement Analysis, Safety Verification, Automated Test Generation. Developed new verification framework in C++ that has achieved from 2 to 3 orders of magnitude performance improvement on industrial-sized designs compared to legacy version.
Extension and debugging of current proprietary solution to translate and analyze MATLAB/Simulink models via model checking and simulation techniques.
Close collaboration with UTAS (United Technologies Aero-Space) engineers for the definition of customized formal verification solutions to be built on top of proprietary MATLAB/Simulink based verification solution.
Worked on real, industrial-sized models.
Close interaction with FBK (Fondazione Bruno Kessler) research center for the identification and adaption of novel verification algorithms for aero-space problems.
Research and Development of formal techniques for hardware verification via Model Checking using SAT, SMT, BDDs (sequential equivalence checking) within the tool SpyGlass, with monthly releases. Strict collaboration with the teams in San Jose (USA) and Noida (India).
Activities included but were not limited to: development and coding of new techniques to help the customer to solve specific verification and performance related tasks, debugging, validation, testing and benchmarking, study of the state-of-the-art scientific publications to mine for new ideas, writing of technical and scientific specifications, representative for Atrenta in international conferences.
Research and development of formal methods techniques for software verification using SMT. Development of tool MCMT and OpenSMT and their integration.Special effort in performance excellence over competing tools. Research in the area of Model Checking (6 publications in international conferences or journals). Teaching assistant. Research project awarded with additional monetary prize.
Research and development of formal methods techniques based on constraint solving via SMT: Main Architect and Developer of tool OpenSMT. Special effort in performance excellence over competing tools. Research in the area of constraint solving with SMT (6 publications in international conferences or journals). Teaching assistant. Assistant in supervising 3 PhD students. Collaboration in writing of research grants (SNF and European projects).
Intership at the NEC Labs of Princeton, (New Jersey, USA). Development of decision procedures and integration in the proprietary suite FSOFT.
Development of scientific software in C/C++.
Research and development of formal methods techniques based on constraint solving via SMT. 11 publications in international conferences or journals). Teaching assistant.
Final grade: 110/110 cum laude (average exam grade 28.85)
List of exams with grades: