Vertex RE

Software Analysis and Security Services

+44 1865 403253

Our classes focus on providing in-depth program analysis material in a manner that is real-world applicable. For bookings email  Private classes are available on request, provided a minimum number of students is reached.

Upcoming Public Trainings

We will host the first public version of the 4 day Advanced Tool Development with SMT Solvers training from Nov 6th-9th in London, UK. This class features a significant amount of new material on the state of the art in symbolic execution systems (see below for an overview and syllabus). Email for bookings or with any enquiries. 

Dates: November 6th-9th 2017 (4 days).
Venue: Imparando, 56 Commercial Rd, Whitechapel, London E1 1LP, UK.
Price:  Early bird (until September 8th) 3825 GBP per student. Full price (after September 8th) 4250 GBP per student. Prices do not include VAT, which may be relevant in some cases.  
Booking: Email Payment may be made via wire transfer or credit card. 
Student Contest: As with our previous public trainings there will be a free student* seat. To enter send an email to with a link to the public source code for some program analysis automation project** you've worked on in the past 12 months (if it's not your own project then include a link to your specific contributions). We'll decide the winner based on novelty, practicality and usability. The deadline for entry is the 16th of September 2017. 
* You must be a full-time student, with a valid student ID, as of the date of the training.  
** The project doesn't have to be related to SMT solvers. Some of last year's entries included a malware analysis system, a fuzzer and a debugger extension.  

Advanced Tool Development with SMT Solvers (4 Days)

Trainer: Sean Heelan

This class is designed to introduce students to the cutting edge of research in program analysis based on SMT solvers and symbolic reasoning. With a focus on practical applications, we will cover the theory and implementation behind a number of techniques developed in recent years that have relevance in vulnerability discovery, exploit development, and reverse engineering. Over the four days, we will go from the foundations of problem solving with SMT solvers through to the construction of analysis systems capable of reasoning about complex problems in real software.  Students will also be introduced to a variety of existing analysis systems, including KLEE, angr, manticore and CBMC, and learn their strengths and weaknesses.

This class features extensive exercises and we require students to be comfortable developing software in Python and have familiarity with the x86 ISA. A grasp of foundational computer science, such as propositional logic, will also be of use but is not a requirement. Some of the topics to be covered include:

  • Modelling problems with SMT solvers, and their usage in understanding complex code
  • Vulnerability detection and program exploration with symbolic execution
  • Concolic execution & whitebox fuzzing, i.e. SMT solver driven fuzzing
  • Usage of open-source symbolic execution frameworks
  • Intermediate languages
  • Static vs dynamic analysis - limitations, strengths, and contrasts
  • General guidance on adding automation to RE, code auditing, and exploitation workflows

A detailed syllabus can be found here. For further information, pricing and bookings please email Private trainings are available on request.