Avatar

Roberto Bruttomesso

Software Engineer, Researcher

Varese, Italy

roberto.bruttomesso@gmail.com

+39 349 29 19 325

My Formal Methods blog

Software and lectures on Github

List of publications

A lecture I gave at MIT

A printable CV (Europass format)


Skills

C++

100%

Java

80%

Python

80%

Languages

Italian

English

French



Work Experience

Software Engineer, Cybersecurity / Nozomi Networks
April 2018 - Current

Development of Nozomi's SCADAGuardian flagship software.


Senior Software Engineer / AXEL S.r.l.
June 2016 - March 2018

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 Engineer / ALES, United Technologies Research Centre
September 2014 - May 2016

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.


Senior Member of Consulting Staff / Atrenta
March 2012 - August 2014

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 Assistant / University of Milan
August 2011 - February 2012

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 Assistant / University of Lugano
November 2007 - July 2011

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).

Intern / NEC Labs. America
January 2007 - March 2007

Intership at the NEC Labs of Princeton, (New Jersey, USA). Development of decision procedures and integration in the proprietary suite FSOFT.

Programmer / Fondazione Bruno Kessler (FBK)
August 2004 - September 2004

Development of scientific software in C/C++.

Education

Fondazione Bruno Kessler (FBK) / University of Trento
2004 - 2007
PhD

Research and development of formal methods techniques based on constraint solving via SMT. 11 publications in international conferences or journals). Teaching assistant.


University of Milan
1999 - 2004
Master Degree

Final grade: 110/110 cum laude (average exam grade 28.85)

List of exams with grades:

  • Programming I [30/30 cum laude]
  • Discrete Mathematics [30/30]
  • Computer Architecture [30/30 cum laude]
  • Mathematical Analysis I [30/30]
  • Physics I [30/30 cum laude]
  • Mathematical Analysis II [21/30]
  • Physics II [30/30]
  • Logic I [30/30 cum laude]
  • Logic II [30/30 cum laude]
  • Operating Systems [27/30]
  • Programming Languages [24/30]
  • Numerical Analysis [30/30 cum laude]
  • Probability Calculus and Statistics [30/30]
  • Formal Methods [30/30]
  • Theory of Computation [28/30]
  • Information Theory [30/30 cum laude]
  • Algorithms and Data Structures [28/30]
  • Graph Theory [30/30 cum laude]
  • Automated Reasoning [30/30 cum laude]
  • Artificial Intelligence [30/30]
  • Computer Networks [28/30]