Roberto Bruttomesso

Leading the Arc and Arc Embedded projects — Nozomi's endpoint sensor line for industrial and IoT environments.

Managed engineering work across the Guardian and Remote Collector products, and led the Arc project from its early stages.

Engineering team leader for the Guardian and Remote Collector projects.

Development of SCADAGuardian, Nozomi's flagship OT network monitoring product.

• Analysis and development of advanced algorithms inside AXEL's LogicLab product for industrial automation (PLC).
• Customisation for specific customer requests, working directly with customer representatives.
• Full-cycle collaboration with the team: planning and scheduling, development, debugging and test.

• Research and development of formal methods for embedded systems — model checking, SAT, SMT, BDDs — applied to requirement analysis, safety verification and automated test generation.
• Built a new C++ verification framework achieving 2–3 orders of magnitude speed-up over the legacy version on industrial-sized designs.
• Extended and debugged the proprietary solution translating and analysing MATLAB/Simulink models via model checking and simulation.
• Worked closely with UTAS (United Technologies Aerospace) engineers on customised verification solutions, and with FBK on adapting novel algorithms to aerospace problems.

• Research and development of formal techniques for hardware verification — model checking via SAT, SMT and BDDs, sequential equivalence checking — inside the SpyGlass tool, on a monthly release cadence.
• Close collaboration with the San Jose (USA) and Noida (India) teams.
• New techniques for customer-specific verification and performance problems; debugging, validation, testing and benchmarking.
• Mined state-of-the-art literature for new ideas, wrote technical and scientific specifications, and represented Atrenta at international conferences.

• Formal methods for software verification using SMT; development and integration of the MCMT and OpenSMT tools, with a strong focus on outperforming competing solvers.
• Research in model checking — 6 publications in international conferences or journals.
• Teaching assistant. Research project awarded an additional monetary prize.

• Main architect and developer of OpenSMT, an open-source SMT solver, with special effort on performance excellence over competing tools.
• Research in constraint solving with SMT — 6 publications in international conferences or journals.
• Teaching assistant; co-supervised 3 PhD students; contributed to research grant writing (SNF and European projects).

Princeton, New Jersey. Development of decision procedures and their integration into the proprietary FSOFT suite.

Development of scientific software in C/C++.

Formal methods 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/30.